[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] first steps in TLA - recursive functions don't work

Thanks for the clarification, Stephan, I greatly appreciate your help.


On Wednesday, February 12, 2014 3:20:30 PM UTC+1, Stephan Merz wrote:

this is another limitation of the current prover that should be mentioned more clearly in the doc (http://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html). in TLA+, f[a,b] is shorthand for f[<<a,b>>], and unfortunately the prover doesn't do this transformation yet. For the time being, I rather recommend "currying" the function, i.e. define f as a function of type [Nat -> [Nat -> whatever]] and write f[1][2].


On 12 Feb 2014, at 10:40, tk <tade...@xxxxxxxxx> wrote:


thank you very much for a swift reply. It clarified a lot!

One more function-related question. How should I work with (non-recursive) functions that take multiple arguments? For instance, I get red highlight when trying to prove that f[1,2] = 3 for a function f: 

f[a \in Nat, b \in Nat] == a + b


On Wednesday, February 12, 2014 1:30:40 PM UTC+1, Stephan Merz wrote:
Hello Ted,

welcome to the TLA+ group!

I had a quick look at your module, and gather that your problems are about proving theorems using TLAPS. Did you experiment with TLC first? I hope that you didn't encounter any significant problems there — except that TLC cannot evaluate definitions such as

foo2 == CHOOSE f : f = [ n \in Nat |-> n * n ] 

that involve an unbounded CHOOSE _expression_.

There are two types of problems in your examples. The first type involves reasoning about recursive functions such as factorial. As you well realized, the complication comes from the fact that recursive definitions involve CHOOSE expressions, so one must prove that the object that one chooses actually exists. For recursive function definitions, in particular over natural numbers, there is support through library modules (NaturalsInduction for functions of type [Nat -> S], WellFoundedInduction for more general cases), and there is some boilerplate that has to be inserted to get what you want. See attached module.

The second type involves reasoning about cardinality. Again, that boils down to CHOOSE etc., as you boldly tried to do manually.  The library module FiniteSetTheorems is your friend here, although I realized that automation is insufficient for the kind of theorem you are trying to prove.

TLAPS is still in active development, so you are bound to run into problems like these, and we'd like to hear about them. I also realized when looking at the TLAPS documentation that the existing library modules do not seem to be mentioned anywhere on the current Web pages. You will find them in directory /usr/local/lib/tlaps in a typical installation of TLAPS, and you may have to add this directory to your Toolbox search path (Toolbox -> Preferences -> TLA+ Preferences -> TLA+ library path location) if it isn't done already (cf. the instructions in the Download section of the TLAPS Web pages). Adding a notice about these modules, and documentation about their contents, is on our to-do list for the next release.

Please feel free to ask for further help, we need feedback such as this for improving the current tool.

Best regards,

Stephan Merz