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..1
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 22, column 5 to line 23, column 22 in chnumerals
1. Line 22, column 8 to line 22, column 15 in chnumerals
2. Line 23, column 8 to line 23, column 22 in chnumerals
3. Line 18, column 5 to line 19, column 35 in chnumerals
4. Line 18, column 8 to line 18, column 34 in chnumerals
5. Line 18, column 15 to line 18, column 34 in chnumerals
6. Line 18, column 15 to line 18, column 31 in chnumerals
7. Line 9, column 30 to line 9, column 64 in chnumerals
8. 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, TLC
CONSTANT Limit \* Upper bound limit, that model will be testing
ASSUME 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 integers
LZero == [s \in [MyNat -> MyNat] |-> [z \in MyNat |-> z]] \* Zero numeral
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]] ]
]
]
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]
/\ PrintT(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>>
```
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.