A λ-calculus structure isomorphic to sequent calculus structure DRAFT

Hugo Herbelin ^{∗} LITP-University Paris 7 & INRIA

April 4, 1996

Abstract

This paper is in three parts.

In the first part, we consider a λ-calculus for which applicative terms have no longer the form (...((u u_{1}) u_{2})... u_{n}) but the form (u [u_{1}; ...; u_{n}]), for which [u_{1}; ...; u_{n}] is a list of terms. While the structure of the usual λ-calculus is isomorphic to the structure of natural deduction, this new structure is isomorphic to the structure of sequent calculus.

To express this isomorphism, we do not consider LJ, but a calculus LJT which leads to restrict the notion of cut-free proofs in LJ. We need also to explicitly consider, in a simply typed version of this λcalculus, a substitution operator and a list concatenation operator. By this way, each elementary step of of cut-elimination exactly matches with a β-reduction, a substitution propagation step or a concatenation computation step.

In the second part, we extend the isomorphism to classical logic by considering the μ operator of the λμ-calculus. A version with the operator C of Felleisen is also described.

In the third part, we consider various extensions of the isomorphism (especially to pair, projections and split operator facing conjunction, to injection and case operator facing disjunction). A version with De Bruijn indices of the classical version of the calculus is also described.

∗Internet author’s address: Hugo.Herbelin@inria.fr.

This research was partly supported by ESPRIT Basic Research Action “Types for Proofs and Programs”

Part I

The minimal isomorphism

1 Introduction

1.1 Informal introduction

Zucker [16] and Pottinger [12] have studied the relations between normalisation in natural deduction and cutelimination in the minimal fragment of sequent calculus (otherwise said, they have compared normalisation in simply-typed λ-calculus and cut-elimination). They were considering normalisation without paying special attention to the computational cost of the substitution of a proof in place of an hypothesis. But in sequent calculus, among the different uses of the cut rule, there is one which stands for an explicit operator of substitution and among the elementary rules for cut-elimination, there are rules to compute the propagation of substitution. Therefore, Zucker and Pottinger were led to consider proofs up to the equivalence generated by these substitution propagation computation rules.

Here, we consider a λ-calculus with an explicit operator of substitution and with appropriated substitution propagation rules. This allows to have a more precise correspondance with the elementary rules for cutelimination. However, there are two problems. The first one is that several cut-free proofs of the minimal fragment of sequent calculus are associated to the same normal λ-terms. Then, a solution is to consider rather a restricted version, called LJT, of the sequent calculus. A second problem is that sequent calculus and λ-calculus (or natural deduction) have not the same structure. Then we describe an alternative syntax for λ-calculus of which, this time, the simply-typed fragment is isomorphic to LJT.

1.2 The usual interpretation of LJ cut-free proofs by normal λ-terms

We consider the minimal cut-free fragment of LJ with the implication as sole connective. There is a standard way to interpret cut-free proofs as λ-terms, see for instance Prawitz [13] or, for a more formal presentation, Zucker [16], Pottinger [12] or Mints [10].

Γ, x:A ⊢ x:A Ax  {Γ, x:A, y:A ⊢ u:C \atop Γ, x:A ⊢ u\{y := x\}:C} Cont

\begin{matrix}Γ, ⊢ u:A & Γ, y:B ⊢ v:C \\ Γ, x:A→B ⊢ v\{y := (x u)\}:C \end{matrix} Imp_{L}  {Γ, x:A ⊢ u:B \atop Γ ⊢ λx.u:A→B} Imp_{R}

for which v{x := u} denotes the term v in which each occurrence of x has been replaced by u.

1.3 Towards the calculus LJT

However different proofs may be associated to the same λ-term. For instance:

\begin{matrix}A, C ⊢ A Ax & A, C, B ⊢ B Ax \\ A→B, A, C ⊢ B \end{matrix} ; Imp_{L} ; A→B, A ⊢ C →B ; Imp_{R}

and

\begin{matrix}A ⊢ A Ax & \begin{matrix}A, C, B ⊢ B & Ax \\ A, B ⊢ C →B \end{matrix} ; Imp_{R} \\ A→B, A ⊢ C →B \end{matrix} ; Imp_{L}

are both associated to the λ-term λz.(x y):C →B for a context in which z:C, x:A→B and y:A.

We decide to restrict LJ in order to have a bijective correspondence between normal λ-terms and cut-free proofs. Especially, we decide to forbid the second proof above. The cut-free calculus defined by the following rules, for which sequents have the form Γ; ⊢ A or Γ; A ⊢ B, achieves this requirement:

Γ; A ⊢ A Ax  {Γ, A; A ⊢ B \atop Γ, A; ⊢ B} Cont

\begin{matrix}Γ; ⊢ A & Γ; B ⊢ C \\ Γ; A→B ⊢ C \end{matrix} Imp_{L}  {Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R}

The “;” delimits a place on its right. This place may be either empty or filled with one formula. This kind of constraint comes from Girard who called this special place “stoup”. This calculus has been also considered in Danos et al [2] in which it appears as the intuitionistic fragment of LKT, a classical sequent calculus defined for its good behaviour w.r.t. embedding into linear logic. From now, we call cut-free LJT this calculus. LJT appears also as a fragment of ILU, the intuitionistic neutral fragment of unified logic described by Girard in [6]. ILU is itself a form of LJ constrained with a stoup, for which Girard pointed out that “the formula [in the stoup] (if there is one) is the analogue of the familiar head-variable for typed λ-calculi”. We show in section 1.5 how to embed LJ in LJT.

The cut-free LJT enjoys the property that its proofs are in one-to-one correspondence with the normal simply-typed λ-terms. For instance, a normal term of the form λx_{1}...λx_{n}.(y u_{1} ...u_{n}) and of type A_{1} →...→ A_{n} →B, in which y is of type D = C_{1} →...→C_{p} →B, is unambiguously associated to the proof

\begin{matrix}Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}}; ⊢ u_{1} :C_{1} & \begin{matrix}Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}}; ⊢ u_{p}:C_{p} & Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}}; y:B ⊢ y:B Ax \\ Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}}; y_{p}:C_{p} →B ⊢ (y_{n} u_{n}):B \end{matrix} ; Imp_{L} ; ⋮ . ; Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}}; y_{2} :C_{2} →...→C_{p} →B ⊢ (y_{2} u_{2} ...u_{n}):B \\ Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}} ; y_{1} :D ⊢  (y_{1} u_{1} ...u_{n}):B \end{matrix} ; Imp_{L} ; Γ, y:D, \overrightarrow{x_{1..n}:A_{1..n}} ;  ⊢  (y u_{1} ...u_{n}):B ; Cont
Γ, y:D, \overrightarrow{x_{1..n−1} :A_{1..n−1}};  ⊢  λx_{n}.(y u_{1} ...u_{n}):A_{n} →B Imp^{R}
⋮ .
Γ, y:D, x_{1} :A_{1}  ;  ⊢ λx_{2}...λx_{n}.(y u_{1} ...u_{n}):A_{2} →...→A_{n} →B
Γ, y:D  ;  ⊢ λx_{1}...λx_{n}.(y u_{1} ...u_{n}):A_{1} →...→A_{n} →B Imp^{R}

Remark: The construction of the applicative part of the term starts from u_{n} and ends with u_{1} in contrast with the usual way of building a term (u u_{1} ... u_{n}) in λ-calculus. This is the motivation for introducing the \overline{λ}-calculus.

1.4 Cut and reduction rules: towards the \overline{λ}-calculus

According to the place of the cut formula (in the stoup or not), there are two kinds of cut rules in LJT:

head-cut rule  mid-cut rule
\begin{matrix}Γ; Π ⊢ A & Γ; A ⊢ B \\ Γ; Π ⊢ B \end{matrix} Cut_{H} \begin{matrix}Γ; ⊢ A & Γ, A; Π ⊢ B \\ Γ; Π ⊢ B \end{matrix} Cut_{M}

for which Π means one or zero formula in the stoup.

The mid-cut rule is naturally interpreted as an operator of explicit substitution :

\begin{matrix}Γ; ⊢ v:A & Γ, x:A; Π ⊢ u:B \\ Γ; Π ⊢ u[x := v]:B \end{matrix} Cut_{M}

A standard way to eliminate cuts is to apply rewriting rules to proofs in order to propagate the cuts towards smaller proofs. Here is an example of such a rewriting rule :

\begin{aligned}Γ; ⊢ v:A & \begin{matrix}Γ, x:A; ⊢ u_{1} : A_{1} & Γ, x:A; y:A_{2} →...→A_{n} →B ⊢ (y u_{2} ... u_{n}):B \\ Γ, x:A; y:A_{1} →...→A_{n} →B ⊢ (y u_{1} ... u_{n}):B \end{matrix} Imp_{L} \\ & Γ; y:A_{1} →...→A_{n} →B ⊢ (y u_{1} ... u_{n})[x := v]:B \end{aligned} ; Cut_{M}

reduces to

\begin{matrix}\begin{matrix}Γ; ⊢ v:A & Γ, x:A; ⊢ u_{1} : A_{1} \\ Γ; ⊢ u_{1}[x := v]:A_{1} \end{matrix} Cut_{M} & \begin{matrix}Γ; ⊢ v:A & Γ, x:A; y:A_{2} →...→A_{n} →B ⊢ (y u_{2} ... u_{n}):B \\ Γ; y:A_{2} →...→A_{n} →B ⊢ (y u_{2} ... u_{n})[x := v]:B \end{matrix} Cut_{M} \\ Γ; y:A_{1} →...→A_{n} →B ⊢ (y u_{1}[x := v] ... u_{n})[x := v]:B \end{matrix} ; Imp_{L}

It seems “natural” that such a rewriting rule is in correspondence with a rule of substitution propagation. But it is not the case. Indeed it corresponds to the reduction of (y u_{1} ... u_{n})[x := v] into (y u_{1}[x := v] ... u_{n})[x := v] while we would like to get ((y u_{1} ...u_{n−1})[x := v] u_{n}[x := v]).

This is because the structure of a proof in sequent calculus is different from the structure of the associated λ-term and this suggests to consider an alternative formalism for the λ-calculus in which an applicative term is no longer of the form ((u u_{1})...u_{n}), but of the form (u [u_{1}; ...; u_{n}]), i.e. considered as the application of a function to the list of its arguments. We call \overline{λ}-calculus this alternative formalism for λ-calculus.

1.5 Digression: how to recover LJ ?

LJT is as strengthful as LJ since proofs of a sequent Γ ⊢ A in LJ can be compositionnally translated into a proof of Γ; ⊢ A in LJT. The translation is as follows:

Γ, A ⊢ A Ax  is translated by  \begin{matrix}Γ, A; A ⊢ A & Ax \\ Γ, A; ⊢ A \end{matrix} ; Cont

⋮ . ; Γ, A, A ⊢ B ; Γ, A ⊢ B Cont  is translated by  \begin{matrix}\begin{matrix}Γ, A; A ⊢ A & Ax \\ Γ, A; ⊢ A \end{matrix} ; Cont & ⋮ . ; Γ, A, A; ⊢ B \\ Γ, A; ⊢ B \end{matrix} Cut_{M}

