In TLA+, tuples and sequences are functions. However, unlike in conventional presentations of ZF set theory, functions are not defined as relations (sets of pairs) but are primitive values, axiomatized by
IsAFcn(f) == f = [x \in DOMAIN f |-> f[x]]
See also Section 16.1.7 of "Specifying Systems".
In particular, << >> = { } is not provable in TLA+, nor is its negation.
Best regards,
Stephan Merz
Sometimes the mathematics behind TLA+ puzzle me. For instance in TLA+ it is possible to prove that ASSUME NEW A PROVE << >> = [ x \in { } |-> A ] So DOMAIN << >> = { } and << >> is a function. If << >> is a function then << >> is a relation. But if << >> is a function and DOMAIN << >> = { } then << >> = { } But I can't prove << >> = { } with TLA+. Why ? -- FL
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|