The duality of computation

Hugo Herbelin INRIA-Futurs, Palaiseau, France

(based on joint work with Pierre-Louis Curien)

WoLP 2004 - Créteil

Contents

Introduction

- Call-by-name vs Call-by-value

- Computational content of Gentzen’s sequent calculus ?

- The symmetry of Gentzen’s sequent calculus

- The legacy of Parigot’s λμ-calculus

I - A computational content for LJ

- Interpreting left introduction of implication

- LJT and the \overline{λ}-calculus

- LJ and let-in

- Call-by-name vs Call-by-value in LJ

- Tree-like presentation of LJ

II - A computational content for LK

- LK and the \overline{λ}μμ̃-calculus

- Call-by-name vs Call-by-value in LK

- The duality of computation

- Tree-like presentation of LK

Introduction

3

Call-by-name vs Call-by-value

Usual λ-calculus is call-by-name λ-calculus

t, u ::= x | λx.t | t u  Terms

Call-by-name reduction

(λx.t) u ⟶_{β} t[x := u]

Call-by-value λ-calculus distinguishes values and non-values

V ::= x | λx.t  Values
t, u ::= V | t u  Terms

Call-by-value reduction: arguments must be evaluated before application

(λx.t) V ⟶_{β_{v}} t[x := V]

Plotkin 1975 defined the call-by-value λ-theory: the λ_{v}-calculus. It has more normal forms than usual (callby-name) λ-calculus. E.g.

(λx.t) (y u)

is normal as soon as t and u are. Moggi 1989 defined the computational λ-calculus and introduced a let-in construct to characterize the

equational call-by-value λ-theory. E.g.

NF ((λx.t)(y u)) is let x = y u in t

Call-by-value is commonly considered dual to call-by-name, how to syntactically characterize this duality?

Computational content of Gentzen’s sequent calculus

Sequent calculus A mixed version of original Gentzen’s intuitionistic LJ sequent calculus and Kleene’s G3

Natural deduction

Γ weakening rule moved to the axiom ... , A ⊢ A Ax  Γ, x : A ⊢ x : A Ax

\begin{matrix}Γ, A ⊢ B \\ Γ ⊢ A → B \end{matrix} →_{R}  \begin{matrix}Γ, x : A ⊢ t : B \\ Γ ⊢ λx.t : A → B \end{matrix} →_{I}

\begin{matrix}Γ ⊢ A Γ, B ⊢ C \\ Γ, A → B ⊢ C \end{matrix} →_{L}  \begin{matrix}Γ ⊢ t : A Γ ⊢ u : A → B \\ Γ ⊢ t u : B \end{matrix} →_{E}

Γ, A, A ⊢ C Γ, A ⊢ C

Cont_{L}

... but an explicit contraction rule

\begin{matrix}Γ ⊢ A Γ, A ⊢ C \\ Γ ⊢ C \end{matrix} Cut

Breazu-Tanen–Kesner–Puel 1993: left introduction rules build patterns Herbelin 1994: left introduction rules (essentially) build evaluation contexts

The symmetry of classical Gentzen’s sequent calculus

Sequent calculus for classical logic:

- axiom and cut rules are symmetric

- introduction rules for disjunction and conjunction are dual How does this symmetry show up on the computational interpretation? See Barbanera-Berardi λ_{sym}-calculus which implements a one-sided version of sequent calculus with disjunction

and conjunction (1996).

How does natural deduction interpret classical proofs: Parigot’s classical natural deduction

The computational interpretation of classical natural deduction distinguishes the active formula on the righthand-side of the sequent.

Γ, x : A ⊢ x : A ; Δ Ax

\begin{matrix}Γ, x : A ⊢ t : B ; Δ \\ Γ ⊢ λx.t : A → B ; Δ \end{matrix} →_{R}  \begin{matrix}Γ ⊢ t : A ; Δ Γ ⊢ u : A → B ; Δ \\ Γ ⊢ t u : B ; Δ \end{matrix} →_{L}

\begin{matrix}Γ ⊢ t : A ; α : A, Δ \\ Γ ⊢ [α]t ; α : A, Δ \end{matrix} Cont_{R}  \begin{matrix}c : (Γ ⊢ α : A, Δ) \\ Γ ⊢ μα.c : A ; Δ \end{matrix} μ
t, u ::= x | λx.t | t u | μα.c  Terms