\begin{matrix}⋮ . ; Γ ⊢ A & ⋮ . ; Γ, B ⊢ C \\ Γ, A→B ⊢ C \end{matrix} Imp^{L}  is translated by  \begin{matrix}\begin{matrix}⋮ . ; Γ, A→B; ⊢ A & Γ, A→B; B ⊢ B Ax \\ Γ, A→B; A→B ⊢ B \end{matrix} ; Imp_{L} ; Γ, A→B; ⊢ B ; Cont & ⋮ . ; Γ, A→B, B; ⊢ C \\ Γ, A→B; ⊢ C \end{matrix} Cut_{M}

for which the formula A→B is added to each sequent occurring in the proofs of Γ ⊢ A and of Γ, B ⊢ C.

⋮ . ; Γ, A ⊢ B ; Γ ⊢ A→B Imp_{R}  is translated by  ⋮ . ; Γ, A; ⊢ B ; Γ; ⊢ A→B Imp^{R}

\begin{matrix}⋮ . ; Γ ⊢ A & ⋮ . ; Γ, A ⊢ B \\ Γ ⊢ B \end{matrix} Cut  is translated by  \begin{matrix}⋮ . ; Γ; ⊢ A & ⋮ . ; Γ, A; ⊢ B \\ Γ; ⊢ B \end{matrix} Cut^{M}

Thus we have an interpretation of LJ into LJT. However, following this interpretation, cut-free proofs in LJ may no more be cut-free in LJT.

2 The \overline{λ}-calculus

2.1 The \overline{λ}-expressions

There is two kinds of \overline{λ}-expressions: the \overline{λ}-terms and the lists of \overline{λ}-terms (= list of arguments). Both are mutually dependent.

We assume the existence of an infinite set V of which the elements are called term variables names and here denoted by the letters x, y, z, ...

Definition 1 The set of \overline{λ}-expressions, including the \overline{λ}-terms (or shortly terms) and the lists of arguments are mutually defined by the following grammar for which x ranges over V

Terms:  t ::= (x l) | (λx.t) | (t l) | (t[x := t])
Argument lists: l ::= [ ] | [t :: l] | (l @ l) | l[x := t]

We use the letters t, u, v,... to denote terms and the syntactic expressions l, l′, ... to denote lists of arguments.

[ ] stands for the empty list of arguments and [t :: l] stands for the adjunction of the term t to the list of arguments l, while (l @ l′) stands for the explicit concatenation of the lists l and l′ of arguments.

(t[x := u]) stands for an operator of explicit substitution in terms (a let x=u in t operator) and (l[x := u]) stands for an operator of explicit substitution in lists of arguments.

We usually abbreviate an argument list [t_{1} :: [... :: [t_{n} :: [ ]]...]] by [t_{1}; ...; t_{n}]. Terms such as ((...(t t_{1}) ...) t_{n}) are abbreviated (t t_{1} ... t_{n}). Sometimes (x [ ]) is shortened into x. Also, the expressions (λx.t), (t[x := u]) and (l @ l′) may be written respectively λx.t, t[x := u] and l @ l′ when there is no ambiguity.

Subexpressions of \overline{λ}-expressions are defined as usual, but, in our case, by a simultaneous recursion on terms and arguments lists.

Bound variables are defined as usual. We say that two \overline{λ}-expressions are α-equal if they differ only in the names (assumed distinct the one from the others) of bound variables. This notion of equality does not affect the structure of expressions and, in the sequel, we consider \overline{λ}-expressions up to this α-equality.

2.2 Normal \overline{λ}-expressions

Definition 2 A \overline{λ}-expression is normal if and only if it does not contain any operator of explicit concatenation or explicit substitution and if all applicative subterms are of the form (x l) with l normal.

Otherwise said, a \overline{λ}-expression, is normal if it is construed using this restricted grammar:

\begin{aligned}t & ::= & (x l)|(λx.t) \\ l & ::= & [ ]|[t :: l] \end{aligned}

An approximation of normality is weak normality.

Definition 3 A \overline{λ}-expression is called weakly normal if it is of the form (x l) or λx.t or [ ] or [t :: l], where t and l denotes respectively any term and any list of arguments.

Remark: There is, in \overline{λ}-calculus, the possibility to consider terms of the form (...(x [u_{1}]) ... [u_{n}]) having a structure similar to the structure of applicative terms in λ-calculus. However, such a \overline{λ}-term is not normal. Indeed, its normal form is (x [u_{1}; ...; u_{n}]).

2.3 Reduction rules

The presence of explicit substitution and concatenation operators entails the presence of appropriated reduction rules :

• β-reduction

\begin{matrix}(λx.u [v :: l]) & →^{r} & (u[x := v] l) & β_{cons} \\ (λx.u [ ]) & →^{r} & λx.u & β_{nil} \end{matrix}

• concatenation of the arguments of a term

((x l) l′) →^{r} (x (l @ l′)) C_{var}

• concatenation computation rules

\begin{matrix}[u :: l] @ l′ & →^{r} & [u :: (l @ l′)] & C_{cons} \\ [ ] @ l′ & →^{r} & l′ & C_{nil} \end{matrix}

• propagation of substitution through weakly normal terms

\begin{matrix}(x l)[x := v] & →^{r} & (v l[x := v]) & S_{yes} \\ (y l)[x := v] & →^{r} & (y l[x := v]) & S_{no} \\ (λy.u)[x := v] & →^{r} & λy.(u[x := v]) & S_{λ} \end{matrix}

warning to a possible variable capture in rule S_{λ} • propagation of substitution through weakly normal arguments

\begin{matrix}[ ][x := v] & →^{r} & [ ] & S_{nil} \\ [u :: l][x := v] & →^{r} & [u[x := v] :: l[x := v]] & S_{cons} \end{matrix}

If u →^{r} v, then u is called a redex. We note →^{1} the one step reduction obtained from →^{r} by congruence. Since the system of reduction rules is left linear (if one takes one different rule for each different variable name) and without critical pairs, according to Huet [7], →^{1} is confluent. We stay unprecised about the α-equality problem stemming from the rule S_{λ}. Solutions exist, for instance by adding an extra explicit renaming rule to the rewriting system.

Remark: The absence of critical pairs may be quite restricting. For instance, it is not possible to simulate usual β-reduction using this rules for the reason that substitutions are not allowed to go through β-redexes. However, the set of rules is enough to reach a normal form, when this one exists.

3 The calculus LJT

We formally describe the calculus LJT. Our presentation is slightly different from the one done by Danos et al [2] in the treatment of structural rules^{1}.

3.1 Formulas and sequents

We assume the existence of an infinite set V_{F} of which the elements are called propositional variable names and here denoted by the letters X, Y, ...

Definition 4 The set of formulas is an inductive structure defined by the following grammar where X ranges over V_{F}.

A ::= X | A→A

We use the letters A, B, C, ... to denote formulas.

We assume the existence of an infinite set N of which the elements are called names. We use the letters m, n, to denote names.

Definition 5 A named formula, written under the form A^{m} is the pair of a name and a formula.

Practically, we do not mention the names, except if a confusion may occur.

Definition 6 An environment is a set of named formulas. It may occur several times the same formula in an environment but each time with a different associated name.

We use the letters Γ, Δ, Ω,... to denote sets of named formulas. Under the condition that Γ and Δ have an empty intersection, the notation Γ, Δ stands for the set-theoretic union of Γ and Δ.

Definition 7 In a sequent, written under the form Γ; Π ⊢ A, the place on the right of the semi-colon is called the stoup. The stoup may be either empty or containing a single formula. Π is such a notation to express “nothing or a formula”.

Thus, there are two kinds of sequents in LJT. Those with an empty stoup and those with a non empty stoup. As said in the introduction, the use of a stoup is a way to restrict the application of the implication left introduction rule.

1Danos et al have pointed out this restriction of LJ for the reason that it is decorable: a proof of LJT can be translated into a proof of linear logic having the same structure.

3.2 Inference rules

The inference rules of LJT have been already given in the introduction. We recall them.

axiom rule  contraction rule
Γ; A ⊢ A Ax  {Γ, A; A ⊢ B \atop Γ, A; ⊢ B} Cont
→ left introduction rule  → right introduction rule
\begin{matrix}Γ; ⊢ A & Γ; B ⊢ C \\ Γ; A→B ⊢ C \end{matrix} Imp_{L}  {Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R}
head-cut rule  mid-cut rule
\begin{matrix}Γ; Π ⊢ A & Γ; A ⊢ B \\ Γ; Π ⊢ B \end{matrix} Cut_{H}  \begin{matrix}Γ; ⊢ A & Γ, A; Π ⊢ B \\ Γ; Π ⊢ B \end{matrix} Cut_{M}

We say that two proofs are equal if they differ only by the names of formula in the proved sequent or by addition of irrelevant formulas to the left part of the proved sequents. We consider proofs up to this notion of equality. In particular, if p is a proof of Γ; Π ⊢ A, then, for any named formula B not in Γ, p is a proof of Γ, B; Π ⊢ A, even if it becomes necessary to change the name of another occurrence of B with the same name throughout p.

3.3 Cut-elimination

Proposition 1 (Strong and confluent cut-elimination) There exists a confluent system of rewriting rules which allows to derive a cut-free proof of Γ; Π ⊢ A from any proof of the same sequent.

Such a system of rewriting rules is listed hereafter. It is easy to see that it is complete, since it exhausts all possible patterns having a cut rule as head symbol. Its confluence comes from its left linearity (if one takes one different rule for each different variable name) and from the absence of critical pairs, as for the system of reduction rules of the \overline{λ}-calculus. As for its strong termination, the proof is done in a next section.

Reduction of Cut_{H} rules

• β-reduction

\begin{matrix}{Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R} & \begin{matrix}Γ; ⊢ A & Γ; B ⊢ C \\ Γ; A→B ⊢ C \end{matrix} Imp_{L} \\ Γ; ⊢ C \end{matrix} ; Cut_{H}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ; ⊢ A & Γ, A; ⊢ B \\ Γ; ⊢ B \end{matrix} Cut_{M} & Γ; B ⊢ C \\ Γ; ⊢ C \end{matrix} Cut^{H}

\begin{matrix}{Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R} & Γ; A→B ⊢ A→B Ax \\ Γ; ⊢ A→B \end{matrix} ; Cut_{H}  \underrightarrow{LJT}  {Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R}

• concatenation of the arguments of a term

\begin{matrix}{Γ, B; B ⊢ A \atop Γ, B; ⊢ A} Cont & Γ, B; A ⊢ C \\ Γ, B; ⊢ C \end{matrix} Cut^{H}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ, B; B ⊢ A & Γ, B; A ⊢ C \\ Γ, B; B ⊢ C \end{matrix} & Cut_{H} \\ Γ, B; ⊢ C \end{matrix} ; Cont

• concatenation computation rules

