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

# [tlaplus] Re: How to pass a function as an argument to the other function?

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]
/\ PrintT(numeral[FPlusOne])

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])

Andrew

On 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 .

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. 

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]

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?

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: