| 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C44FB9E1-60FE-4E86-BE63-2B3CAF3D8455%40gmail.com. |