\begin{matrix}\begin{matrix}Γ; ⊢ D & Γ; B ⊢ A \\ Γ; D →B ⊢ A \end{matrix} Imp_{L} & Γ; A ⊢ C \\ Γ; D →B ⊢ C \end{matrix} Cut^{H}  \underrightarrow{LJT}  \begin{matrix}Γ; ⊢ D & \begin{matrix}Γ; B ⊢ A & Γ; A ⊢ C \\ Γ; B ⊢ C \end{matrix} Cut_{H} \\ Γ; D →B ⊢ C \end{matrix} ; Imp_{L}

\begin{matrix}Γ; A ⊢ A Ax & Γ; A ⊢ C \\ Γ; A ⊢ C \end{matrix} Cut_{H}  \underrightarrow{LJT}  Γ; A ⊢ C

Reduction of Cut_{M} rules • propagation of substitutions through weakly normal terms

\begin{aligned}Γ; ⊢ A & {Γ, A; A ⊢ C \atop Γ, A; ⊢ C} Cont \\ & Γ; ⊢ C \end{aligned} ; Cut_{M}  \underrightarrow{LJT}  \begin{aligned}Γ; ⊢ A & \begin{matrix}Γ; ⊢ A & Γ, A; A ⊢ C \\ Γ; A ⊢ C \end{matrix} Cut_{M} \\ & Γ; ⊢ C \end{aligned} ; Cut_{H}

\begin{matrix}Γ, B; ⊢ A & {Γ, A, B; B ⊢ C \atop Γ, A, B; ⊢ C} Cont \\ Γ, B; ⊢ C \end{matrix} ; Cut_{M}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ, B; ⊢ A & Γ, A, B; B ⊢ C \\ Γ, B; B ⊢ C \end{matrix} & Cut_{M} \\ Γ, B; ⊢ C \end{matrix} ; Cont

\begin{matrix}Γ; ⊢ A & {Γ, A, B; ⊢ C \atop Γ, A; ⊢ B →C} Imp_{R} \\ Γ; ⊢ B →C \end{matrix} ; Cut_{M}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ, B; ⊢ A & Γ, A, B; ⊢ C \\ Γ, B; ⊢ C \end{matrix} & Cut_{M} \\ Γ; ⊢ B →C \end{matrix} ; Imp_{R}

note that, if B already occurs with the same name somewhere in the proof of Γ; ⊢ A, then this latter name has to be changed throughout the proof.

• propagation of substitution through weakly normal list of arguments

\begin{aligned}Γ; ⊢ A & \begin{matrix}Γ, A; ⊢ B & Γ, A; C ⊢ D \\ Γ, A; B →C ⊢ D \end{matrix} Imp_{L} \\ & Γ; B →C ⊢ D \end{aligned} ; Cut_{M}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ; ⊢ A & Γ, A; ⊢ B \\ Γ; ⊢ B \end{matrix} Cut_{M} & \begin{matrix}Γ; ⊢ A & Γ, A; C ⊢ D \\ Γ; C ⊢ D \end{matrix} Cut_{M} \\ Γ; B →C ⊢ D \end{matrix} ; Imp_{L}

\begin{matrix}Γ; ⊢ A & Γ, A; B ⊢ B Ax \\ Γ; B ⊢ B \end{matrix} ; Cut_{M}  \underrightarrow{LJT}  Γ; B ⊢ B Ax

4 The assignment of proofs in LJT by \overline{λ}-expressions

Proofs of LJT have a structure of \overline{λ}-expressions. We show it by assigning \overline{λ}-expressions to proofs of LJT. What has to be noticed is that, through this assignment, the reduction rules for \overline{λ}-expressions are in exact correspondence with the rewriting rules for proofs of LJT. Definition 8 A declaration, written under the form x : A is the pair of a term variable name and a formula. Definition 9 We keep the word environment to denote a sequence of declarations and we use the same letters Γ, Δ, Ω as before to denote them.

To describe the assignment, it is more cumbersome to consider arguments lists as applicative contexts. Definition 10 An applicative context is a list of arguments written under the form (. l) where . is a special notational symbol. Also, we call hole declaration a formula written under the form . :A.

We express the assignment by judgments. Definition 11 A judgement is something of the form Γ; Π ⊢ t: A. In this writing Π is either nothing, in which case t is a term, or a hole declaration in which case t is an applicative context.

Otherwise said, in the assignment, proofs of sequents with an empty stoup are interpreted by terms while proofs of sequents with a non empty stoup are interpreted by applicative contexts.

Applicative context formation rules

Empty list of arguments  Γ; . :A ⊢ (. [ ]):A Ax
Addition of an argument  \begin{matrix}Γ; ⊢ u:A & Γ; . :B ⊢ (. l):C \\ Γ; . :A→B ⊢ (. [u :: l]):C \end{matrix} Imp_{L}
Concatenation of list of arguments \begin{matrix}Γ; . :C ⊢ (. l):A & Γ; . :A ⊢ (. l′):B \\ Γ; . :C ⊢ (. (l @ l′)):B \end{matrix} Cut_{H}
Substitution in list of arguments  \begin{matrix}Γ; ⊢ u:A & Γ, x:A; . :C ⊢ (. l):B \\ Γ; . :C ⊢ (. l[x := u]):B \end{matrix} Cut_{M}

Term formation rules

Weakly normal applicative term  {Γ, x:A; . :A ⊢ (. l):B \atop Γ, x:A; ⊢ (x l):B} Cont
Abstraction  {Γ, x:A; ⊢ u:B \atop Γ; ⊢ λx.u:A→B} Imp_{R}
Non weakly normal applicative term \begin{matrix}Γ; ⊢ u:A & Γ; . :A ⊢ (. l):B \\ Γ; ⊢ (u l):B \end{matrix} Cut_{H}
Substitution in terms  \begin{matrix}Γ; ⊢ u:A & Γ, x:A; ⊢ v:B \\ Γ; ⊢ v[x := u]:B \end{matrix} Cut_{M}

Remark: The rules with an non empty stoup are polymorphic in the role of the formula in the stoup. So, there is a strong relation between a judgement

Γ; . :A_{1} →...→A_{n} →B ⊢ (. [u_{1}; ...; u_{n}]):B

and a judgement

Γ ⊢ [u_{1}; ...; u_{n}]:A_{1} ∧ ... ∧ A_{n}

where A_{1} ∧ ... ∧ A_{n} is defined as ∀B.(A_{1} → ... → A_{n} → B) → B (encoding of tuples in second order λ-calculus).

Definition 12 A \overline{λ}-expression e such that we have x_{1} : A_{1}, ..., x_{n}: A_{n} ⊢ e: A for some term variable names x_{1}, ..., x_{n} and for some formulas A_{1}, ..., A_{n}, A is said simply-typed of type A, or shortly, typable by A.

5 Strong termination

By the isomorphism, the strong termination of cut-elimination for LJT (using the above rewriting system) and the strong termination of reduction for typable \overline{λ}-expressions are equivalent. We show hereafter the strong termination for typable \overline{λ}-expressions.

Proof of strong termination

Definition 13 Let e be a \overline{λ}-expression and →^{R} a notion of reduction. We say that e is strongly normalisable w.r.t. →^{R} in the following cases:

• e is not reducible w.r.t. →^{R}

• for all e′ such that e →^{R} e′, we have e′ strongly normalisable

Let e be a \overline{λ}-expression. If e is typable, then it is strongly normalisable w.r.t. the reduction →^{1}. To prove that, we prove something stronger, the strong E-normalisability. This latter is preserved by the various operations of \overline{λ}-expressions construction.

We define a notion of reduction →^{h} which removes the head constructor of a \overline{λ}-expression.

Definition 14 More precisely, the reduction →^{h} is defined by the following cases:

\begin{matrix}λx.u & →^{h} & u \\ (x l) & →^{h} & l \\ [u :: l] & →^{h} & u \\ [u :: l] & →^{h} & l \end{matrix}

where u ranges over the set of \overline{λ}-terms and l over the set of argument lists.

Definition 15 We note →^{E}, and we call E-reduction, the notion of reduction defined by e →^{E} e′ either because e →^{1} e′ or because e →^{h} e′ (without considering the closure of →^{h} by congruence). We say that e is strongly E-normalisable (shortly SEN) if it is strongly normalisable w.r.t. →^{E}.

Lemma 1 If the \overline{λ}-term u and the argument list l are SEN then λx.u, (x l) and [u :: l] are SEN.

Proof: By induction on the proof that u is SEN then by induction on the proof that l is SEN. Let us treat of the case [u :: l]. If [u :: l] →^{E} e′ then, either e′ is u or l, in which case, by hypothesis, e′ is SEN, or e′ is [u′ :: l] with u →^{1} u′ , or [u :: l′] with l →^{1} l′ in which cases e′ is SEN by induction hypothesis. Therefore, in any case, e reduces to a SEN \overline{λ}-expression. This implies that e is itself SEN.

Lemma 2 Let e and u be SEN \overline{λ}-expressions. If, for all l SEN, the typability of (u l) implies that (u l) is SEN, then also the typability of e[x := u] implies that e[x := u] is SEN.

Proof: It works by induction on the proof that e is SEN then by induction on the proof that u is SEN.

Let us assume that e[x := u] →^{1} w. If the reduction touchs a redex in u then w has the form e[x := u′] with u →^{1} u′. The proof of SEN for u′ is smaller than the one for u, thus, by induction hypothesis, e[x := u′] is SEN. Similarly, if the reduction is in e.

It remains the case where e[x := u] is itself a redex and where it is this redex which is reduced. We look at the different possible forms for e.

• The case where e is (x l′) — in which case w denotes (u l′[x := u]) — is the more delicate one. But since e →^{h} l′, the proof of SEN for l′ is smaller than the one for e. Therefore, by induction hypothesis, l′[x := u] is SEN. And since we have assumed that for all l SEN, (u l) was SEN, we infer that (u l′[x := u]) is SEN.

• If e is (y l) then w is (y l[x := u]). Here again, l[x := u] is SEN by induction hypothesis. Then, by lemma 1, we get that w is SEN.

• If e is the term λy.v, up to a change of the variable name y in λy.v — and this does not change the structure of the proof of SEN —, we may assume that y and x are distinct variable names. We may then affirm that w is λy.(v[x := u]). Since λy.v →^{E} v, by induction hypothesis, (v[x := u]) is SEN and by lemma 1, w is SEN.

• If e is [v :: l] then w denotes [v[x := u] :: l[x := u]]. But we have both [v :: l] →^{E} v and [v :: l] →^{E} l. Therefore, by induction hypothesis, we have that v[x := u] and l[x := u] are SEN. Then, by lemma 1, we get that w is also SEN.

• If e is [ ] then w is [ ] which is directly SEN.

Thus, whatever the form of e, the reducts of e[x := u] are all SEN. This is enough to say that e[x := u] is SEN.

Lemma 3 Let A be a formula. Let e be a \overline{λ}-expression, SEN and typable by A. Let l be a SEN arguments list. If the expression (e l) (if e is a \overline{λ}-term) or the expression e @ l (if e is an arguments list) is typable, then it is SEN.

Proof: We proceed by induction on A, then on the proof that e is SEN, then on the proof that l is SEN. Let us assume that (e l) →^{1} w (if e is a \overline{λ}-term) or e @ l →^{1} w (if e is an arguments list). If the reduction affects a redex in e then w has the form (e′ l) or e′ @ l with e →^{1} e′. Since the proof of

