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

*From*: Alex <vstrength@xxxxxxxxx>*Date*: Sat, 29 May 2021 23:42:46 -0700 (PDT)*Ironport-hdrordr*: A9a23:UKmlzqihh7NjN31hvEo7fta0LnBQXi4ji2hC6mlwRA09TyX4rbHSoB1/73XJYVkqKRYdcLy7Sc+9qZ21z+8A3WE+VY3SKTUO+1HYXL2L1OPZsk/d8lTFh5lgPMRbAtJD4GiaNykKsS+F2njBLz96+qj4zEnAv463pAYPPGRXgsdbnnhE4ymgfnGeLzM2fqbReqDsn/auZlKbGUj/rf7VOpDGZYX+T22hruOUXffLPXAaAPnkt0LV1FcyKXnovGZ7bw9y

As part of learning TLA+ I'm trying to write a spec to verify definition of some functions on Church numerals. I'm trying to start with a simple spec that verifies a definition of a successor function on Church numerals [1].

Specification-wise my approach to this is as follows:

* I define a zero numeral and successor function

* I define an upper bound integer limit up to which successor function will be verified

* Verification function would try to convert current Church numeral to an integer using "plus one" function and zero as arguments. [1]

I ended up with the following (incorrect) specification:

```

EXTENDS Integers

CONSTANT Limit \* Upper bound limit, that model will be testing

ASSUME Limit \in Nat \union {0}

FPlusOne(n) == n + 1 \* Helper function to convert Church numerals to integers

LZero(L) == [s \in L |-> [z \in L |-> z]] \* Zero numeral

LSucc(L) == [s \in L |-> [z \in L |-> s[z]]] \* Successor function for generating next Church numeral

VARIABLE

step, \* Execution step, ranging from 0 to Limit

numeral \* Church numeral, produced on each step

TypeOK == \* At every step we'll verify that current Church numeral could be correctly converted to an integer

/\ step = numeral[FPlusOne][0]

Init == \* Start with zero numeral

/\ step = 0

/\ numeral = LZero

SetNext == \* Try up to a "Limit" numbers

/\ step < Limit

/\ numeral' = LSucc[numeral]

/\ step' = step + 1

ComputationComplete == \* Stop, when we tried "Limit" worth of numerals

/\ step = Limit

/\ UNCHANGED<<step, numeral>>

Next ==

\/ SetNext

\/ ComputationComplete

-------------------------------------------------------------------------------

Spec == Init /\ [][Next]_<<step, numeral>>

```

this is predictably not working. At least one missing piece, as far as I can tell, is defining a proper domain for numeral functions - this apparently should be a union of "plus one" function, integer range from zero to "Limit" and all relevant Church numerals definitions. It seems it requires a some sort of recursive definition for set "L" in the spec above.

Another part that I don't entirely understand is how to make passing a function to a function work.

Is it even practical to do it in a way that requires a recursive definition of a domain that some functions will be defined on?

Is there a simple enough way of defining common domain for functions that may take other functions which also happen to be elements of that domain?

[1] https://en.wikipedia.org/wiki/Church_encoding#Calculation_with_Church_numerals

P.S.: The above is a toy example, but it could be extended to something much less obvious - let's say verifying that subtraction or exponent functions on Church numerals are working properly. Unlike example above, both of these may require a definition of a number of helper functions on Church numerals, so ideally I'd like to have separate definition in a spec for each function that operates on Church numerals.

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d7826de2-40f7-4224-9c84-2dd3c38bec70n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: How to pass a function as an argument to the other function?***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Re: tlc invariant violation visualization** - Next by Date:
**[tlaplus] Re: How to pass a function as an argument to the other function?** - Previous by thread:
**[tlaplus] Re: tlc invariant violation visualization** - Next by thread:
**[tlaplus] Re: How to pass a function as an argument to the other function?** - Index(es):