[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?

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


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 [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

    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/96f53a07-fec9-4790-a1b1-850334fcdfbdn%40googlegroups.com.