SEN for e′ is smaller that the one for e, by induction hypothesis, w is SEN. Similarly if the reduction is in l. It may also happen that (e l) or e @ l is a redex and that this redex is the reduced one.

• The more delicate case is when e has the form λx.u while l has the form [v :: l′]. In this case, the type of A has the form B →C, the \overline{λ}-term v is typable by B and w denotes (u[x := v] l′). Since B is smaller than A, by induction hypothesis, the typability of (v l′′) implies that it is SEN whatever l′′ SEN. It is then possible to use lemma 2 in order to infer that u[x := v] is SEN. But this latter is typable by C which is also smaller than A. By induction hypothesis, again, (u[x := v] l) is SEN.

• If e is (x l′) then w denotes (x (l′ @ l)). But (x l′) →^{E} l′, therefore, by induction hypothesis, (l′ @ l) is SEN. By lemma 1, w is SEN.

• If e is λx.u and l denotes [ ] then w is e which, by hypothesis, is SEN.

• If e is [ ] then w denotes l which is directly SEN.

• If e is [v :: l′] then w denotes [v :: (l′ @ l)]. But [v :: l′] →^{E} l′, therefore, by induction hypothesis, l′ @ l is SEN. As for v, it is also SEN by induction hypothesis. Then, by lemma 1, w is SEN.

Thus, whatever reduction of (e l) or e @ l we consider, we get a SEN \overline{λ}-expression. This means that (e l) (if e is a \overline{λ}-term) or e @ l (if e is an arguments list) is SEN.

Proposition 2 Typable \overline{λ}-expressions are SEN.

Proof: Let e be a typable \overline{λ}-expression. The proof works by induction on e. The cases λv, (p l) and (v :: l) come directly from the lemma 1. The cases (u l) and (l @ l′) come from the lemma 3. As for the cases v[x := u] and l[x := u], they come from the lemma 2 applied to the lemma 3.

The strong E-normalisability directly implies the strong normalisability.

Corollary 1 Simply-typed \overline{λ}-expressions are strongly normalizable.

Remark: A similar proof has been done by Dragalin [3] for LK. The difference is that Dragalin’s proof does not work by structural induction on the proof of strong E-normalisability, but rather by induction on the length of these proofs. Our proof has been done independently, extending a proof from Coquand that the elimination of cuts according to an outermost strategy of reduction terminates.

6 Related works

First links between LJ and λ-calculus appear implicitly in Gentzen, and precisely in Prawitz [13], via the translation of LJ-proofs into proofs of natural deduction. It was suggested by Kreisel in [9] to investigate the links between cut-elimination and normalisation.

This has been partially done by Zucker [16] who deduced a strong cut-elimination theorem (up to some “unessential” permutation of rules) for LJ with implication, conjunction and universal quantification from a precise translation of LJ-proofs into proofs of natural deduction. This has been also considered by Pottinger [12] who has extended the result to disjunction and existential quantification. In fact, Zucker and Pottinger were only interested in “essential” reduction rules: the rules which reduces a cut in one (or more) cut(s) of smaller cut formula (what corresponds for the implication to our rule β_{nil}). The other reductions were treated implicitly in the sense that the proofs were considered up to the equivalence generated by these other rules (namely the rules which perform a permutation between a cut and an introduction rule).

More recently, Mints defined in [10] a notion of normal form for cut-free proofs of LJ such that we can get a one-to-one correspondence between normal proofs in LJ and normal simply-typed terms.

On another side, the linear logic approach has led to define constrained versions of LJ. The calculus ILU, described by Girard [6], is such an instance and the relation with λ-calculus seems clear when Girard explicitly says about ILU that “the formula [in the stoup] (if there is one) is the analogue of the familiar head-variable for typed λ-calculi”.

A radically different approach of the computational content of Gentzen’s sequent calculus appears in Breazu Tanen et al [1], Gallier [5] and Wadler [15]. Each of them interprets the left introduction rules of sequent calculus as pattern construction rules.

A proof of strong normalisation similar to ours has already been done by Dragalin [3]. This was for the system of reduction rules given in the seminal paper of Gentzen on the cut-elimination theorem for LK.

Note that this kind of strong cut-elimination proof applies also to non-confluent systems of reduction rules (it is the case of Gentzen’s system of reduction rules) but not to system including rules affecting the order of cuts. This is contrast with Zucker or Pottinger cut-elimination procedures. Note also that an adaptation of Dragalin’s proof has been done by Roorda [14] for the sequent calculus LL (linear logic).

7 Conclusion

By this isomorphism, sequent calculus and its left introduction rules, appear no less related to functional (or deductive) features than natural deduction. Therefore, the problem of assigning a meaning to sequent calculus, say LJ or LK, seems to lie mostly in the control of what seems to be a too large freedom in the possible order of introduction rules.

We get a calculus which, like natural deduction, has a precise computational term counterpart, but which, unlike natural deduction, behaves well w.r.t. disjunction.

We have to recall also that the fact to consider an explicit substitution is crucial in our work.

Part II

The isomorphism for classical logic

8 Extension to classical logic

The λμ-calculus of Parigot [11] extends the Curry-Howard-De Bruijn isomorphism to classical natural deduction. It has been shown in Danos et al [2] that a natural sequent calculus for which cut-free proofs are in bijection with normal typed λμ-terms is a calculus called LKT. This calculus, defined by Joinet in his thesis and which is also described in [2], is a proper fragment of LK ^{2}. We extend \overline{λ}-expressions into \overline{λ}μ-expressions and show an isomorphism between simply-typed \overline{λ}μ-expressions and a certain classical sequent calculus LKT with implication as sole connective.

8.1 The \overline{λ}μ-calculus

In addition to the set V of term variable names, we assume the existence of an infinite set V_{C} of which the elements are called conclusion names. Here, we denote these conclusion names by the letters α, β, γ, ...

Definition 16 The set of \overline{λ}μ-expressions including the \overline{λ}μ-terms and the lists of arguments is defined by the following grammar in which x ranges over V and α, β over V_{C}

Terms:  t ::= (x l) | (λx.t) | (t l) | (t[x := t]) | μβ[α]t | t[[α]x := [α](x l)]
Argument lists: l ::= [ ] | [t :: l] | (l @ l) | l[x := t] | l[[α]x := [α](x l)]

We use the same letters t, u, v,... as for \overline{λ}-terms to denote \overline{λ}μ-terms and the expressions l, l′, ... to denote lists of arguments.

Intuitively, \overline{λ}μ-terms manage several nested \overline{λ}-terms together. α, β are names for these \overline{λ}-terms which can be nested. Several such \overline{λ}-terms may share the same name. At each time, one of these families of \overline{λ}-terms having the same name is active and the role of the operator μβ[α]t is to hide the current term t under the name α and to active the family of terms having the name β. The syntax t[[α]x := [α](x l)] stands for the explicit substitution of the arguments l on the subterms of the family referred by α. Similarly for l[[α]x := [α](x l)] inside arguments list.

Among the new expression constructors, only the μβ[α]t operator may occur in normal \overline{λ}μ-expressions.

Definition 17 A \overline{λ}μ-expression is normal if it belongs to the expressions generated by this grammar:

\begin{aligned}t & ::= & (x l) | (λx.t) | μβ[α]t \\ l & ::= & [ ] | [t :: l] \end{aligned}

A conclusion name α occurring in the scope of a μα[β] operator is called bound conclusion. We say that two \overline{λ}μ-expressions are α-equal if they differ only in the names of bound conclusions and bound variables. This notion of equality does not affect the structure of the expression and, in the sequel, we consider \overline{λ}μexpressions up to this α-equality.

2As for LJT, the proofs of this calculus have a structure of proof of linear logic. That was the motivation for giving a name to it

Reduction rules

In addition to the reduction rules already given for \overline{λ}-expressions, we consider the following reduction rules:

• μ-reduction

(μβ[α]u l) →^{r} μβ[α](u[[β]x := [β](x l)]) μ

• “push of an arguments list towards its place”

\begin{matrix}(μβ[α]u)[[α]x := [α](x l)] & →^{r} & μβ[α](u l) & D_{yes} \\ (μβ[γ]u)[[α]x := [α](x l)] & →^{r} & μβ[γ](u[[α]x := [α](x l)]) & D_{no} \\ (λy.u)[[α]x := [α](x l)] & →^{r} & λy.(u[[α]x := [α](x l)]) & D_{λ} \\ (y l′)[[α]x := [α](x l)] & →^{r} & (y (l′[[α]x := [α](x l)])) & D_{app} \\ ([u :: l′])[[α]x := [α](x l)] & →^{r} & [u[[α]x := [α](x l)] :: l′[[α]x := [α](x l)]] & D_{cons} \\ ([ ])[[α]x := [α](x l)] & →^{r} & [ ] & D_{nil} \end{matrix}

warning to a possible capture of the name β inside l for the rules D_{yes} and D_{no}

8.2 The calculus LKT

We describe here a version for which environments are sets of named formulas.

Definition 18 A classical sequent has the form Γ; Π ⊢ Δ; A. There are two stoups. The left one may be either empty or containing a single formula. Π is such a notation to express “nothing or a formula”. The right one defines the current conclusion. It always contains one and only one formula.

The place where A stands is the intuitionistic place. LJT can be seen as the fragment of LKT for which Δ is always empty. Actually, all rules of LKT which do not affect Δ are rules also of LJT.

To the rule of LJT extended with Δ, we add the introduction rule

{Γ; ⊢ Δ, A, B; A \atop Γ; ⊢ Δ, A; B} Chg

and the cut rule

Γ; Π ⊢ Δ, A; C Γ; A ⊢ Δ; B

Γ; Π ⊢ Δ, B; C Cut_{μ}

They are related to \overline{λ}μ-expressions by the following assignments

{Γ; ⊢ Δ, α:A, β:B; u:A \atop Γ; ⊢ Δ, α:A; μβ[α]u:B} Chg

\begin{matrix}Γ; ⊢ Δ, α:A; u:C & Γ; . :A ⊢ Δ; (. l):B \\ Γ; ⊢ Δ, α:B; u[[α]x := [α](x l)]:C \end{matrix} Cut_{μ}

\begin{matrix}Γ; . :D ⊢ Δ, α:A; (. l′):C & Γ; . :A ⊢ Δ; (. l):B \\ Γ; . :D ⊢ Δ, α:B; (. l′)[[α]x := [α](x l)]:C \end{matrix} Cut_{μ}

In addition to the system of rewriting rules for LJT, we have seven new rules of cut-elimination in correspondence with the extra reduction rules for \overline{λ}μ-expressions. These extra rules also express that the rules are compatible with typing.

8.3 How to recover LK ?

Any proof of Γ ⊢ Δ in LK may be translated into a proof of Γ; ⊢ Δ′; A in LKT in which A is a formula of Δ such that Δ is Δ′, A. The translation is as follows:

Γ, A ⊢ Δ, A Ax  is translated by  \begin{matrix}Γ; A ⊢ Δ; A & Ax \\ Γ, A; ⊢ Δ; A \end{matrix} ; Cont

\begin{matrix}⋮ . ; Γ, A→B ⊢ Δ, A & ⋮ . ; Γ, A→B, B ⊢ Δ, C \\ Γ, A→B ⊢ Δ, C \end{matrix} Imp_{L}  is translated by  ⋮ . ; Γ, A→B; ⊢ Δ′′, A; E ; Γ, A→B; ⊢ Δ; A Chg Γ, A→B; B ⊢ Δ; B Γ, A→B; A→B ⊢ Δ; B Imp_{L} Γ, A→B; ⊢ Δ; B Cont ⋮ . ; Γ, A→B, B; ⊢ Δ′, C; D Γ, A→B; ⊢ Δ′, C; D Cut_{M}

in which Δ′, D and Δ′′, E are identical to Δ

⋮ . ; Γ, A ⊢ Δ, B ; Γ ⊢ Δ, A→B Imp_{R}  is translated by  \begin{matrix}⋮ . ; Γ, A; ⊢ Δ′, B; D ; Γ, A; ⊢ Δ; B & Chg \\ Γ; ⊢ Δ; A→B \end{matrix} ; Imp_{R}

\begin{matrix}⋮ . ; Γ ⊢ Δ, A & ⋮ . ; Γ, A ⊢ Δ, B \\ Γ ⊢ Δ, B \end{matrix} Cut  is translated by  ⋮ . ; Γ; ⊢ Δ′, A; D ; Γ; ⊢ Δ; A Chg ⋮ . ; Γ, A; ⊢ Δ′′, B; E Γ; ⊢ Δ′′, B; E Cut_{M}

in which Δ′, D and Δ′′, E are identical to Δ

Simplifications of this translation are possible. Especially, the change rule is sometimes useless.

8.4 Strong termination

The cut rules are strongly eliminable from proofs of LKT, w.r.t. the above system of elementary cutelimination rewriting rules. Concurrently, typable \overline{λ}μ-expressions are strongly normalisable.

The proof is not basically different from the proof of strong termination for typable \overline{λ}-expressions. In addition to the redexes associated to the head-cut and mid-cut rules, we have to consider the redexes associated to the μ-cut rule. But the μ-cut rule works as the head-cut rule. Thus, it is sufficient to restate the lemma 3 under this form:

Lemma 4 Let A be a formula. Let u_{1} (resp l_{1}) be a \overline{λ}-expression typable by A and having a degree. If l_{2} has a degree and (u_{1} l_{2}) (resp l_{1} @ l_{2}) and u_{1}[[α]x := [α](x l_{2})] (resp l_{1}[[α]x := [α](x l_{2})]) are typable, then (u_{1} l_{2}) (resp l_{1} @ l_{2}) and u_{1}[[α]x := [α](x l_{2})] (resp l_{1}[[α]x := [α](x l_{2})]) have also a degree.

We do not explicit the proof. A quite similar proof can be found a bit further for LKT with a non implicit weakening rule.

8.5 The \overline{λ}μ-calculus with De Bruijn indices

It is also possible to define a version of the calculus with conclusions marked by De Bruijn indices. This implies the use of a second lifting operator with its associated reduction rules.

Definition 19 The set of expressions and the set of lists of arguments are mutually defined by the following grammar in which p ranges over the set of natural numbers.

Terms:  t ::= (p l) | (λt) | (t l) | (t[p := t]) | (t↑_{p})
μ[p]t | t[[p]x := [p](x l)] | (t↑^{p})
Argument lists: l ::= [ ] | [t :: l] | [l @ l] | l[p := t] | (l ↑_{p})
l[[p]x := [p](x l)] | (l ↑^{p})

The expression t↑^{p} stands for the explicit operation of one unit lifting for conclusion indices greater than p in the expression t. Similarly for lists of arguments.

8.6 The calculus LKT with weakening rules

We describe here a version for which environments are sequences of formulas.

Definition 20 A classical sequent has the form Γ; Π ⊢ Δ; A. There are two stoups. The left one may be either empty or containing a single formula. Π is such a notation to express “nothing or a formula”. The right one defines the current conclusion. It always contains one and only one formula.

All the rules of the version of LJT for which environments are sequences of formulas, when they are extended with a Δ part, are rules of the version of LKT with environments defined as sequences of formulas. In addition, there are the following rules.

{Γ; ⊢ Δ, A, Ω, B; A \atop Γ; ⊢ Δ, A, Ω; B} Chg
Γ; Π ⊢ Δ, A, Ω; C Γ; A ⊢ Δ, Ω; B

Γ; Π ⊢ Δ, B, Ω; C Cut_{μ}

Γ; Π ⊢ Δ, Ω; C

Γ; Π ⊢ Δ, A, Ω; C W_{R}

They are related to \overline{λ}μ-expressions with De Bruijn indices by the following assignments

{Γ; ⊢ Δ,:A, Ω, B; u:A \atop Γ; ⊢ Δ,:A, Ω; μ[p]u:B} Chg
Γ; ⊢ Δ, A, Ω; u:C Γ; . :A ⊢ Δ, Ω; (. l):B

Γ; ⊢ Δ, B, Ω; u[[p]x := [p](x l)]:C Cut_{μ}

Γ; . :D ⊢ Δ, A, Ω; (. l′):C Γ; . :A ⊢ Δ, Ω; (. l):B

Γ; . :D ⊢ Δ, B, Ω; (. l′)[[p]x := [p](x l)]:C Cut_{μ}

Γ; Π ⊢ Δ, Ω; u:C

Γ; Π ⊢ Δ, A, Ω; u↑^{p}:C W_{R}

for which p is, each time, the length of Ω.

In addition to the system of rewriting rules for LJT, we have new rules of cut-elimination in correspondence with the extra reduction rules for \overline{λ}μ-expressions. These extra rules also express that the rules are compatible with typing. We have also new rules of W_{R} elimination which match the rules of reduction for the lifting operator for de Bruijn conclusion indices.

8.7 Strong termination

Let u (resp l) be a \overline{λ}μ-expression with de Bruijn indices. If u (resp l) is typable, then it is strongly normalisable w.r.t. to the reduction →^{1}.

The proof is not basically different from the proof of strong termination for typable \overline{λ}-terms with De Bruijn indices. In addition to the eliminability of the left weakening, head-cut and mid-cut ruleswe have to consider the case of the right weakening and μ-cut rules. The eliminability of the former works as the eliminability of the left weakening rule. The eliminability of the latter works as the eliminability of the head-cut rule.

Definition 21 u′ (resp l′) is an immediate reduct of u (resp l) iff u →^{1} u′ (resp l →^{1} l′).

Definition 22 The degree of a term (resp an arguments list), if it exists, is a combined measure of its depth and of the depth of its reduction tree.

• The term (resp arguments list) is weakly normal

– [ ] has degree 0.

– If u has a degree n then λu has degree n + 1

– If u has a degree n and l degree m then [u :: l] has degree max(n, m) + 1.

– If l has a degree n then (p l) has degree n + 1

– If t has a degree n then μ[p]t has degree n + 1

• The term (resp arguments list) is not weakly normal

– If the immediate reducts of u (resp l) have respective degrees n_{1}, ..., n_{r} then u (resp l) has degree max(n_{1}, ..., n_{r}) + 1.

Lemma 5 If u (resp l) has a degree n and u →^{1} u′ (resp l →^{1} l′) then u′ (resp l′) has a degree m < n.

Proof: By simultaneous induction on u and l. If u or l is not weakly normal, it is direct by the definition. Otherwise, we use the induction hypothesis.

Lemma 6 If u (resp l) has a degree then u↑_{p} (resp l ↑_{p}) and u↑^{p} (resp l ↑^{p}) have too.

Proof: We proceed by simultaneous induction on the degree of u or l.

Let us consider the case of u. Let u′ such that u ↑_{p}→^{1} u′. If the reduction affects a proper subterm of u ↑_{p} then u′ has the form u′′ ↑_{p}, with u →^{1} u′′. By lemma 5, u′′ has a smaller degree than u and therefore, by induction hypothesis, u′ has a degree. If u is weakly normal, u ↑_{p} is a redex and u′ may result of the reduction of this redex. If u is λv then u′ is λ(v ↑_{p+1}). By definition of the degree, v has a degree less than the degree u. Therefore, by induction hypothesis, v ↑_{p+1} has a degree and thus u′ also. If u is (p l) then u′ is (p l ↑_{p}). The degree of l is smaller than the degree of u, hence, by induction hypothesis, l ↑_{p} has a degree and u′ also. In any case, u′ has a degree, thus, u↑_{p} has a degree.

The cases of l and ↑^{p} are of the same kind.

Lemma 7 Let u_{1} and u_{2} (resp l_{2}) be \overline{λ}-terms having a degree. If, for all l_{1} having a degree, (u_{1} l_{1}) has a degree, then u_{2}[x := u_{1}] (resp l_{2}[x := u_{1}]) has a degree.

Proof: The proof is done by induction on the degrees of u_{2} (resp l_{2}) then on the degree of u_{1}.

• The case of u_{2}[p := u_{1}] is the more delicate one.

Let us suppose that u_{2}[p := u_{1}] →^{1} w. If the reduction affects a redex in u_{1} then w has the form u_{2}[p := u′_{1}] with u_{1} →^{1} u′_{1}. By lemma 5, u′_{1} has a smaller degree than u_{1} and therefore, by induction hypothesis, u_{2}[p := u′_{1}] has a degree. Similarly if the reduction is in u_{2}. But u_{2}[p := u_{1}] can be itself a redex.

The more complex case when u_{2}[p := u_{1}] is itself a redex is when u_{2} is (p l). In such a case w is (u_{1} l[p := u_{1}]). But l has a smaller degree than u_{2}, therefore, by induction hypothesis, l[p := u_{1}] has a degree. Also, using the assumption to the lemma, (u_{1} l[p := u_{1}]) has a degree.

Another case is when u_{2} is λv and w is λ(v[p := u_{1} ↑_{0}]). In this case we use lemma 6 to affirm the existence of a degree for u_{1} ↑_{0}. Then v has a smaller degree than λv and we can apply the induction hypothesis to get a degree for w.

The case when u_{2} is (q l) with q ≠ p and the case when u_{2} is μ[q]v are simple.

Thus, in all the cases, the reducts of (u_{1} l_{2}) have a degree and then (u_{1} l_{2}) has itself a degree.

• It remains to study the case of l_{2}[p := u_{1}], which is simpler.

Lemma 8 Let A be a formula. Let u_{1} (resp l_{1}) be a \overline{λ}-term typable by A and having a degree. If l_{2} has a degree and (u_{1} l_{2}) (resp l_{1} @ l_{2}) and u_{1}[[p]x := [p](x l_{2})] (resp l_{1}[[p]x := [p](x l_{2})]) are typable, then (u_{1} l_{2}) (resp l_{1} @ l_{2}) and u_{1}[[p]x := [p](x l_{2})] (resp l_{1}[[p]x := [p](x l_{2})]) have also a degree.

Proof: The proof is by induction on A then by induction on the degrees of u_{1} or l_{1} and on the degree of l_{2}.

