Functions and Sets

52 views
Skip to first unread message

Igor Kim

unread,
Oct 19, 2020, 6:43:22 AM10/19/20
to tlaplus
Clarifying my fundamental (mis-)understanding :) 

[ {0, 1} -> {2, 3} ] \* set of functions. evaluates to:

{ (0 :> 2 @@ 1 :> 2),
  (0 :> 2 @@ 1 :> 3),
  (0 :> 3 @@ 1 :> 2),
  (0 :> 3 @@ 1 :> 3) }

(0 :> 2 @@ 1 :> 2) \* is a function from the set above

(0 :> 2 @@ 1 :> 2) \in [ {0, 1} -> {2, 3} ] \* evals to TRUE

(0 :> 2 @@ 1 :> 2)[1] \* evaluates to 2

<<3,2,1>>[1] \* sequence/ tuple is a function so this evals to 3

So far makes sense.

Now...

(0 :> 2 @@ 1 :> 2) \* What is function? 

I am under impression that function is set of one-to-one relations. Which it does look like. So it is a set, but not a proper TLA+ set? E.g. I cannot do this:

SUBSET (0 :> 2 @@ 1 :> 2)

Thank you!



 

Stephan Merz

unread,
Oct 19, 2020, 6:59:01 AM10/19/20
to tla...@googlegroups.com
Hello,

every value of TLA+ is a set, but for some values we do not know which set they correspond to. For example, we do not know which set the number 42 denotes [1]. It is better to think of such values as being primitive, and that's the case of functions.

For example,

[ {0,1} -> {2,3} ]

is a *set* of functions, and it consists of the functions that you enumerate. But,

(0 :> 2) @@ (1 :>2)

is a single function, it could also be written as

[i \in 0..1 |-> 2]

but we don't know which set this function denotes [2]. Therefore,

SUBSET (0 :> 2) @@ (1 :>2)

is a well-formed expression, but we cannot enumerate its elements, and TLC refuses to evaluate the expression, as you noticed.

Stephan

[1] Traditional presentations of ZF set theory define 0 == {} and Suc(x) == x \cup {x}, but TLA+ uses a CHOOSE expression to define the set of natural numbers as some set satisfying the Peano axioms, see chapter 18.4 of Specifying Systems. The standard definition yields one such set, but there are other models as well.

[2] Again, standard presentations of ZF set theory, as well as the Z and B methods, represent functions as sets of pairs. In TLA+, functions are primitive and pairs are an instance of functions (with domain {1,2}). In particular, you cannot assume that (0 :> 2 @@ 1 :> 2) equals { <<0,2>>, <<1,2>> }.


--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0c1c51bb-e38c-471d-8d74-b95155267750n%40googlegroups.com.

Igor Kim

unread,
Oct 19, 2020, 7:41:56 AM10/19/20
to tlaplus
Thank you Stephan, got it  single function is a primitive.
Reply all
Reply to author
Forward
0 new messages