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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 19 Oct 2020 12:58:54 +0200*References*: <0c1c51bb-e38c-471d-8d74-b95155267750n@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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/C44FB9E1-60FE-4E86-BE63-2B3CAF3D8455%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Functions and Sets***From:*Igor Kim

**References**:**[tlaplus] Functions and Sets***From:*Igor Kim

- Prev by Date:
**[tlaplus] Functions and Sets** - Next by Date:
**Re: [tlaplus] Functions and Sets** - Previous by thread:
**[tlaplus] Functions and Sets** - Next by thread:
**Re: [tlaplus] Functions and Sets** - Index(es):