• The case of (u_{1} l_{2}) is the delicate one.

Let us suppose that (u_{1} l_{2}) →^{1} w. If the reduction affects a redex in u_{1} then w has the form (u′_{1} l_{2}) with u_{1} →^{1} u′_{1}. By lemma 5, u′_{1} has a smaller degree than u_{1} and therefore, by induction hypothesis, (u′_{1} l_{2}) has a degree. Similarly if the reduction is in l_{2}. But (u_{1} l_{2}) can be itself a redex. The more subtil case is when u_{1} is λu and l_{2} is [v :: l]. In such a case, A has the form B → C, v is typable by B and w is (u[0 := v] l). Since B is structurally smaller than A, by induction hypothesis, (u l′) has a degree, whatever l′ having a degree. Then, by lemma 7, u[0 := v] has a degree. But this last term is typable by C structurally smaller than A. Therefore (u[0 := v] l) has a degree. For the other possible forms of w, we can prove similarly that w has a degree. Thus, all reducts of (u_{1} l_{2}) have a degree, then (u_{1} l_{2}) has itself a degree.

• We do not write precisely the case of l_{1} @ l_{2} is: it is simpler than the case of (u_{1} l_{2}).

• The case of u_{1}[[p]x := [p](x l_{2})] is simple, using the case (u_{1} l_{2})

• The case of l_{1}[[p]x := [p](x l_{2})] is simple using the case of l_{1} @ l_{2}.

Proposition 3 If u (resp l) is typable then it has a degree.

Proof: By simultaneous induction on u or l. The cases λv, (p l′), (v :: l′), (l_{1} @ l_{2}) and μ[p]t are direct by the definition of degree. The other cases comes from lemmas 6, 8 and 7, this latter being combined with 8

By lemma 5, the existence of a degree implies the finiteness of reductions.

Corollary 2 Simply-typed \overline{λ}μ-terms (and LKT-proofs) are strongly normalizable.

8.8 \overline{λ}_{C}-calculus and LJT + ¬¬A→A

We get an alternative framework for classical logic if we consider the C operator of Felleisen [4] which is known to be typable by the rule of double negation elimination.

The \overline{λ}_{C}-calculus Definition 23 The set of terms and arguments lists for the \overline{λ}_{C}-calculus are defined by

Terms:  t ::= (p l) | (λt) | (t l) | (t[p := t]) | C(t)
Argument lists: l ::= [ ] | [t :: l] | [l @ l] | l[p := t]

Definition 24 The set of normal terms and arguments lists are defined by

\begin{aligned}t & ::= & (p l) | (λt) | C(t) \\ l & ::= & [ ] | [t :: l] \end{aligned}

The additional rules of reduction are:

• C-reduction

(C(u) l) →^{r} C(λk.(u [λx.(k [(x l)])]))

for which k and x have to be fresh in u and l • propagation of substitution

C(u)[x := v] →^{r} C(u[x := v])

The calculus LJT with the rule ¬¬A→A First, formulas are extended with the constant ⊥. Definition 25 The set of formulas is now defined by the following grammar:

A ::= X | A→A | ⊥

Notation: ¬A stands for the formula A→⊥.

To the rules of LJT, we add the rule

{Γ; ⊢ ¬¬A \atop Γ; ⊢ A}

with the assignment

{Γ; ⊢ u:¬¬A \atop Γ; ⊢ C(u):A}

and we recover classical logic.

Part III

Variants and extensions

9 Extension to disjunction, injections and the case operator

9.1 The \overline{λ}-calculus with injections and the case operator

Definition 26 The new set of terms is defined by the following rules:

Terms:  t ::= (x l) | (λx.t) | (t l) | (t[x := t]) | inj_{1}(t) | inj_{2}(t)
Argument lists: l ::= [ ] | [t :: l] | (l @ l) | l[x := t] | [<(x)t|(x)t>]

The argument list [< (x)t|(y)u >] stands for a case operator. If we see it as the applicative context (. [<(x)t|(y)u>]), then we can adopt the more expressive notation

case . of inj_{1}(x) −> t | inj_{2}(y) −> u

Definition 27 The subset of normal forms is defined by:

\begin{aligned}t & ::= & (x l) | (λx.t) | inj_{1}(t) | inj_{2}(t) \\ l & ::= & [ ] | [t :: l] | [<(x)t|(x)t>] \end{aligned}

Reduction rules

To the reduction rules of the minimal version of the calculus, we add the following reduction rules:

• case operator reduction

