4 ms·

can even reason about the composition of logics I'm not aware of a fully fledged approach to logical composition that tells me an interesting story about the c

by mafribe 10y ago

can even reason about the composition of logics I'm not aware of a fully fledged approach to logical composition that tells me an interesting story about the combination of logics that arise in computation, I know that people work on this, but as far as I can see, this work is far from finished. Please point to papers if you know more than that. first class continuations As far as I'm aware, Griffin's work, which was a stroke of genius, does not provide a 1-to-1 correspondence between classical proofs and programs. That's why even today, 1/4 of a century later, people work on CH for classical logic.

danharaj 10y ago
It's true that the CH approach to classical logic is by no means exhausted. I see this as a feature of classical logic's rich structure. In any case, I disagree that this is a break down of the CH correspondence. Analyzing the type theories related to classical logic demonstrates to me that the CH correspondence is a gift that keeps on giving. The approach I have in mind about composition of logics is the theory of pseudodistributive laws: http://dl.acm.org/citation.cfm?id=2612113 http://dl.acm.org/citation.cfm?id=2612113 It's kind of cutting edge and has only yet been applied to a few situations, but it seems to be the correct notion of composing type theoretic (and hence logical) structures in compatible ways. Another approach I like that is strictly logical is Nuel Belnap's display logic, which characterizes a ridiculously broad range of logics and proves a general cut elimination theorem for them. The relationship between the categorical approach and the display logic approach is not entirely clear yet. In any case, the CH correspondence is a rich and very active area of research. Just because we haven't nailed it down exactly yet doesn't mean it's broken! Our current understanding is a shadow of a much deeper concept.
- mafribe 10y ago
  The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most forms of computation beyond strongly normalising pure functions. If you are broadening what you mean by CH, then fair enough, but it's shifting the argument.

by mafribe 10y ago

danharaj 10y ago

It's true that the CH approach to classical logic is by no means exhausted. I see this as a feature of classical logic's rich structure. In any case, I disagree that this is a break down of the CH correspondence. Analyzing the type theories related to classical logic demonstrates to me that the CH correspondence is a gift that keeps on giving. The approach I have in mind about composition of logics is the theory of pseudodistributive laws: http://dl.acm.org/citation.cfm?id=2612113 http://dl.acm.org/citation.cfm?id=2612113 It's kind of cutting edge and has only yet been applied to a few situations, but it seems to be the correct notion of composing type theoretic (and hence logical) structures in compatible ways. Another approach I like that is strictly logical is Nuel Belnap's display logic, which characterizes a ridiculously broad range of logics and proves a general cut elimination theorem for them. The relationship between the categorical approach and the display logic approach is not entirely clear yet. In any case, the CH correspondence is a rich and very active area of research. Just because we haven't nailed it down exactly yet doesn't mean it's broken! Our current understanding is a shadow of a much deeper concept.

mafribe 10y ago
The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most forms of computation beyond strongly normalising pure functions. If you are broadening what you mean by CH, then fair enough, but it's shifting the argument.