[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Functions and Sets



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>> }.


On 19 Oct 2020, at 12:43, Igor Kim <biosckon@xxxxxxxxx> wrote:

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!



 

--
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/0c1c51bb-e38c-471d-8d74-b95155267750n%40googlegroups.com.

--
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/C44FB9E1-60FE-4E86-BE63-2B3CAF3D8455%40gmail.com.