\begin{matrix}(inj_{1}(t) [<(x)u|(y)v >] & →^{r} & u[x := t] \\ (inj_{2}(t) [<(x)u|(y)v >] & →^{r} & v[y := t] \end{matrix}

• additional rules for substitution propagation

\begin{matrix}inj_{1}(t)[z := v] & →^{r} & inj_{1}(t[z := v]) \\ inj_{2}(t)[z := v] & →^{r} & inj_{2}(t[z := v]) \\ [<(x)u|(y)v >][z := w] & →^{r} & [<(x)u[z := w]|(y)v[z := w]>] \end{matrix}

warning to a possible capture of variable in the third rule

• additional rules for concatenation computation

[<(x)u|(y)v >] @ l′ →^{r} [<(x)(u l′)|(y)(v l′)>]

Remark: The rule

((case u of inj_{1}(x) −> v | inj_{2}(y) −> w) l) →^{r} (case u of inj_{1}(x) −> (v l) | inj_{2}(y) −> (w l))

derives quite directly from the concatenation computation rules for the case operator. This is not what happens when we add injections and the case operator to the usual λ-calculus. There, the rule above has to be individually considered.

9.2 The calculus LJT with ∨

We add the following disjunction introduction rules:

{Γ; ⊢ A \atop Γ; ⊢ A ∨ B} ∨_{r1} {Γ; ⊢ B \atop Γ; ⊢ A ∨ B} ∨_{r2}

\begin{matrix}Γ, A; ⊢ C & Γ, B; ⊢ C \\ Γ; A ∨ B ⊢ C \end{matrix} ∨_{l}

9.3 The term assignment

{Γ; ⊢ u:A \atop Γ; ⊢ inj_{2}(u):A ∨ B} ∨_{r1} {Γ; ⊢ v:B \atop Γ; ⊢ inj_{2}(v):A ∨ B} ∨_{r2}

\begin{matrix}Γ, x:A; ⊢ u:C & Γ, y:B; ⊢ v:C \\ Γ; . :A ∨ B ⊢ Δ; (. [<(x)u|(y)v >]):C \end{matrix} ∨_{l}

To eliminate the cuts we have to add some new cut elimination rules. We do not mention them. They are the same as the extra rules for the \overline{λ}-calculus. There is just to explicitelyt add which sequents are proved.

10 Extension to conjunction, pair, projections and the splitting operator

The integration of conjunction is simple. The conjunction right introduction cut-free is interpreted by a pairing operator. Two kinds of conjunction left introduction are possible. They are respectively interpreted by projections or by the splitting operator (as in Martin-Löf type theory [8]).

10.1 The \overline{λ}-calculus with pair, projections and the splitting operator

Definition 28 The new set of terms is defined by the following rules:

Terms:  t ::= (x l) | (λx.t) | (t l) | (t[x := t]) | < t, t>
Argument lists: l ::= [ ] | [t :: l] | (l @ l) | l[x := t] | [<x, x> t] | [π_{1} :: l] | [π_{2} :: l]

Definition 29 TThe subset of normal forms is defined by:

\begin{aligned}t & ::= & (x l) | (λx.t) | <t, t> \\ l & ::= & [ ] | [t :: l] | [<x, x> t] | [π_{1} :: l] | [π_{2} :: l] \end{aligned}

Remark: Projections and the splitting operator are redundant. Keeping only one of them does not remove the completeness of the intuitionistic calculus with conjunction.

Reduction rules

To the reduction rules of the minimal version of the calculus, we add the following reduction rules:

• pair destruction

\begin{matrix}(<t, u> [π_{1} :: l]) & →^{r} & (t l) \\ (<t, u> [π_{2} :: l]) & →^{r} & (u l) \\ (<t, u> [<x, y > v]) & →^{r} & v[x := t][y := u] \end{matrix}

• additional rules for substitution propagation

\begin{matrix}<t, u> [z := v] & →^{r} & <t[z := v], u[z := v]> \\ [π_{1} :: l][z := v] & →^{r} & [π_{1} :: l[z := v]] \\ [π_{2} :: l][z := v] & →^{r} & [π_{2} :: l[z := v]] \\ [<x, y > v][z := v] & →^{r} & [<x, y > (v[z := v])] \end{matrix}

warning to a possible capture of variable in the fourth rule

• additional rules for concatenation computation

\begin{matrix}[π_{1} :: l] @ l′ & →^{r} & [π_{1} :: (l @ l′)] \\ [π_{2} :: l] @ l′ & →^{r} & [π_{2} :: (l @ l′)] \\ [<x, y > v] @ l′ & →^{r} & [<x, y > (v l′)] \end{matrix}

10.2 The calculus LJT with ∧

We add the following conjunction introduction rules:

\begin{matrix}Γ; ⊢ A & Γ; ⊢ B \\ Γ; ⊢ A ∧ B \end{matrix} ∧_{r}

{Γ; A ⊢ C \atop Γ; A ∧ B ⊢ C} ∧_{l1} {Γ; B ⊢ C \atop Γ; A ∧ B ⊢ C} ∧_{l2}

{Γ, A, B; ⊢ C \atop Γ; A ∧ B ⊢ C} ∧_{l0}

10.3 The term assignment

\begin{matrix}Γ; ⊢ u:A & Γ; ⊢ v:B \\ Γ; ⊢<u, v >:A ∧ B \end{matrix} ∧_{r}
{Γ; . :A ⊢ (. l):C \atop Γ; . :A ∧ B ⊢ Δ; (. [π_{1} :: l]):C} ∧_{l1} {Γ; . :B ⊢ (. l):C \atop Γ; . :A ∧ B ⊢ Δ; (. [π_{2} :: l]):C} ∧_{l2}

{Γ, x:A, y:B; ⊢ u:C \atop Γ; . :A ∧ B ⊢ Δ; (. [<x, y > u]):C} ∧_{l0}

To eliminate the cuts we have to add some new cut elimination rules. We do not mention them. They are the same as the extra rules for the \overline{λ}-calculus. There is just to explicitelyt add which sequents are proved.

11 Extension to quantifiers and to product and sigma operators

We have now to consider a set of individual terms built upon individual variable names, but also formulas containing such individuals terms.

We use the letters a, b, c, ... to denote individuals terms and r, s to denote individual variable names.

11.1 The \overline{λ}-calculus with product and sigma operators

Definition 30 The sets of terms and arguments lists are defined by:

Terms:  t ::= (x l) | (λx.t) | (t l) | (t[x := t])
| λs.t | <a, t>
Argument lists: l ::= [ ] | [t :: l] | (l @ l) | l[x := t]
| [a :: l] | [<r, x> t>]

where s ranges over the set of individual variable names and a over the set of individual terms. Definition 31 The subset of normal forms is defined by:

\begin{aligned}t & ::= & (x l) | (λx.t) | λs.t | <a, t> \\ l & ::= & [ ] | [t :: l] | [a :: l] | [<r, x> t>] \end{aligned}

Reduction rules We have the extra following reduction rules:

• computation rules

\begin{matrix}(λr.u [a :: l]) & →^{r} & (u′ l) \\ (<a, t> [<r, x> u>]) & →^{r} & u′[x := t] \end{matrix}

where u′ is u in which all occurrences of r have been replaced by a.

• additional rules for substitution propagation

\begin{matrix}(λr.u)[z := v] & →^{r} & λr.(u[z := v]) \\ (<a, t>)[z := v] & →^{r} & <a, t[z := v]> \\ ([a :: l])[z := v] & →^{r} & [a :: l[z := v]] \\ ([<r, x> u>])[z := v] & →^{r} & [<r, x> u[z := v]>] \end{matrix}

warning to a possible capture of variable in the third rule

• additional rules for concatenation computation

\begin{matrix}[a :: l] @ l′ & →^{r} & [a :: (l @ l′)] \\ [<r, x> u>] @ l′ & →^{r} & [<r, x> (u l′)] \end{matrix}

In fact, we see no special interest in this extension of the language of terms, except the fact that this extends the isomorphism to the universal quantifiers.

11.2 The calculus LJT with quantifiers

{Γ; ⊢ A(s) \atop Γ; ⊢ ∀s.A(s)} ∀_{r} {Γ; A(a) ⊢ B \atop Γ; ∀s.A(s) ⊢ B} ∀_{l}
{Γ; ⊢ A(a) \atop Γ; ⊢ ∃s.A(s)} ∃_{r} {Γ, A(s); ⊢ B \atop Γ; ∃s.A(s) ⊢ B} ∃_{l}

with the respective assignment

{Γ; ⊢ u:A(s) \atop Γ; ⊢ λs.u:∀s.A(s)} ∀_{r}  {Γ; . :A(a) ⊢ (. l):B \atop Γ; . :∀s.A(s) ⊢ Δ; (. [a :: l]):B} ∀_{l}
{Γ; ⊢ u:A(a) \atop Γ; ⊢<a, u>:∃s.A(s)} ∃_{r} {Γ, x:A(s); ⊢ u:B \atop Γ; . :∃s.A(s) ⊢ (. [<s, x> u]):B} ∃_{l}

As for the rules allowing the elimination of cuts, they are the typed version of the reduction rules for \overline{λ}-calculus.

12 The full isomorphism

All the previous extensions can be put together in order to get an assignment of proofs of classical predicate calculus either by \overline{λ}μ-terms or by \overline{λ}μ-terms with De Bruijn indices. This induces an impressive number of reduction rules which remain strongly normalizable.

13 An isomorphism for the \overline{λ}-calculus with De Bruijn indices

13.1 The \overline{λ}-calculus with De Bruijn indices

A version of the \overline{λ}-calculus with de Bruijn indices is interesting in two respects. First, the problem of possible clashes for variable names is avoided. Second, we get a nicer correspondence between \overline{λ}-terms and LJT-proofs in the sense that we do not have to consider proofs up to the change of names of formulas and the addition of irrelevant formulas on the left part of the sequents (= implicit weakening rule). Rather, if we consider an explicit weakening rule in LJT, we get a correspondence with the lift operator of the calculus with De Bruijn indices.

Terms

Definition 32 The set of terms and the set of lists of arguments are mutually defined by the following grammar where p ranges over the set of natural numbers.

Terms:  t ::= (p l) | (λt) | (t l) | (t[p := t]) | (t↑_{p})
Argument lists: l ::= [ ] | [t :: l] | [l @ l] | l[p := t] | (l ↑_{p})

The term t↑_{p} stands for the explicit operation of one unit lifting for indices greater than p in the term t. Similarly for lists of arguments.

Reduction rules

The reduction rules for the calculus with De Bruijn indices include computation rules for the lifting operator.

• β-reduction

\begin{matrix}(λu [v :: l]) & →^{r} & (u[0 := v] :: l) & β_{cons} \\ (λu [ ]) & →^{r} & λu & β_{nil} \end{matrix}

• concatenation of the arguments of a term

((p l) l′) →^{r} (p (l @ l′)) C_{var}

• concatenation computation rules

\begin{matrix}[u :: l] @ l′ & →^{r} & [u :: (l @ l′)] & C_{cons} \\ [ ] @ l′ & →^{r} & l′ & C_{nil} \end{matrix}

• propagation of substitution through weakly normal terms

\begin{matrix}(p l)[p := v] & →^{r} & (v l[p := v]) & S_{yes} \\ (q l)[p := v] & →^{r} & (q l[p := v]) & S_{>} (p > q) \\ (q l)[p := v] & →^{r} & (q−1 l[p := v]) & S_{<} (p < q) \\ (λu)[p := v] & →^{r} & λ(u[p+1 := v ↑_{0}]) & S_{λ} \end{matrix}

• propagation of substitution through weakly normal arguments

\begin{matrix}[ ][p := v] & →^{r} & [ ] & S_{nil} \\ [u :: l][p := v] & →^{r} & [u[p := v] :: l[p := v]] & S_{cons} \end{matrix}

• lifting computation rules for weakly normal arguments

\begin{matrix}[ ]↑_{p} & →^{r} & [ ] & L_{nil} \\ [u :: l]↑_{p} & →^{r} & [u↑_{p}:: l ↑_{p}] & L_{cons} \end{matrix}

• lifting computation rules for weakly normal terms

\begin{matrix}(λu)↑_{p} & →^{r} & λ(u↑_{p+1}) & L_{λ} \\ (q l)↑_{p} & →^{r} & (q+1 (l ↑_{p})) & L_{yes} (q ≥ p) \\ (q l)↑_{p} & →^{r} & (q (l ↑_{p})) & L_{no} (q < p) \end{matrix}

13.2 The calculus LJT with a weakening rule

Environment as sequences of formulas

To get the correspondence, we consider now environment as sequence of formulas.

Definition 33 An environment is a sequence of formulas. It may occur at different places several times the same formula in an environment.

We still use the letters Γ, Δ, Ω,... to denote sets of formulas. A notation such as Γ, Δ denotes the concatenation of Γ and Δ.

Definition 34 A sequent is written under the form Γ; Π ⊢ A where the place on the right of the semi-colon is the stoup. The stoup may be either empty or containing a single formula. Π is such a notation to express “nothing or a formula”.

Thus, there are two kinds of sequents in LJT. Those with an empty stoup and those with a non empty stoup. The use of a stoup is a way to restrict the application of the implication left introduction rule Inference rules The inference rules of LJT with an explicit weakening rule are the following ones:

axiom rule  contraction rule
Γ; A ⊢ A Ax  {Γ, A, Δ; A ⊢ B \atop Γ, A, Δ; ⊢ B} Cont
→ left introduction rule  → right introduction rule
\begin{matrix}Γ; ⊢ A & Γ; B ⊢ C \\ Γ; A→B ⊢ C \end{matrix} Imp_{L}  {Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R}
head-cut rule  mid-cut rule
\begin{matrix}Γ; Π ⊢ A & Γ; A ⊢ B \\ Γ; Π ⊢ B \end{matrix} Cut_{H}  Γ, Δ; ⊢ A Γ, A, Δ; Π ⊢ B Γ, Δ; Π ⊢ B Cut_{M}

weakening rule

{Γ, Δ; Π ⊢ B \atop Γ, A, Δ; Π ⊢ B} W

Reduction rules The system of rewriting rules allowing to eliminate cuts is not very different of the one for the calculus without weakening rule. We state it to underline the slight differences.

Reduction of Cut_{H} rules • β-reduction

\begin{matrix}{Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R} & \begin{matrix}Γ; ⊢ A & Γ; B ⊢ C \\ Γ; A→B ⊢ C \end{matrix} Imp_{L} \\ Γ; ⊢ C \end{matrix} ; Cut_{H}  \underrightarrow{LJT}  \begin{matrix}\begin{matrix}Γ; ⊢ A & Γ, A; ⊢ B \\ Γ; ⊢ B \end{matrix} Cut_{M} & Γ; B ⊢ C \\ Γ; ⊢ C \end{matrix} Cut^{H}

\begin{matrix}{Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R} & Γ; A→B ⊢ A→B Ax \\ Γ; ⊢ A→B \end{matrix} ; Cut_{H}  \underrightarrow{LJT}  {Γ, A; ⊢ B \atop Γ; ⊢ A→B} Imp_{R}

• concatenation of the arguments of a term

{Γ, B, Δ; B ⊢ A \atop Γ, B, Δ; ⊢ A} Cont Γ, B, Δ; A ⊢ C Γ, B, Δ; ⊢ C Cut_{H} \underrightarrow{LJT} \begin{matrix}Γ, B, Δ; B ⊢ A & Γ, B, Δ; A ⊢ C \\ Γ, B, Δ; B ⊢ C \end{matrix} Cut_{H} Γ, B, Δ; ⊢ C Cont

\begin{matrix}\begin{matrix}Γ; ⊢ D & Γ; B ⊢ A \\ Γ; D →B ⊢ A \end{matrix} Imp_{L} & Γ; A ⊢ C \\ Γ; D →B ⊢ C \end{matrix} Cut^{H}  \underrightarrow{LJT}  \begin{matrix}Γ; ⊢ D & \begin{matrix}Γ; B ⊢ A & Γ; A ⊢ C \\ Γ; B ⊢ C \end{matrix} Cut_{H} \\ Γ; D →B ⊢ C \end{matrix} ; Imp_{L}

\begin{matrix}Γ; A ⊢ A Ax & Γ; A ⊢ C \\ Γ; A ⊢ C \end{matrix} Cut_{H}  \underrightarrow{LJT}  Γ; A ⊢ C

Reduction of Cut_{M} rules • propagation of substitutions through weakly normal terms

Γ, Δ; ⊢ A {Γ, A, Δ; A ⊢ C \atop Γ, A, Δ; ⊢ C} Cont

Γ, Δ; ⊢ C Cut^{M} \underrightarrow{LJT} Γ, Δ; ⊢ A \begin{matrix}Γ, Δ; ⊢ A & Γ, A, Δ; A ⊢ C \\ Γ, Δ; A ⊢ C \end{matrix} Cut_{M} Γ, Δ; ⊢ C Cut^{H}

Γ, Δ, B, Ω; ⊢ A {Γ, A, Δ, B, Ω; B ⊢ C \atop Γ, A, Δ, B, Ω; ⊢ C} Cont

Γ, Δ, B, Ω; ⊢ C Cut^{M} \underrightarrow{LJT}

Γ, Δ, B, Ω; ⊢ A Γ, A, Δ, B, Ω; B ⊢ C

Γ, Δ, B, Ω; B ⊢ C Cut_{M}

Γ, Δ, B, Ω; ⊢ C Cont

and a similar rule with the places of A and B permuted.

Γ, Δ; ⊢ A {Γ, A, Δ, B; ⊢ C \atop Γ, A, Δ; ⊢ B →C} Imp_{R}

Γ, Δ; ⊢ B →C Cut^{M} \underrightarrow{LJT}

{Γ, Δ; ⊢ A \atop Γ, Δ, B; ⊢ A} W Γ, A, Δ, B; ⊢ C

Γ, Δ, B; ⊢ C Cut_{M}

Γ, Δ; ⊢ B →C Imp^{R}

• propagation of substitution through weakly normal list of arguments

Γ, Δ; ⊢ A \begin{matrix}Γ, A, Δ; ⊢ B & Γ, A, Δ; C ⊢ D \\ Γ, A, Δ; B →C ⊢ D \end{matrix} Imp_{L}

Γ, Δ; B →C ⊢ D Cut^{M} \underrightarrow{LJT} \begin{matrix}Γ, Δ; ⊢ A & Γ, A, Δ; ⊢ B \\ Γ, Δ; ⊢ B \end{matrix} Cut_{M} \begin{matrix}Γ, Δ; ⊢ A & Γ, A, Δ; C ⊢ D \\ Γ, Δ; C ⊢ D \end{matrix} Cut_{M} Γ, Δ; B →C ⊢ D Imp^{L}

\begin{matrix}Γ, Δ; ⊢ A & Γ, A, Δ; B ⊢ B Ax \\ Γ, Δ; B ⊢ B \end{matrix} ; Cut_{M}  \underrightarrow{LJT}  Γ, Δ; B ⊢ B Ax

• shifting of weakening rules until axiom rules

\begin{matrix}Γ, Δ; B ⊢ B & Ax \\ Γ, A, Δ; B ⊢ B \end{matrix} ; W  \underrightarrow{LJT}  Γ, A, Δ; B ⊢ B Ax
\begin{matrix}Γ, Δ; ⊢ B & Γ, Δ; C ⊢ D \\ Γ, Δ; B →C ⊢ D \end{matrix} Imp_{L}

Γ, A, Δ; B →C ⊢ D W \underrightarrow{LJT} {Γ, Δ; ⊢ B \atop Γ, A, Δ; ⊢ B} W {Γ, Δ; C ⊢ D \atop Γ, A, Δ; C ⊢ D} W Γ, A, Δ; B →C ⊢ D Imp^{L}

\begin{matrix}{Γ, Δ, B; ⊢ C \atop Γ, Δ; ⊢ B →C} & Imp_{R} \\ Γ, A, Δ; ⊢ B →C \end{matrix} ; W  \underrightarrow{LJT}  \begin{matrix}{Γ, Δ, B; ⊢ C \atop Γ, A, Δ, B; ⊢ C} & W \\ Γ, A, Δ; ⊢ B →C \end{matrix} ; Imp_{R}
{Γ, Δ, B, Ω; B ⊢ C \atop Γ, Δ, B, Ω; ⊢ C} Cont

Γ, A, Δ, B, Ω; ⊢ C W \underrightarrow{LJT} {Γ, Δ, B, Ω; B ⊢ C \atop Γ, A, Δ, B, Ω; B ⊢ C} W Γ, A, Δ, B, Ω; ⊢ C Cont

{Γ, B, Δ, Ω; B ⊢ C \atop Γ, B, Δ, Ω; ⊢ C} Cont

Γ, B, Δ, A, Ω; ⊢ C W \underrightarrow{LJT} {Γ, B, Δ, Ω; B ⊢ C \atop Γ, B, Δ, A, Ω; B ⊢ C} W Γ, B, Δ, A, Ω; ⊢ C Cont

Note that, as before, since the system is left linear and without critical pairs, it is confluent.

13.3 Assignment by terms with de Bruijn indices

We show the correspondence between the \overline{λ}-terms with de Bruijn indices and the proofs for the calculus with an explicit weakening rule.

Applicative context formation rules

Empty list of arguments  Γ; . :A ⊢ (. [ ]):A Ax
Addition of an argument  \begin{matrix}Γ; ⊢ u:A & Γ; . :B ⊢ (. l):C \\ Γ; . :A→B ⊢ (. [u :: l]):C \end{matrix} Imp_{L}
Concatenation of list of arguments \begin{matrix}Γ; . :C ⊢ (. l):A & Γ; . :A ⊢ (. l′):B \\ Γ; . :C ⊢ (. (l @ l′)):B \end{matrix} Cut_{H}
Substitution in list of arguments \begin{matrix}Γ, Δ; ⊢ u:A & Γ, A, Δ; . :C ⊢ (. l):B \\ Γ, Δ; . :C ⊢ (. l[n := u]):B \end{matrix} Cut_{M}
Lifting for arguments  {Γ, Δ; Π ⊢ (. l):B \atop Γ, A, Δ; Π ⊢ (. l ↑_{n}):B} W

Term formation rules

Weakly normal applicative term  {Γ, A, Δ; . :A ⊢ (. l):B \atop Γ, A, Δ; ⊢ (n l):B} Cont

Abstraction  {Γ, A; ⊢ u:B \atop Γ; ⊢ λu:A→B} Imp_{R}

Non weakly normal applicative term \begin{matrix}Γ; ⊢ u:A & Γ; . :A ⊢ (. l):B \\ Γ; ⊢ (u l):B \end{matrix} Cut_{H}

Substitution in terms  \begin{matrix}Γ, Δ; ⊢ u:A & Γ, A, Δ; ⊢ v:B \\ Γ, Δ ⊢ v[n := u]:B \end{matrix} Cut_{M}

Lifting for terms  {Γ, Δ; Π ⊢ u:B \atop Γ, A, Δ; Π ⊢ u↑_{n}:B} W

where in each rules involving Δ and n, this latter is the length of Δ.

A \overline{λ}-term with de Bruijn indices such that there exists formulas A_{1}, ..., A_{n} and A such that u is the assignment of a proof of A_{1}, ..., A_{n} ⊢ A is said simply-typable of type A.

13.4 Cut-elimination

The cut-elimination includes now the elimination of the weakening rule too.

Definition 35 We call normal a proof without cut and without weakening rule.

Proposition 4 (Strong and confluent cut-elimination) There exists a confluent system of rewriting rules which allows to derive a normal proof of Γ; Π ⊢ A from any proof of the same sequent.

The system of rewriting rules has been given above. As for the proof of strong termination, we do not give it here since it appears as a restriction of the proof of strong termination for the cut-elimination in LKT. This latter proof is done in the next section.

14 Acknowledgments

I thank Thierry Coquand for his helpful and pertinent remarks. Especially, it is Coquand’s idea to do induction on the proof of strong E-normalisability rather than to do successive inductions on the future normal form then on the proof of strong normalisability, as I did in a first version of the proof.

Our first version of reduction rules for the calculus with de Bruijn indices was erroneous. I thank Phil Wadler for having pointed it out.

References

[1] V. Breazu Tanen, D. Kesner, L. Puel, A typed pattern calculus, IEEE Symposium on Logic in Computer Science, Montréal, Canada, June 1993, pp 262-274.

[2] V. Danos, J-B. Joinet, H. Shellinx, A new Deconstructive Logic: Linear Logic, to appear in the proceedings of the Workshop on Linear Logic, Cornell, edited by J-Y. Girard, Y. Lafont, L. Régnier, 1993.

[3] A. G. Dragalin, Mathematical Intuitionism: Introduction to Proof Theory, Translations of mathematical monographs, Vol 67, Providence, R.I.: American Mathematical Society, 1988.

[4] M. Felleisen, Reasoning About Continuations, proceedings of LICS, 1986.

[5] , J. Gallier, Constructive logics, part I: A tutorial on proof systems and typed λ-calculi, Theoretical Computer Science, Vol 110, 1993, pp 249-339.

[6] J-Y. Girard, On the Unity of Logic, Annals of Pure and Applied Logic, Vol 59, pp 201-217.

[7] G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, Journal of the Association for Computing Machinery, Vol 27, 1980, pp 797-821.

[8] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1988.

[9] G. Kreisel, A Survey of Proof Theory II, in Proceedings of the Second Scandinavian Logic Symposium, Fenstad J. Ed, North Holland, 1971.

[10] G. Mints, Reference not yet available, 1993.

[11] M. Parigot, λ-μ-calculus: an Algorithmic Interpretation of Classical Natural Deduction, Springer Lecture Notes in Computer Sciences 624, pp 190-201.

[12] G. Pottinger, Normalization as a homomorphic image of cut-elimination, Annals of mathematical logic (now Annals of Pure and Applied Logic), Vol 12, 1977, pp 323-357.

[13] D. Prawitz, Natural Deduction, a Proof-Theoretical Study, Almquist and Wiksell, Stockholm, 1965, pp 90-91

[14] A. S. Troelstra, Lectures in Linear Logic, CSLI Lecture Notes, number 29, 1991.

[15] P. Wadler, A Curry-Howard isomorphism for sequent calculus, Private communication, 1993.

[16] J. I. Zucker, Correspondence between cut-elimination and normalization, part I and II, Annals of mathematical logic (now Annals of Pure and Applied Logic), Vol 7, 1974, pp 1-156.

Contents

1 Introduction 2 1.1 Informal introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 The usual interpretation of LJ cut-free proofs by normal λ-terms . . . . . . . . . . . . . . . . 2 1.3 Towards the calculus LJT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Cut and reduction rules: towards the \overline{λ}-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.5 Digression: how to recover LJ ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 The \overline{λ}-calculus 5 2.1 The \overline{λ}-expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Normal \overline{λ}-expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Reduction rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

3 The calculus LJT 7 3.1 Formulas and sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.2 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Cut-elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 The assignment of proofs in LJT by \overline{λ}-expressions 10

5 Strong termination 11 6 Related works 13

7 Conclusion 14

8 Extension to classical logic 15 8.1 The \overline{λ}μ-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 8.2 The calculus LKT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 8.3 How to recover LK ? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 8.4 Strong termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 8.5 The \overline{λ}μ-calculus with De Bruijn indices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 8.6 The calculus LKT with weakening rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 8.7 Strong termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 8.8 \overline{λ}_{C}-calculus and LJT + ¬¬A→A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

9 Extension to disjunction, injections and the case operator 22 9.1 The \overline{λ}-calculus with injections and the case operator . . . . . . . . . . . . . . . . . . . . . . . 22 9.2 The calculus LJT with ∨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 9.3 The term assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

10 Extension to conjunction, pair, projections and the splitting operator 23 10.1 The \overline{λ}-calculus with pair, projections and the splitting operator . . . . . . . . . . . . . . . . . 23 10.2 The calculus LJT with ∧ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 10.3 The term assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

11 Extension to quantifiers and to product and sigma operators 24 11.1 The \overline{λ}-calculus with product and sigma operators . . . . . . . . . . . . . . . . . . . . . . . . . 25 11.2 The calculus LJT with quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

12 The full isomorphism 26

13 An isomorphism for the \overline{λ}-calculus with De Bruijn indices 26 13.1 The \overline{λ}-calculus with De Bruijn indices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 13.2 The calculus LJT with a weakening rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 13.3 Assignment by terms with de Bruijn indices . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 13.4 Cut-elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

14 Acknowledgments 31