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

*From*: Afonso Fernandes <afonsonf42@xxxxxxxxx>*Date*: Sun, 30 May 2021 08:41:11 -0700 (PDT)*Ironport-hdrordr*: A9a23:+YLt9KPUk0fxY8BcTkqjsMiBIKoaSvp037BL7TEMdfUxSKb0qynApoV+6faZskd3ZJhko6H5BEFvKUmsg6Kcz+EqTMCftUrdyRiVxLgL1/qX/9SYIVy2ygc/79YcT0DKY+eAfWSS8/yKmTVQSOxQseVvmZrA7YyurUuFDzsaEJ2IiT0JdDpzPXcYeOAsP+tCKHPz3Lsgm9JgEU5nDfhTxUNqYwEAnbH2fCKMW29yO/fq0mizZcPC0s+EL/FQ5HduNg9n8PMZ6GDA1yb56q+gv/z+6hiZ+XTU840+oqqS9ud+*References*: <d7826de2-40f7-4224-9c84-2dd3c38bec70n@googlegroups.com> <96f53a07-fec9-4790-a1b1-850334fcdfbdn@googlegroups.com>

Here is my try of writing the specification of Church numerals, adapted from the one you posted:

```

EXTENDS Integers, TLC

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

ASSUME Limit \in Nat \union {0}

VARIABLE

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

numeral \* Church numeral, produced on each step

MyNat == 0..Limit

\* the if clause is for the function to be MyNat -> MyNat and not MyNat -> (MyNat+1)

FPlusOne == [x \in MyNat |-> IF x = Limit THEN x ELSE x + 1] \* Helper function to convert Church numerals to integers

LZero == [f \in [MyNat -> MyNat] |-> [x \in MyNat |-> x] ] \* Zero numeral

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

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

/\ step = numeral[FPlusOne][0]

/\ PrintT(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

```

A domingo, 30 de maio de 2021 à(s) 15:17:29 UTC+1, andrew...@xxxxxxxxx escreveu:

You can pass operators as parameters to operators:apply(op(_,_)) == op(1,2)

f(a, b) == a + b

doApply == apply(f)doApplyLambda == apply(LAMBDA a,b : a + b)You can also pass functions as parameters to other functions, assuming you can define their domain & range as a set:apply[f \in [Nat \X Nat -> Nat]] == f[1, 2]

doApply == apply[[x, y \in Nat |-> (x + y) % 100]]And of course you can pass functions as parameters to operators:apply(f) == f[1, 2]

doApply == apply([x, y \in Nat |-> (x + y) % 100])AndrewOn Sunday, May 30, 2021 at 9:46:13 AM UTC-4 Alex wrote: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 IntegersCONSTANT Limit \* Upper bound limit, that model will be testingASSUME Limit \in Nat \union {0}FPlusOne(n) == n + 1 \* Helper function to convert Church numerals to integersLZero(L) == [s \in L |-> [z \in L |-> z]] \* Zero numeralLSucc(L) == [s \in L |-> [z \in L |-> s[z]]] \* Successor function for generating next Church numeralVARIABLEstep, \* Execution step, ranging from 0 to Limitnumeral \* Church numeral, produced on each stepTypeOK == \* 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 = LZeroSetNext == \* Try up to a "Limit" numbers/\ step < Limit/\ numeral' = LSucc[numeral]/\ step' = step + 1ComputationComplete == \* 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?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/250ce0dc-872a-4b2f-860b-0cc6cf44c98cn%40googlegroups.com.

**Follow-Ups**:

**References**:

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