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

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

/\ 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.