How to pass a function as an argument to the other function?

84 views
Skip to first unread message

Alex

unread,
May 30, 2021, 9:46:13 AM5/30/21
to tlaplus
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]

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.

Andrew Helwer

unread,
May 30, 2021, 10:17:29 AM5/30/21
to tlaplus
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

Afonso Fernandes

unread,
May 30, 2021, 11:41:12 AM5/30/21
to tlaplus
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][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
```

Alex

unread,
May 30, 2021, 7:41:29 PM5/30/21
to tlaplus
Thank you for finding time to respond.

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.

Alex

unread,
May 30, 2021, 7:43:03 PM5/30/21
to tlaplus
Small correction - in the spec above `MyInt` should read as `MyNat`.

Afonso Fernandes

unread,
May 31, 2021, 6:26:14 AM5/31/21
to tlaplus
To make it easier to read we can define these three sets
```
SetOfAllFunctions == {FPlusOne} \* this functions must all have the same domain and image set (T -> T)
SetOfAllArguments == MyNat \* must be in the domain of T
SetOfAllChurchNumbers == [SetOfAllFunctions -> [SetOfAllArguments -> SetOfAllArguments]]
``` 
This also makes it more efficient because the set of functions is smaller

From there, we can write LZero and LSucc as:
```
LZero == [f \in SetOfAllFunctions |-> [x \in SetOfAllArguments |-> x]] \* Zero numeral
LSucc == \* Successor function for generating next Church numeral
    [n \in SetOfAllChurchNumbers |->
        [f \in SetOfAllFunctions |-> [x \in SetOfAllArguments |-> f[n[f][x]]] ]
    ]
```
This gives the correct numbers in the typeok, I tested it with a limit of 5

On your questions, I think TLA+ is not typed so, using the TLA+ tools, I don't know if there is a way to enforce types (beyond adding enabling conditions on the arguments to be in certain set).
However, you can use something like https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html to write type annotations and enforce type on the declarations. 

Michael Leuschel

unread,
May 31, 2021, 10:06:19 AM5/31/21
to tla...@googlegroups.com
Hi,

>
> On 31 May 2021, at 01:41, Alex <vstr...@gmail.com> wrote:
>
>
> ```
> The first argument of >= should be an integer, but instead it is:
>


I think in your spec it should be
MyNat == 0..Limit
instead of
MyNat == {0..Limit}

In CSP/FDR you write {a..b} for the interval from a to b, but in TLA+/B this is a singleton set containing an interval.

However, even after that correction there is a type error in your construction (s[n[s][z]]).

Greetings,
Michael

Alex

unread,
Jun 1, 2021, 10:02:42 PM6/1/21
to tlaplus
Thanks a lot guys! For someone who interested here is the complete spec that verifies successor function behavior:

```
EXTENDS Integers, TLC

CONSTANT Limit \* Upper bound limit, that model will be testing
ASSUME Limit \in Nat

IntRange == 0..Limit

FPlusOne == [x \in IntRange |-> IF x >= Limit THEN Limit ELSE x + 1] \* Helper function to convert Church numerals to integers
ReducerFunctions == {FPlusOne} \* this functions must all have the same domain and image set (T -> T)
ReducerArguments == IntRange \* must be in the domain of T
ChurchNumbers == [ReducerFunctions -> [ReducerArguments -> ReducerArguments]]

LZero == [f \in ReducerFunctions |-> [x \in ReducerArguments |-> x]] \* Zero numeral
LSucc == \* Successor function for generating next Church numeral
    [n \in ChurchNumbers |->
        [f \in ReducerFunctions |-> [x \in ReducerArguments |-> f[n[f][x]]] ]
    ]

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(<<"Reduced Church Numeral", 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>>
```
Reply all
Reply to author
Forward
0 new messages