λρ-calculus^{∗}

Yuichi Komori

              komori@math.s.chiba-u.ac.jp

Department of Mathematics, Faculty of Sciences, Chiba University

Arato Cho

             aratoc@g.math.s.chiba-u.ac.jp

Department of Mathematics, Faculty of Sciences, Chiba University

In [K02], one of the authors has posed a new system λρ-calculus and stated without proof that the strong normalization theorem hold. We will give a proof of it. While the type assignment system T A_{λ} gives a natural deduction for intuitionistic implicational logic (cf. [H97]), T A_{λρ} gives a natural deduction for classical implicational logic. Our system is simpler than Parigot’s λμ-calculus (cf. [P92]).

1 The type free λρ-calculus

Definition 1.1 (λρ-terms). An infinite sequence of λ-variables is assumed to be given, and an infinite sequence of ρ-variables is assumed to be given. Then linguistic expressions called λρ-terms are defined thus:

1. each λ-variable is a λρ-term, called an atom or atomic term;

2. if M and N are λρ-term then (MN) is a λρ-term called an application;

3. if M is a λρ-term and a is a ρ-variable then (aM) is a λρ-term called an absurd;

4. if M is a λρ-term and f is a λ-variable or a ρ-variable then (λf.M) is a λρ-term called an abstract. (If f is a λ-variable or a ρ-variable, then it called a λ-abstract or a ρ-abstract respectively.)

λ-variables are denoted by u, v, w, x, y, z, with or without number-subscripts. ρ-variables are denoted by a, b, c, d, with or without number-subscripts. A termvariable means a λ-variable or a ρ-variable. Term-variables are denoted by f, g, h, with or without number-subscripts. Distinct letters denotes distinct variables unless otherwise stated.

∗This article is an abstract and details will be published elsewhere.

A term λa.M is sometimes denoted by ρa.M if the variable a is a ρ-variable. Arbitrary λρ-terms are denoted by L, M, N, P, Q, R, S, T, with or without

number-subscripts. For λρ-term we shall say just term.

F V (M) is the set of all variables free in M. For example, F V (λxb.a(x(by))) = {a, y}.

Definition 1.2 (βρ-contraction). A βρ-redex is any λρ-term of form (aM)N, (λx.M)N or (λa.M)N; its contractum is (aM), [N/x]M or λa.([λx.a(xN)/a]M)N respectively. The re-write rules are

(aM)N ⊳_{1βρ} (aM),
(λx.M)N ⊳_{1βρ} [N/x]M,
(λa.M)N ⊳_{1βρ} λa.([λx.a(xN)/a]M)N.

If P containd a βρ-redex-occurence \underline{R} and Q is the result of replacing this by its contractum, we say P βρ-contracts to Q (P ⊳_{1βρ} Q).

The notion of βρ-reduction and the notation P ⊳_{βρ} Q are defined as usual.

Theorem 1.3 (Church-Rosser threorem for βρ-reduction). If M ⊳_{βρ} P and M ⊳_{βρ} Q, then there exists T such that

P ⊳_{βρ} T and Q ⊳_{βρ} T.

Proof. Simmlar to the case of β-reduction, see [HS86]. ■

2 Assgning types to terms

Definition 2.1 (Types). An infinite sequence of type-variables is assumed to given, distinct from the term-variables. Types are linguistic expressions defined thus:

1. each type-variable is a type called an atom;

2. if σ and τ are types then (σ → τ) is a type called a composite type.

Type-variables are denoted by p, q, r with or without number-subscripts, and distinct letters denote distinct variables unless otherwise stated.

Aribitrary types are denoted by lower-case Greek letters except λ and ρ. Parentheses will often (but not always) be omitted from types, and the reader

should restore omitted ones in the way of association to the right.

Definition 2.2 (Type-assignment). A type-assignment is any expression

M : τ

where M is a λρ-term or a ρ-variable and τ is a type; we call M its subject and τ is its predicate.

Definition 2.3 (The system T A_{λρ}). T A_{λρ} is a Natural Deduction system. Its formulas are type-assignments. T A_{λρ} has no axioms and has four rules called (→ E), (→ I), (Absurd) and (Rati), as follows.

Deduction rules of T A_{λρ}:

\begin{matrix}P : σ → τ & Q : σ \\ P Q : τ \end{matrix} (→ E), {x : σ \atop Π} ; P : τ ; λx.P : σ → τ (→ I),

\begin{matrix}a : τ & P : τ \\ aP : σ \end{matrix} (Absurd), {a : τ \atop Π} ; P : τ ; λa.P : τ (Rati).

Example 2.4 (Peirce’s Law).

\begin{matrix}y : (α → β) → α & \begin{matrix}\begin{matrix}a : α & x : α \\ ax : β \end{matrix} & (Absurd) \\ λx.ax : α → β \end{matrix} ; (→ I) \\ y(λx.ax) : α \end{matrix} ; (→ E) ; λa.y(λx.ax) : α ; (Rati) ; λya.y(λx.ax) : ((α → β) → α) → α ; (→ I)

The above T A_{λρ}-deduction is writen in more compact style:

\begin{matrix}y : (α → β) → α & \begin{matrix}a : α & x : α \\ ax : β \end{matrix} ; α → β ; λx \\ α \end{matrix} ; (→ E) ; α ; ρa ; ((α → β) → α) → α ; λy

3 Strong Normalization Theorem for T A_{λρ}

βρ-reductions of deductions of T A_{λρ} correspond to βρ-reductions of λρ-terms. We prove the strong normalization theorem for deductions of T A_{λρ} ,that is, for every deduction of T A_{λρ} Π, all reductions starting at Π are finite. To prove the theorem, we introduce ∗-expansion and use the strong normalization theorem for deductions of T A_{λ}.

Definition 3.1 (∘-translation). For every deduction of T A_{λρ}, of which the last rule is Rati, we define ∘-translation as follows:

1. Π^{∘} ≡ Π , where Π ≡ {Π \atop M : α} and α is an atomic type;

2. Π^{∘} ≡ {y : β \atop (Π_{2})^{∘}} ; N : γ ; λy.N : β → γ , where Π ≡ {a : β → γ \atop Π_{1}} ; M : β → γ ; λa.M : β → γ and

Π_{2} ≡ \begin{matrix}\begin{aligned}a : γ & \begin{matrix}x : β → γ & y : β \\ xy : γ \end{matrix} \\ & a(xy) : δ \end{aligned} ; λx.a(xy) : (β → γ) → δ ; [λx.a(xy)/a]Π_{1} ; [λx.a(xy)/a]M : β → γ & y : β \\ [λx.a(xy)/a]My : γ \end{matrix} ; λa.[λx.a(xy)/a]My : γ .

Definition 3.2 (∗-expansion). For every deduction of T A_{λρ}, we define ∗- expansion as follows:

1. (x : α)^{∗} ≡ x : α ;

2. Π^{∗} ≡ \begin{matrix}{(Π_{1})^{∗} \atop M^{∗} : α → β} & {(Π_{2})^{∗} \atop N^{∗} : α} \\ M^{∗}N^{∗} : β \end{matrix} , where Π ≡ \begin{matrix}{Π_{1} \atop M : α → β} & {Π_{2} \atop N : α} \\ MN : β \end{matrix} ;

3. Π^{∗} ≡ {x : α \atop (Π_{1})^{∗}} ; M^{∗} : β ; λx.M^{∗} : α → β , where Π ≡ {x : α \atop Π_{1}} ; M : β ; λx.M : α → β ;

4. Π^{∗} ≡ \begin{matrix}a : α & {(Π_{1})^{∗} \atop M^{∗} : α} \\ aM^{∗} : β \end{matrix} , where Π ≡ \begin{matrix}a : α & {Π_{1} \atop M : α} \\ aM : β \end{matrix} ;

5. Π^{∗} ≡ (Π_{1})^{∘} , where Π ≡ {a : α \atop Π_{2}} ; M : α ; λa.M : α and Π_{1} ≡ {a : α \atop (Π_{2})^{∗}} ; M^{∗} : α ; λa.M^{∗} : α .

Definition 3.3 (βa-reduction). A βa-reduction is a βρ-reduction which does not allow a contruction (λa.M)N ⊳_{1βρ} λa.([λx.a(xN)/a]M)N.

Theorem 3.4 (Strong normalization theorem for βa-reduction). For every deduction Π of T A_{λρ}, all βa-reductions starting at Π are finite.

Proof. Similar to the case of T A_{λ}, see [HS86]. ■

Theorem 3.5 (Strong normalization theorem for T A_{λρ}). For every deduction Π of T A_{λρ}, all βρ-reductions starting at Π are finite.

Proof. We can prove that (Π_{1})^{∗} ⊳_{1βa} (Π_{2})^{∗} if Π_{1} ⊳_{1βρ} Π_{2}. So we get a infinite sequence of βa-reductions from a infinite sequence of βρ-reductions. That is, strong normalization theorem for βa-reduction leads strong normalization theorem for T A_{λρ}. ■

References

[H97] J. Roser Hindley. Basic Simple Type Theory, Vol. 42 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1997.

[HS86] J. Roger Hindley and Jonathan P. Seldin. Introduction to combinators and λ-calculus, Vol. 1 of London Mathematical Society Student Texts, Cambridge University Press, 1986.

[P92] Michel Parigot. λμ-CALCULUS: AN ALGORITHMIC INTERPRETA-TION OF CLASSICAL NATURAL DEDUCTION, Lecture Notes in Computer Science 624, 190-201, 1992.

[K02] Yuichi Komori. λρ-Calculus: A Natural Deduction for Classical Logic, BULLETIN OF THE SECTION OF LOGIC, VOL. 31, No. 2, 65-70, 2002.