Small correction - in the spec above `MyInt` should read as `MyNat`.On Sunday, May 30, 2021 at 4:41:29 PM UTC-7 Alex wrote:Thank you for finding time to respond.I'm not sure though I understand how the above can work out. Model verification for Limit=1 yields```The first argument of >= should be an integer, but instead it is:0..1The error occurred when TLC was evaluating the nestedexpressions at the following positions:0. Line 22, column 5 to line 23, column 22 in chnumerals1. Line 22, column 8 to line 22, column 15 in chnumerals2. Line 23, column 8 to line 23, column 22 in chnumerals3. Line 18, column 5 to line 19, column 35 in chnumerals4. Line 18, column 8 to line 18, column 34 in chnumerals5. Line 18, column 15 to line 18, column 34 in chnumerals6. Line 18, column 15 to line 18, column 31 in chnumerals7. Line 9, column 30 to line 9, column 64 in chnumerals8. Line 9, column 33 to line 9, column 42 in chnumerals```and it also gives warnings about SetNext - `SetNext is never enabled` and the same for ComputationComplete.I see that in my spec I made a mistake of passing L as a set, it seems it better be defined a parameter instead.In Church encoding `succ` function is defined as follows:```succ = λ n . λ s . λ z . s (n s z)```so, in order to make it work successor function must be extended with one more argument. It seems plausible that the type of argument `s` could be [MyNat -> MyNat] (a function taking a number and returning a number `0..Limit`) and a type of `z` could be just `MyNat`.Recalling definition of any n-th Church numeral (number of s invocations in the functions body equals to the integer that numeral corresponds to):```Cn = λ s . λ z . s (s ... (s z))) - n invocations of s```so given definition in the spec the type of Church numeral should rather be [MyInt -> MyInt] -> [MyInt -> MyInt] - lets call it ChurchT for brevity, as a signature of "reduceable" church numeral could be represented as follows, argument type highlighted in yellow:```Cn = λ s : (integer -> integer) . λ z : integer . s (s ... (s z))) - n invocations of s```So in order to make it work only one missing piece remains - define a proper type for argument `n`.But we know that successor function takes a Church numeral and returns back Church numeral, so given this its definition should be `ChurchT -> ChurchT` or, in other words```[[[MyInt -> MyInt] -> [MyInt -> MyInt]]->[[MyInt -> MyInt] -> [MyInt -> MyInt]]]```attempt to define this as```LSucc == \* Successor function for generating next Church numeral[n \in [[[MyInt -> MyInt] -> [MyInt -> MyInt]] -> [[MyInt -> MyInt] -> [MyInt -> MyInt]]] |->[s \in [MyNat -> MyNat] |->[z \in MyNat |-> s[n[s][z]] ]]]```yields the following warning:```Unknown operator: `MyInt'.```So, it brings the following questions:* Is it possible to have a some sort of type aliasing for function declarations? I.e. is it possible to somehow define `ChurchT` type?* How can type of argument n could be fixed in the declaration of LSucc?My full spec now looks as follows:```EXTENDS Integers, TLCCONSTANT Limit \* Upper bound limit, that model will be testingASSUME Limit \in Nat \union {0}MyNat == {0..Limit}FPlusOne == [x \in MyNat |-> IF x >= Limit THEN Limit ELSE x + 1] \* Helper function to convert Church numerals to integersLZero == [s \in [MyNat -> MyNat] |-> [z \in MyNat |-> z]] \* Zero numeralLSucc == \* Successor function for generating next Church numeral[n \in [[[MyInt -> MyInt] -> [MyInt -> MyInt]] -> [[MyInt -> MyInt] -> [MyInt -> MyInt]]] |->[s \in [MyNat -> MyNat] |->[z \in MyNat |-> s[n[s][z]] ]]]VARIABLEstep, \* 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]/\ PrintT(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>>```I'm verifying this using a model referring to a `Limit <- 1`.For what it is worth behavior spec is set to `Initial predicate and next-state relation` both set to `Init` and `Next` correspondingly with `TypeOK` referred as invariant.On Sunday, May 30, 2021 at 8:41:12 AM UTC-7 Afonso Fernandes wrote:Here is my try of writing the specification of Church numerals, adapted from the one you posted:```EXTENDS Integers, TLCCONSTANT Limit \* Upper bound limit, that model will be testingASSUME Limit \in Nat \union {0}VARIABLEstep, \* Execution step, ranging from 0 to Limitnumeral \* Church numeral, produced on each stepMyNat == 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 integersLZero == [f \in [MyNat -> MyNat] |-> [x \in MyNat |-> x] ] \* Zero numeralLSucc(L) == [f \in [MyNat -> MyNat] |-> [x \in MyNat |-> f[L[f][x]] ] ] \* Successor function for generating next Church numeralTypeOK == \* 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 = 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```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.