How to define a partial function and add an element to a set of functions in TLA+?

[mlj...@gmail.com]

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

[saksha...@stonybrook.edu]

It seems that it treats [a |-> b] as a record

>> [a |-> b] is a record. Valid access operation on this would be [a |-> b].a (or [a |-> b]["a"]). Note that a is a string here. So [a |-> b]["a"] = [a |-> b].a = b is true.

But my purpose is to add a tuple of (a, b) to the function f

>> This can be done like this: Add(a, b) == f' = [f EXCEPT![a] = b]. This is equivalent to f' = [x \in DOMAIN f |-> IF x = a THEN b ELSE f[x]].

I strongly recommend reading Lamport's Specifying Systems. Chapter 16 covers Functions and Records. Also, if I am not wrong, your TypeOK is incorrect. SUBSET [A -> B] is set of sets of functions in [A -> B]. So, f \subseteq [A -> B] means f is a set of some functions in [A -> B].

Regarding the initial question of defining a partial function, I'm not sure if syntax is available in TLA+ for partial functions, but I could be wrong. The way I specify this is:

CONSTANT None
ASSUME NoneNotInB == None \notin B

Init == f = [x \in A |-> None]
Add(a, b) == f' = [f EXCEPT![a] = b]

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

Or if you do not like None and want to express f as a set then,

Init == f = {}
Add(a, b) == f' = f \cup {[a |-> a, b |-> b]}

TypeOK == f \subseteq [a : A, b : B]


Hope this helps,
Saksham

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

[mlj...@gmail.com]

Thank you for your help. I'm switching from Z to TLA, so still learning the differences between them.

在 2018年1月16日星期二 UTC-5下午4:16:30，saksha...@stonybrook.edu写道：

[mlj...@gmail.com]

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写道：

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

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

--