4 ms·

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence break

by mafribe 10y ago

programming languages and formal logics are ultimately instances of the same general idea. That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either. It seems to me that constructive proofs are a special class of programs, and fall under the purview of programming language, but not the other way around.

tikhonj 10y ago
The point is that they're both formal systems of reasoning, not that they have exactly the same properties. The techniques and abstractions from both PL and formal logic often generalize well to both.
- mafribe 10y ago
  Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.
mkehrt 10y ago
Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A. There's some connection between classical logics and concurrency, though it's hard to get at. You can use callcc to implement threads, and Getzen's classical sequent calculus has multiple conclusions. Here is a PHD thesis that uses modal logic to model distributed code in a CH fashion: http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-code.pdf http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-co... Classical logic is perfectly modeled with callcc, which has the type Peirce's Law, and allows one to write terms with the types of the law of excluded middle or Double Negation Elimination.
- mafribe 10y ago
  Non termination is modeled as false: That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) about non-terminating computation. The T. Murphy PhD doesn't deal with distribution because it lacks the key feature of distribution which is partial failure. As far as I'm aware the work on modelling double negation by call/cc doesn't actually provide a 1-to-1 correspondence between programs and proofs. I've forgotten the details but I think only some programs come out being proofs.
danharaj 10y ago
> The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. No it doesn't. Each of those features leads to a different logic. You can even reason about the composition of logics via category theory to see how various features interact with each other. > Classical logic doesn't really have wholly convincing CH-correspondences either. Sure it does, first class continuations: http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf I suppose you have the right to remain unconvinced.
- 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.

by mafribe 10y ago

tikhonj 10y ago

The point is that they're both formal systems of reasoning, not that they have exactly the same properties. The techniques and abstractions from both PL and formal logic often generalize well to both.

mafribe 10y ago
Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.

mkehrt 10y ago

Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A. There's some connection between classical logics and concurrency, though it's hard to get at. You can use callcc to implement threads, and Getzen's classical sequent calculus has multiple conclusions. Here is a PHD thesis that uses modal logic to model distributed code in a CH fashion: http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-code.pdf http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-co... Classical logic is perfectly modeled with callcc, which has the type Peirce's Law, and allows one to write terms with the types of the law of excluded middle or Double Negation Elimination.

mafribe 10y ago
Non termination is modeled as false: That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) about non-terminating computation. The T. Murphy PhD doesn't deal with distribution because it lacks the key feature of distribution which is partial failure. As far as I'm aware the work on modelling double negation by call/cc doesn't actually provide a 1-to-1 correspondence between programs and proofs. I've forgotten the details but I think only some programs come out being proofs.

danharaj 10y ago

> The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. No it doesn't. Each of those features leads to a different logic. You can even reason about the composition of logics via category theory to see how various features interact with each other. > Classical logic doesn't really have wholly convincing CH-correspondences either. Sure it does, first class continuations: http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf I suppose you have the right to remain unconvinced.

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.