Each of set theory, higher-order logic (in the tradition of Church's Simple Type Theory, implemented in HOL or Isabelle), and strong type theories as Coq's calculus of inductive constructions has a very different "look and feel".
Looking at just expressiveness (as in flexibility), set theory is certainly stronger than HOL and I believe also than Coq. For example, HOL or Coq do not admit a set like {1, {2,3}}. In fact, the original motivations for type theory were to tame the expressiveness of set theory because it led to paradoxes.
Whether you need that power in practice is a different question. I have rarely felt bothered by the discipline that HOL imposes, and it helps proof automation. At any rate, TLA+ is more expressive than what you might ever need for specifying algorithms.
Stephan
Thank you both Stephan and FL. That Math Exchange link was particularly useful.
So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set (I've read the definition in Specifying Systems). In practice, however, it seems like this can always be avoided, and rather trivially. I have heard people dismiss TLA+ as "not even higher-order (like Coq)", and so less expressive. Similarly, I've heard people say that things like separation logic require higher-orderness, but from what little I've seen of it (which is very little), it also seems to be rather trivially expressed in TLA+. Is there an actual difference in expressiveness or just a formal one?
Ron
--
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.
|