c ::= [α]t Commands

Called unnamed terms in Parigot

Can we distinguish a formula to the left-hand-side of the sequents?

Sequent calculus has more proofs than natural deduction

LJ \underrightarrow{many-one} LJT ⟷ NJ

LJT: the image of NJ within LJ Implicitly considered by Mints. Identified and named by Danos-Joinet-Schellinx 1995. To what correspond the extra proofs of LJ?

Results of this talk

- Left introduction rules build evaluation contexts

- Syntactic duality between terms and evaluation contexts Syntactic duality between call-by-name and call-by-value - The “dark” side of sequent calculus is the call-by-value side - A tree-like presentation of LJ and LK

References: Herbelin 1994 and Curien-Herbelin 2000

I - A computational content for LJ

10

Interpreting left introduction of implication

How to interpret implication left introduction rule?

\begin{matrix}Γ ⊢ t : A Γ, x : B ⊢ u : C \\ Γ, y : A → B ⊢ ? : C \end{matrix}

Introduce a distinguished formula on the left-hand-side! Two kinds of sequents:

Γ ⊢ A for terms
Γ ; A ⊢ B for lists of arguments

Interpret a sequent with a distinguished formula on the left-hand-side as a typing rule for list of arguments.

\begin{matrix}Γ ⊢ t : A Γ ; l : B ⊢ C \\ Γ ; t l : A → B ⊢ C \end{matrix} →_{L}

Read Γ ; l : A ⊢ B as the typing derivation of an evaluation context: Γ ; [ ] : A ⊢ [ ] l : B.

Interpreting the cut rule

The new kind of sequent suggests the following new version of the cut rule

\begin{matrix}Γ ⊢ t : A Γ ; l : A ⊢ B \\ Γ ⊢ t · l : B \end{matrix} Cut

I.e. the cut rule makes a function t interact with a list of arguments l.

Interpreting the axiom rule

The axiom rule naturally builds an empty list of arguments, that we write ⋆.

Γ ; ⋆ : A ⊢ A Ax

Interpreting the left contraction rule

We have two choices for interpreting the left contraction rule. 1st choice (Herbelin 1994) The contraction rule builds normal applicative terms x l.

\begin{matrix}Γ, x : A ; l : A ⊢ B \\ Γ, x : A ⊢ x · l : B \end{matrix} Cont

The corresponding syntax of terms (\overline{λ}-calculus in Herbelin 1994) is

t, u ::= x l contraction | λx.t→_{R} | t · l cut Terms
l ::= ⋆ axiom | t l →_{L}  Lists of arguments

Advantage: “normal = cut-free” Slight disadvantage: x is not a term any longer. Its natural encoding is x().

Interpreting the left contraction rule

2nd choice (Curien-Herbelin 2000) Add a second axiom rule

Γ, x : A ⊢ x : A Ax_{R}

and derive contraction from cut

\begin{matrix}Γ, A ; A ⊢ B \\ Γ, A ⊢ B \end{matrix} Cont =^{△} \begin{matrix}Γ, x : A ⊢ x : A Ax_{R} Γ, x : A; l : A ⊢ B \\ Γ, x : A ⊢ x · l : B \end{matrix} Cut

The corresponding syntax of terms is

t, u ::= x right axiom rule | λx.t | t · l  Terms
l ::=\begin{matrix}⋆ \\ left axiom rule \end{matrix} | t l  Lists of arguments

Disadvantage: normal ≠ cut-free. We only have: “normal = constructive cut only” where a constructive cut is a cut between an axiom and an introduction rule or between two axiom rules.

Advantage 1: closer from natural deduction and enjoys a tree-form representation. Advantage 2: scales to a dual classical version

The sequent calculus LJT

The resulting calculus is essentially LJT. Example: the encoding of λx.(y x) : A → B is λx.(y · (x⋆))

\begin{aligned}Γ′, x : A ⊢ y : A → B & Ax_{R} & \begin{matrix}Γ′, x : A ⊢ x : A & Ax_{R} & Γ′, x : A ; ⋆ : B ⊢ B & Ax_{L} \\ Γ′, x : A ; x⋆ : A → B ⊢ B \end{matrix} & →_{L} \\ \begin{matrix}Γ′, x : A ⊢ y · (x⋆) : B \\ Γ′ ⊢ λx.(y · (x⋆)) : B \end{matrix} & →_{R} \end{aligned}Cut

