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



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. 
A segunda-feira, 31 de maio de 2021 à(s) 00:43:03 UTC+1, Alex escreveu:
Small correction - in the spec above `MyInt` should read as `MyNat`.

On Sunday, May 30, 2021 at 4:41:29 PM UTC-7 Alex wrote:
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.

On Sunday, May 30, 2021 at 8:41:12 AM UTC-7 Afonso Fernandes wrote:
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
```

A domingo, 30 de maio de 2021 à(s) 15:17:29 UTC+1, andrew...@xxxxxxxxx escreveu:
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

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

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.

--
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/df1dafdf-0126-48fb-b1d5-b4de630de23dn%40googlegroups.com.