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

Re: [tlaplus] TLA+ logic

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.


On 04 Dec 2015, at 16:24, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

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?


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.