where Γ′ is Γ, y : A → B. LJT is the image of NJ within LJ. Its normal forms are isomorphic to the normal forms of natural deduction.

\begin{aligned}x & ⟷ & x \\ λx.t & ⟷ & λx.t \\ (...(x t_{1}) … t_{n}) & ⟷ & x · (t_{1} … t_{n} ⋆) \end{aligned}

Non-normal forms map canonically

(...((λx.t) t_{1}) … t_{n}) ⟷ (λx.t) · (t_{1} … t_{n} ⋆)

but there are more non-normal forms in LJT than in NJ

The reduction rules of LJT

(λx.t) · (u l) ⟶ t[x := u] · l β-reduction
(t · l) · l′  ⟶ t · (ll′)  list concatenation
x · ⋆  ⟶ x  simplification
λx.t · ⋆  ⟶ λx.t  simplification

The tree-like presentation of LJT

Two kinds of nodes ⊢ t : A for terms l : A ⊢ for lists of arguments

Leaves have the form ⊢ t : A or ⋆ : A ⊢. They can be “bracketed”. Construction rules are

[⊢ x : A] ; ⋮ ; ⊢ t : B ; ⊢ λx.t : A → B →_{R}  \begin{matrix}⊢ t : A l : B ⊢ \\ t l : A → B ⊢ \end{matrix} →_{L}

\begin{matrix}⊢ t : A [⋆ : B ⊢] ; ⋮ ; l : A ⊢ \\ ⊢ t · l : B \end{matrix} Cut

The tree-like presentation of LJT

Example: the encoding of λx.(y x) : A → B is λx.y · (x⋆)

\begin{matrix}⊢ y : A → B \begin{matrix}[⊢ x : A] [⋆ : B ⊢] \\ x⋆ : A → B ⊢ \end{matrix} →_{L} \\ \begin{matrix}⊢ y · (x⋆) : B \\ ⊢ λx.(y · (x⋆)) : B \end{matrix} & →_{R} \end{matrix}Cut

The missing part of LJ

Normal forms of LJT have the following form

\begin{matrix}Γ ⊢ y : B⃗ → A Ax_{R} & \begin{matrix}Γ ; ⋆ : A ⊢ A & Ax_{L} \\ ⋮ . →_{L} \end{matrix} ; Γ ; l : B⃗ → A ⊢ A \\ Γ ⊢ y · l : A \end{matrix} ; Cut ; ⋮ . →_{R} ; Γ′ ⊢ λx_{1} … x_{n}.y · l : C⃗ → A

There is no way to interpret

\begin{matrix}Γ ⊢ t : A Γ, x : B ⊢ u : C \\ Γ, y : A → B ⊢ ? : C \end{matrix}

The missing rule is a rule “activating” an hypothesis of the context

{Γ, x : A ⊢ B \atop Γ ; ? : A ⊢ B}

Such a rule implements a let-in evaluation context.

{Γ, x : A ⊢ t : B \atop Γ ; let x = [ ] in t : A ⊢ B} Letin

Then we can derive full LJ implication left introduction.

Γ ⊢ t : A Γ, x : B ⊢ u : C Γ, y : A → B ⊢ let x = y · t in u : C

The let-in evaluation context

The let-in constructor is dual to Parigot’s μ operator. Let’s write μ̃x.u for let x = [ ] in u. This notation allows to concatenate evaluation contexts and avoids to have to nest them.

The full LJ implication left introduction rewrites as follows:

\begin{matrix}Γ, y : A → B ⊢ y : A → B Ax_{R} & {Γ ⊢ t : A {Γ, x : B ⊢ u : C \atop Γ ; μ̃x.u : B ⊢ C} Letin \atop Γ ; t μ̃x.u : A → B ⊢ C} ; →_{L} \\ Γ, y : A → B ⊢ y · t μ̃x.u : C \end{matrix} ; Cut

The extended syntax is

t, u ::= x | λx.t | t · l  Terms
l ::= ⋆ | t l | μ̃x.t  Lists of arguments

