4
$\begingroup$

What is the precise connection between:

  • strong normalization of the simply typed $\lambda$-calculus, and

  • cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent calculus” form?

Does either follow from the other? Does each follow from the other? (Do they have the same computational complexity and/or arithmetic strength?)

I can vaguely see that, under the Curry-Howard correspondence, a redex $(\lambda (v:\sigma).E)T$ will translate to a natural deduction style proof with $\rightarrow$ introduction immediately followed by $\rightarrow$ elimination, which becomes a cut proof in sequent calculus, whose immediate elimination should correspond to the reduct $E[v := T]$. So certainly there should be some connection. The precise details escape me, however, in particular because terms in the s.t.$\lambda$.c. correspond to natural deduction proofs whereas cut elimination takes place at the sequent calculus level (there are three things in correspondence: a $\lambda$-term, a natural deduction proof and a sequent calculus proof, and I'm not sure what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points at the “$\lambda$-calculs” and “sequent calculus” levels).

I'm sure this is very standard: is there a textbook that explains this, hopefully in a pleasant way?

Improve this question
$\endgroup$
2
  • $\begingroup$ Maybe sections 3.4, 3.5 and 3.6 of Proofs and Types (paultaylor.eu/stable/prot.pdf) can help. It takes place in a slightly broader setting, where there are three kinds of redexes. $\endgroup$
    – sparusaurata
    Nov 16 at 22:37
  • 2
    $\begingroup$ Concerning "what the correct statement at the “natural deduction” level should be that corresponds to the two bullet points", the usual keyword is "detour elimination". $\endgroup$
    – Lê Thành Dũng Nguyễn
    Nov 17 at 9:34

1 Answer 1

Reset to default
2
$\begingroup$

  1. How “standard” is it? A post by Anupam Das on the proof theory blog attacks the folklore by comparing the following two results:

    Proposition 1 (Folklore). For any theorem A of IPL, we can compute a cut-free LJ proof of A in exponential time and polynomial space in |A|.

    Theorem 3 (Statman ’79). Deciding whether two simply typed $\lambda$-terms reduce to the same normal form is not elementary recursive.

    He then remarks:

    [...] Statman’s result does not imply any lower bounds on the complexity of cut-elimination for LJ, since normalisation of $\lambda$-terms constitutes just one particular strategy for cut-elimination. Note in particular, that both Proposition 1 and Theorem 3 are perfectly consistent with each other.

  2. Nevertheless, let me mention two works in this direction that help clarify the link. Consistently with the previous remark, they assume a strategy corresponding to the negative polarisation of logic (corresponding to call-by-name reduction in the λ-calculus). But even with this assumption the result is deeper than it looks, relating global transformations (substitution) with local ones (from cut-elimination).

    Additional references can be found in their bibliography. Some discussion about this correspondence is also found at the end of Chapter 6 in the following textbook:

Improve this answer
$\endgroup$
2
  • $\begingroup$ OK, this is probably stupid, but: if we take a $\lambda$-term, interpret it as a natural deduction proof, convert the latter to a sequent proof, eliminate cuts in the latter, and convert it back to a natural deduction proof and then $\lambda$-term… what goes wrong? From the difference in complexity we can't expect to get a normal form so easily, so what do we get? $\endgroup$
    – Gro-Tsen
    Nov 17 at 21:44
  • 1
    $\begingroup$ Cut-elimination being stated in terms of proving the same sequent, there is no requirement of preserving any notion of meaning of proofs. For instance, a cut-elimination procedure returning $K_*=\lambda x\lambda yy$ when the input is βη-equivalent to $K=\lambda x\lambda yx$ would be allowed. (The blog post mentions more subtle cut-elimination procedures, which are "local" in a certain sense.) $\endgroup$
    – gadmm
    Nov 18 at 14:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.