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