Separating call-by-name and call-by-value reduction

Thanks to the let-in construction, β-reduction can be refined into β-contraction and let-in-reduction.

(λx.t) · (u l) ⟶ (u · μ̃x.t) · l  β-contraction
(t · l) · l′  ⟶ t · (ll′)  concatenation of evaluation contexts
x · ⋆  ⟶ x  simplification
λx.t · ⋆  ⟶ λx.t  simplification
u · μ̃x.t  ⟶ t[x := u]  μ̃

But there is now a critical pair!

(t · l) · μ̃x.u
↙  ↘
t · (lμ̃x.u)  u[x := (t · l)]

Giving preference to the left-hand side implements call-by-value: only values can be substituted within let-in, hence, full β-reduction (not just β-contraction) applies only to values.

Giving preference to the right-hand side implements call-by-name as before.

The tree-like presentation of let-in

Expressed in tree-form, the let-in rule is

\begin{matrix}[⊢ x : A] ; ⋮ ; ⊢ t : B ⋆ : B ⊢ \\ μ̃x.t : A ⊢ \end{matrix} Letin

Thanks to let-in, new normal forms occur that are call-by-value normal form. E.g., the derivation of let x = y u in t which indeed corresponds to the full form of implication left introduction.

Remark: For t and u normal, (y · t ⋆) · μ̃x.u is not normal, it reduces to the normal form y · (t μ̃x.u) along call-by-value reduction and to u[x := (y · t ⋆)] along call-by-name reduction.

II - A computational content for LK

24

Sequent calculus with multiple conclusions

As in Parigot’s λμ-calculus, we

- name conclusions with lowercase Greek letters

- distinguish a formula on the right for the rules building terms

- introduce a sequent c : (Γ ⊢ Δ) for commands, with no distinguished formulae at all Let’s re-interpret the previous formulation of LJ with multiple conclusions. The implication right introduction rule builds a term, it extends directly to multiple conclusions as in λμ-

calculus.

\begin{matrix}Γ, x : A ⊢ t : B; Δ \\ Γ ⊢ λx.t : A → B; Δ \end{matrix} →_{R}

The implication left introduction rule and the right axiom rule extend easily.

\begin{matrix}Γ ⊢ t : A ; Δ Γ ; l : B ⊢ Δ \\ Γ ; t l : A → B ⊢ Δ \end{matrix} →_{L}
Γ, x : A ⊢ x : A, Δ Ax_{R}

Sequent calculus with multiple conclusions: the Cut rule

The cut rule used to build a term. In a symmetric calculus, there is no reason it builds a term rather than an evaluation context. It should build a command.

\begin{matrix}Γ ⊢ t : A; Δ Γ ; l : A ⊢ Δ \\ t · l : (Γ ⊢ Δ) \end{matrix} Cut

Sequent calculus with multiple conclusions: many continuation variables

With multiple conclusions, it is possible to switch the evaluation contexts. Let’s add the μ rule as in λμ-calculus.

\begin{matrix}c : (Γ ⊢ α : A, Δ) \\ Γ ⊢ μα.c : A ; Δ \end{matrix} μ

We now need to re-interpret the meaning of the empty list of arguments. In LJ, it tells that there are no more argument to apply and that the computation can go on with the surrounding context. The direct generalisation to sequent calculus with multiple conclusion is to go on with a given named evaluation context denoted by a continuation variable.

This leads to the following rephrasing of the left axiom rule, dual to the right axiom rule.

Γ; α : A ⊢ α : A, Δ Ax_{L}

Finally, we can restate the let-in rule. By symmetry with the μ rule, we make it take a command as argument.

{c : (Γ, x : A ⊢ Δ) \atop Γ ; μ̃x.c : A ⊢ Δ} μ̃

Re-interpreting LJ within LK

LJ is LK with a single continuation variable, written ⋆ (like the empty list of argument). LK gives a finer analysis of the previous constructions as follows:

\begin{matrix}LJ & LK \\ x & x \\ λx.t & λx.t \\ t · l & μ ⋆ .(t · l) \\ ⋆ & ⋆ \\ μ̃x.t & μ̃x.(t · ⋆) \end{matrix}

Injecting natural deduction

