Re: [tlaplus] Re: How to define a partial function and add an element to a set of functions in TLA+?

The most significant difference between functions in Z or B and in TLA+ lies in the fact that TLA+ is untyped. In the absence of types, I don't know what a partial function would be or why it would be useful.

Leslie

On Wednesday, January 17, 2018 at 12:49:14 AM UTC-8, Stephan Merz wrote:

Hello,

one of the differences between the set theories underlying Z (or B / Event-B) and TLA+ lies in the representation of functions. In TLA+, functions are primitive (i.e., not defined as sets of pairs), they always total, and they have an explicit domain. In your original posting you said that you want to represent a partial function f from A to B. There are two ways to do so in TLA+:

1. As suggested by Saksham, represent f as a total function from A to B \cup {None} with a null value None. In order to test if f is defined for some a \in A, you write f[a] # None.

2. Represent f as a function from a subset of A to B. The operator

PFun(S,T) == UNION { [ AS -> T ] : AS \in SUBSET S }

defines the set of partial functions in this representation. Your operators can then be written as follows

TypeOK == f \in PFun(A,B)
Init == f = [x \in {} |-> {}]
Add(a,b) == f' = (a :> b) @@ f \* need to EXTEND TLC

Note that in the definition of Init, the value on the right-hand side of the arrow is irrelevant (you could also use some value of B, perhaps write CHOOSE b \in B : TRUE). Because the function with empty domain also represents the empty sequence, you can alternatively write

Init == f = << >>

but this is perhaps a little obscure. The operators :> and @@ that appear in the definition of Add are defined in the TLC module. In this approach, you write

a \in DOMAIN f

in order to test if the function is defined for a.

Which of the two approaches you prefer depends on taste and sometimes on how TLC evaluates expressions: you don't want TLC to enumerate the set PFun(A,B), although testing if f \in PFun(A,B) holds (as in evaluating the typing invariant) is fine.

Regards,
Stephan

On 16 Jan 2018, at 22:53, mljzcj wrote:

Now, I understand that I should use \in instead of \subseteq in TypeOK. Declaring a Null value will solve my question, but I still feel a little bit strange.

In Z, we often use partial functions and define an "Add" function to add new elements. But it looks like we should use total functions and update values in functions in TLA+.

在 2018年1月16日星期二 UTC-5下午4:20:14，Andrew Helwer写道：
You are correct that functions can be represented as sets of tuples, but in TLA+ they are instead represented as a record. The two representations are equivalent. Use this syntax to define f on a new input value:

Add(a, b) == f' = [f EXCEPT ![a] = b]

Unfortunately, this makes your TypeOK a bit weird - your function f does not start off as a member of the set [A -> B]. You should define a Null value as follows:

Null == CHOOSE b : b \notin B

TypeOK == f \in [A -> B \cup {Null}]

Init == f = [a \in A |-> Null]

On Tuesday, January 16, 2018 at 11:43:45 AM UTC-8, mlj... wrote:
Hi guys,
I've met some problems of function definitions. For instance, in math, I've got two sets A and B; and I'd like to define a partial function f as A -|-> B. Also, I want to define an operation that adding an element to the set, like f' = f \cup {(a, b)}, where a \in A and b \in B.
So in TLA+, I tried to write the spec like:
CONSTANT A, B
VARIABLES f
TypeOK == f \subseteq [A -> B]
Init == f = {}
Add(a, b) == f' = f \cup {[a |-> b]}
Next == \E a \in A, b \in B : Add(a, b)
However, I got errors when running model checking in TLC. It seems that it treats [a |-> b] as a record. But my purpose is to add a tuple of (a, b) to the function f, where f should be a set of tuples as it defined in math, like {(a1, b1), (a2, b2)}.
So how can I write it in TLA+?
Best Regards,
Changjian Zhang

--