[solved] sequent calculus as programming language - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T20:13:15Z http://mathoverflow.net/feeds/question/29577 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language [solved] sequent calculus as programming language beroal 2010-06-26T05:31:17Z 2010-07-30T08:10:25Z <p>intuitionistic logic ~ programming</p> <p>natural deduction ~ lambda-calculus</p> <p>Hilbert system ~ combinatory logic {S, K}</p> <p>Gentzen system=sequent calculus ~ ?</p> <p>What would you write in place of the question mark?</p> <p>Update 0: Common mathematical tree notation for proofs is too cumbersome and redundant. I need a language as compact as e.g.:</p> <p><code> data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -} </code></p> <p>Update 1: After following the links suggested by commentators I found this perfectly concrete and accessible article: "Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure." There, "?" language is named "the usual interpretation of LJ cut-free proofs by normal lambda-terms", i.e. is made out of lambda-calculus.</p> http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language/29594#29594 Answer by supercooldave for [solved] sequent calculus as programming language supercooldave 2010-06-26T09:21:58Z 2010-06-28T19:11:49Z <p>To answer your question about representing sequent calculi proofs in a computer, you need to look at the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">Curry-Howard isomorphism</a>. Formula in a sequent are annotated with terms and the sequent calculus for intuitionistic logic resembles the type rules for the typed lambda calculus. If you want to manipulate this, then you need to record the assumptions (left-hand side of the turnstyle $\vdash$), which corresponds to recording the types of free variables. Then the right-hand side is a $\lambda$-term (describing the proof) and its type (the formula proven).</p> <p>There's a vast amount of literature about this. The reference you probably want is <a href="http://pauillac.inria.fr/~herbelin/publis/csl-Her94-lambda-bar.ps.gz" rel="nofollow"><em>A $\lambda$-calculus structure isomorphic to sequent calculus structure</em></a> by Hugo Herbelin. The <a href="http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf" rel="nofollow">book</a> by Morten Heine B. Sørensen and Pawel Urzyczyn is an extensive study of the topic. This kind of encoding is at the heart of proof assistants such as <a href="http://coq.inria.fr/" rel="nofollow">Coq</a>.</p> <p>Other possible correspondences include <strong>Sequent calculus ~ Abstract Machine.</strong> See <em><a href="http://www.cs.indiana.edu/~sabry/papers/sequent.pdf" rel="nofollow">Sequent calculi and abstract machines</a></em> by Zena M. Ariola, Aaron Bohannon, Amr Sabry, ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 31 , Issue 4 (May 2009). Or more generally, and perhaps more loosely, <strong>Sequent calculus ~ Operational Semantics.</strong> You also have <strong>proofs ~ processes</strong>, as explored by <a href="http://www.comlab.ox.ac.uk/files/301/pasp.ps" rel="nofollow">Abramsky</a> and <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.85.9963&amp;rep=rep1&amp;type=pdf" rel="nofollow">Saraswat</a>, the latter in the context of concurrent constraint programming.</p> http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language/29597#29597 Answer by Neel Krishnaswami for [solved] sequent calculus as programming language Neel Krishnaswami 2010-06-26T10:59:19Z 2010-06-26T10:59:19Z <p>There is no single answer to this question, because of the high degree of nondeterminism inherent in the sequent calculus -- to get a computational interpretation, you need to resolve the ambiguity, and each way of doing so leads to different operational interpretations. Furthermore, the answers differ somewhat for classical and intuitionistic sequent calculi. </p> <p>Proof term assignments for classical sequent calculi correspond closely to continuation calculi, such as Herbelin's $\lambda\mu$ calculus. Now continuation transforms correspond to double-negation translations of classical logic into intuitionistic logic, and of there are many different double-negation translations possible. Each choice of double-negation translation gives rise to a different evaluation order, which explains why they are so valuable for the study for abstract machines (as in supercooldave's link) -- you can get the benefits of studying different evaluation orders via CPS transforms, without having to code everything up in functions. </p> <p>Now, you can also try to eliminate the nondeterminism in another way: by fiat. This relies upon Andreoli's idea of <em>focusing</em> for linear logic. In operational terms, the idea is to define logical connectives either in terms of their values, or their elimination forms (this is called <em>polarity</em>). After picking one, the other is determined by the need to satisfy cut-elimination. For linear logic, each of the connectives has unique polarity. For classical logic, every connective can be given either polarity (ie, every connective can be defined either in terms of values or continuations), and the choice of polarities for the connectives essentially determines the evaluation order. This is very well explained in Noam Zeilberger's PhD thesis, <a href="http://www.cs.cmu.edu/~noam/thesis.pdf" rel="nofollow">http://www.cs.cmu.edu/~noam/thesis.pdf</a>. </p> <p>For intuitionistic sequent calculi, the proof term assignments still have a lot of nondeterminism in them. When you resolve this through focalization, you find that the resulting calculi are <em>pattern matching calculi</em>. A beautiful abstract take on this is also in Noam's thesis, and I wrote a very concrete paper about this for POPL 2009, <a href="http://www.cs.cmu.edu/~neelk/pattern-popl09.pdf" rel="nofollow">"Focusing on Pattern Matching"</a>, which showed how to explain Haskell/ML style pattern matching in terms of proof term assignments for focused sequent calculi. </p> http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language/29688#29688 Answer by Noam Zeilberger for [solved] sequent calculus as programming language Noam Zeilberger 2010-06-27T08:38:33Z 2010-06-27T09:00:44Z <p>To add to Neel's response, you can't get a more concrete answer unless you clarify what you mean by "sequent calculus". If you mean Gentzen's original systems LK or LJ, then the answer is simply that there is no independently discovered/motivated computational system. (Remember that Gentzen's original motivation for introducing sequent calculus was as a tool for studying <em>provability</em>, and natural deduction as a tool for studying <em>proofs</em>.) Different operational interpretations have been associated with sequent calculus by departing from these original systems (or just by being satisfied with a looser "correspondence"), but then the questions are 1. whether you can really call these systems "sequent calculus" (what mathematical properties are invariant?), and 2. whether it really matters that you do?</p> <p>On the other hand, there are still many aspects of proofs-as-programs that are not understood---as Neel and supercooldave mentioned, pattern-matching and operational semantics are examples---and people have tried to gain a handle on these by studying <em>ideas</em> from sequent calculus and from refinements of sequent calculus.</p> <p>For example, one important idea from sequent calculus is the "subformula property", that a proof of a formula only needs to mention its subformulas. In natural deduction this property is broken for connectives like disjunction. The connection between focusing proofs and pattern-matching that Neel mentioned can be understood as a way of regaining this normal form property for programs with sum types.</p> http://mathoverflow.net/questions/29577/solved-sequent-calculus-as-programming-language/33810#33810 Answer by RD1 for [solved] sequent calculus as programming language RD1 2010-07-29T17:30:21Z 2010-07-29T17:30:21Z <p>Some additional work on the pattern matching and cut elimination is that of Cerrito and Kesner:</p> <p><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.8703&amp;rep=rep1&amp;type=pdf" rel="nofollow">http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.54.8703&amp;rep=rep1&amp;type=pdf</a></p> <p>The work by Noam gives a more complete view though.</p> <p>I often think of the situation as that there's clear and strong relationship, but (so far) we don't have a concrete syntax that works out as well as C-H does for introduction and elimination rules in natural deduction.</p>