Injecting usual λ-calculus is as before except that we cannot just use the single continuation variable ⋆. We need a fresh continuation variable α.

\begin{matrix}NJ & LK \\ x & x \\ λx.t & λx.t \\ x t_{1} … t_{n} & μα.(x · t_{1} … t_{n} α) \\ (λx.t) t_{1} … t_{n} & μα.((λx.t) · t_{1} … t_{n} α) \end{matrix}

On normal forms, the injection from λμ-calculus is

\begin{matrix}CND & LK \\ λx_{1} … x_{m}.μγ[β](y t_{1} … t_{n}) & λx_{1} … x_{m}.μγ.(y · (t_{1} … t_{n} β)) \\ λx_{1} … x_{m}.(y t_{1} … t_{n}) & λx_{1} … x_{m}.μα.(y · (t_{1} … t_{n} α)) \end{matrix}

Reduction rules

The reduction rules are symmetrical in LK:

(λx.t) · (u l) ⟶ u · μ̃x.(t · l)  β-contraction
(μα.t) · l  ⟶ t[α := l]  μ
u · (μ̃x.t) ⟶ t[x := u]  μ̃
μα.(V · α) ⟶ V  simplification (α not free in V)
μ̃x.(x · L) ⟶ L  simplification (x not free in L)

where

V ::= x | λx.t  Values
L ::= α | tl  Applicative evaluation contexts

Note that the substitution work is done by the rules μ and μ̃ only. The critical pair now expresses symmetrically.

(μα.c) · (μ̃x.c′)

↙  ↘
c[α := μ̃x.c′]  c′[x := μα.c]

Call-by-value and call-by-name

Giving preference to the left-hand side implements call-by-value. Typically, a configuration like

(λx.t)(μα.c)

is interpreted in LK as

μβ.((λx.t) · ((μα.c)β))

which reduces to

μβ.((μα.c) · μ̃x.(t · β))
CBV ↙  ↘ CBN
μβ.c[α := μ̃x.(t · β)]  t[x := μα.c]

Example: reduction of μβ.[β]((λx.3)(μα.[β]4))

μβ.(λx.3 · ((μα.[β]4) β))

CBV ↙  ↘ CBN
4  3

Summary

The resulting sequent calculus is essentially LK in the sense that there is a correspondence with Gentzen’s LK that preserves the structure of introduction rules.

Γ; α : A ⊢ α : A, Δ Ax_{L}  Γ, x : A ⊢ x : A, Δ Ax_{R}
\begin{matrix}Γ ⊢ t : A ; Δ Γ ; l : B ⊢ Δ \\ Γ ; t l : A → B ⊢ Δ \end{matrix} →_{L} \begin{matrix}Γ, x : A ⊢ t : B; Δ \\ Γ ⊢ λx.t : A → B; Δ \end{matrix} →_{R}
{c : (Γ, x : A ⊢ Δ) \atop Γ ; μ̃x.c : A ⊢ Δ} μ̃  \begin{matrix}c : (Γ ⊢ α : A, Δ) \\ Γ ⊢ μα.c : A ; Δ \end{matrix} μ
\begin{matrix}Γ ⊢ t : A Γ ; l : A ⊢ Δ \\ t · l : (Γ ⊢ Δ) \end{matrix} Cut

The \overline{λ}μμ̃-calculus

t, u ::= x | λx.t | μα.c  Terms
l ::= α | t l | μ̃x.c  Evaluation contexts
c ::= t · l  Commands

The tree-like presentation of LK

The resulting sequent calculus is essentially LK in the sense that removing the “;” yields a proof of LK extended with the identity rule. It enjoys a tree-like presentation.

\begin{matrix}\begin{matrix}⊢ t : A l : B ⊢ \\ t l : A → B ⊢ \end{matrix} →_{L} & [⊢ x : A] ; ⋮ ; ⊢ t : B ; ⊢ λx.t : A → B →_{R} \\ [⊢ x : A] ; ⋮ ; c ; μ̃x.c : A ⊢ μ̃ & [α : A ⊢] ; ⋮ ; c ; ⊢ μα.c : A μ \\ \begin{matrix}⊢ t : A l : A ⊢ \\ t · l \end{matrix} & Cut \end{matrix}