Investigations into the Duality of Computation

Hugo Herbelin

(INRIA-Futurs)

International Workshop on Higher-Order Rewriting

Seattle, August 15, 2006

(based on joint work with Pierre-Louis Curien [ICFP’ 00])

Outline

Introduction

An analysis of the underlying term structure of sequent calculus

- System μμ̃: the core of computation

- Adding connectives

- Typing system μμ̃

- Sequent calculus presented with implicit context

- Back to (untyped) system μμ̃: the call-by-name vs call-by-value dilemma

Further investigations

- “Canonical” call-by-name and call-by-value λ-calculi

- Applications to the study of call-by-value

- A dual to call-by-need

- Sequent calculus and the proof-as-strategy approach

- Sequent calculus and abstract machines

- A limit to duality: dependent types

Conclusion and problems

General research framework

proof theory  theory of computation
[figure]

proof-as-program correspondence Curry [1958] Howard [1969] (de Bruijn [1968])

intuitionistic natural deduction Gentzen [1936] = (call-by-name) λ-calculus

Church [1936]

classical logic = control operators

sequent calculus Gentzen [1936] = ?

[figure]

strategies in game-theoretic models of computation

left/right symmetry abstract machines (redex at root)

duality ⟶ a tool to revisit proof and computation theories

The μμ̃-subsystem: the core of computation

Computational properties

• syntactic emphasis of the call-by-name vs call-by-value duality,

• syntactic emphasis of a duality between term and evaluation contexts that interact to produce results,

• accepts extensions made by specific sets of interacting constructors,

• condenses all the computational aspects of its extensions

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x
Evaluation contextse ::= μ̃x.c || α

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

• a good tool to better understand the theory of call-by-value λ-calculus

• a uniform analysis of η-conversion,

• a close connection with abstract environment machines (redexes are at the head of the expressions), Proof-theoretical properties

• full Curry-Howard correspondence for sequent calculus (left introduction rules build evaluation contexts),

• the “dark side” of sequent calculus is the call-by-value side,

• context-implicit tree-like representation of sequent calculus.

The μμ̃-subsystem

Syntax of μμ̃^{→∧} (aka \overline{λ}μμ̃)

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || λx.v
Evaluation contextse ::= μ̃x.c || α || v · e

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \\ (→) & ⟨λx.v||v′ · e⟩ & → & ⟨v′||μ̃x.⟨v||e⟩⟩ \end{aligned}

Equivalent syntax in λμ-calculus

Commands  c ::= e[v]
Terms  v ::= μα.c || x || λx.v
Evaluation contextse[ ] ::= let x = [ ] in c || [α]([ ]) || e[[ ] v]

Rules in the syntax of λμ-calculus

(μ) e[μα.c]  → c[[α]v ← e[v]]
(μ̃) let x = v in c → c[x ← v]
(→) e[(λx.v)v′]  → let x = v′ in e[v]

Adding constructions: the example of abstraction and application

Syntax of μμ̃^{→∧} (aka \overline{λ}μμ̃)

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || λx.v
Evaluation contextse ::= μ̃x.c || α || v · e

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \\ (→) & ⟨λx.v||v′ · e⟩ & → & ⟨v′||μ̃x.⟨v||e⟩⟩ \end{aligned}

Equivalent syntax in λμ-calculus

Commands  c ::= e[v]
Terms  v ::= μα.c || x || λx.v
Evaluation contextse[ ] ::= let x = [ ] in c || [α]([ ]) || e[[ ] v]

Rules in the syntax of λμ-calculus

(μ) e[μα.c]  → c[[α]v ← e[v]]
(μ̃) let x = v in c → c[x ← v]
(→) e[(λx.v)v′]  → let x = v′ in e[v]

Other examples of connectives

Syntax of μμ̃^{→∧∨⊤⊥}

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || λx.v || (v, v) || ι_{1}(v) || ι_{2}(v) || 1
Evaluation contextse ::= μ̃x.c || α || v · e || π_{1} · e || π_{2} · e || [e, e]  || 0
Semantics of μμ̃^{→∧∨⊤⊥}

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \\ (→) & ⟨λx.v||v′ · e⟩ & → & ⟨v′||μ̃x.⟨v||e⟩⟩ \\ (∧) & ⟨(v_{1}, v_{2})||π_{j} · e⟩ & → & ⟨v_{j}||e⟩ \\ (∨) & ⟨ι_{j}(v)||[e_{1}, e_{2}]⟩ & → & ⟨v||e_{j}⟩ \end{aligned}

Typing the μμ̃-subsystem

(a sequent calculus structure)

- two axioms

- no contraction: simulated by cuts with the axioms

- three kinds of sequents \{ \begin{matrix}terms: distinguished formula on the right \\ ev. contexts: distinguished formula on the left \\ commands: no distinguished formula \end{matrix}

Γ, x : A ⊢ x : A | Δ Ax_{R} Γ | α : A ⊢ α : A, Δ Ax_{L}

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

\begin{matrix}Γ ⊢ v : A | Δ Γ | e : A ⊢ Δ \\ ⟨v||e⟩ : (Γ ⊢ Δ) \end{matrix} Cut

Typing extensions (e.g. implication connective)

\begin{matrix}Γ, x : A ⊢ v : B | Δ \\ Γ ⊢ λx.v : A → B | Δ \end{matrix} \begin{matrix}Γ ⊢ v : A | Δ Γ | e : B ⊢ Δ \\ Γ | v · e : A → B ⊢ Δ \end{matrix}

Typing the μμ̃-subsystem

(sequent calculus in context-free form)

Thanks to the absence of contraction, sequent calculus proofs can be represented à la natural deduction

\begin{matrix}[A ⊢] ; ⋮ ; ⊢ ; ⊢ A μ & [⊢ A] ; ⋮ ; ⊢ ; A ⊢ μ̃ \\ \begin{matrix}⊢ A A ⊢ \\ ⊢ \end{matrix} & Cut \\ [⊢ A] ; ⋮ ; ⊢ B ; ⊢ A → B →_{R} & \begin{matrix}⊢ A B ⊢ \\ A → B ⊢ \end{matrix} →_{L} \end{matrix}

The μμ̃-subsystem

(the critical dilemma of computation)

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || …
Evaluation contextse ::= μ̃x.c || α || …
Linear ev. contextsE ::= α || …

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

The critical pair

call-by-value ⟨μα.c||μ̃x.c′⟩  call-by-name
↙ (μ)  (μ̃) ↘
c[α ← μ̃x.c′]  c′[x ← μα.c]

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || …
Evaluation contextse ::= μ̃x.c || α || …
Linear ev. contextsE ::= α || …

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

The critical pair in the syntax of λμ-calculus

call-by-value  let x = μα.c in c′  call-by-name
↙ (μ)  (μ̃) ↘
c[[α]v ← let x = v in c′]  c′[x ← μα.c]

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || …
Evaluation contextse ::= μ̃x.c || α || …
Linear ev. contextsE ::= α || …

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

The critical pair

call-by-value ⟨μα.c||μ̃x.c′⟩  call-by-name
↙ (μ)  (μ̃) ↘
c[α ← μ̃x.c′]  c′[x ← μα.c]

The μμ̃-subsystem

(the call-by-name confluent restriction)

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || …
Evaluation contextse ::= μ̃x.c || E
Linear ev. contextsE ::= α || …

Semantics

\begin{aligned}(μ_{n}) & ⟨μα.c||E⟩ & → & c[α ← E] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

The solved critical pair

call-by-value ⟨μα.c||μ̃x.c′⟩  call-by-name
↙ (μ)  (μ̃) ↘
c[α ← μ̃x.c′]  c′[x ← μα.c]

The μμ̃-subsystem

(the call-by-value confluent restriction)

Syntax

Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || V
Evaluation contextse ::= μ̃x.c || α || …
Values  V ::= x || …

Semantics

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃_{v}) & ⟨V ||μ̃x.c⟩ & → & c[x ← V] \end{aligned}

The solved critical pair

call-by-value ⟨μα.c||μ̃x.c′⟩  call-by-name
↙ (μ)  (μ̃) ↘
c[α ← μ̃x.c′]  c′[x ← μα.c]

The μμ̃-subsystem

(two confluent symmetric restrictions)

μ_{n}μ̃-subsystem
Commands  c ::= ⟨v||e⟩
Terms  v ::= μα.c || x || …
Linear ev. contextsE ::= α || …
Evaluation contextse ::= μ̃x.c || E

\begin{aligned}(μ_{n}) & ⟨μα.c||E⟩ & → & c[α ← E] \\ (μ̃) & ⟨v||μ̃x.c⟩ & → & c[x ← v] \end{aligned}

μμ̃_{v}-subsystem
Commands  c ::= ⟨v||e⟩
Linear terms (= values)V ::= x || …
Terms  v ::= μα.c || V
Evaluation contexts e ::= μ̃x.c || α || …

\begin{aligned}(μ) & ⟨μα.c||e⟩ & → & c[α ← e] \\ (μ̃_{v}) & ⟨V ||μ̃x.c⟩ & → & c[x ← V] \end{aligned}

The principle of duality

Static duality

term  / evaluation context
value  / linear ev. context
term variable/ ev. context variable
Parigot’s μ / let-in context (μ̃)

Semantical duality

call-by-value / call-by-name
(μ̃_{v})  / (μ_{n})
(μ)  / (μ̃)

Connective-level duality

conjunction / disjunction
true  / false
implication / subtraction

A tool to transfer results from one side to the other side...

The computational-classical-logic lineage of μμ̃^{→}

The programming side  The proof theory side
Landin’s J [1964]  Prawitz [1965]
an operator to translate goto and labels  normalisation of natural deduction + ¬¬A → A

(no Curry-Howard)

Reynolds’ escape [1972] a syntactical variant of call-cc

Scheme’s catch/throw [1975] a static variant of Lisp’s catch/throw

Felleisen et al’s C [1986] abstract study of λ-calculus with control

↘  ↙

The Curry-Howard connection

Griffin [1990]

typing C of type ¬¬A → A

Parigot [1992]

a “clean” variant to λ_{C}-calculus: λμ-calculus

Connected works

Computational symmetry

- Barbanera-Berardi’s symmetric λ-calculus [1996]

- Filinski’s symmetric λ-calculus syntax [1988]

Call-by-name/call-by-value duality

- Filinski’s dual cont.-passing-style call-by-name and call-by-value semantics of his symmetric λ-calculus [1988]

- Selinger’s dual control and co-control categories modelling call-by-name and call-by-value λμ-calculi [2000]

The computational-content-of-sequent-calculus lineage of μμ̃^{→}

- Gentzen’s LK sequent calculus [1935]: various (implicitly weak) cut-elimination strategies of LK

- Dragalin [1979]: strong cut-elimination of LK Griffin’s stimulus: classical logic computes in real life

- Girard’s LC [1991]: associativity-and-commutativity-preserving ¬¬-translation of LK

- Danos-Joinet-Schellinx’s LKT/LKQ fragments of LK [1994]: intuition of a connection to call-by-name and call-by-value

- Barbanera-Berardi’s λ_{sym}-calculus [1996]: non-deterministic computational content (implicitly?) of sequent calculus

- Herbelin’s \overline{λ}-calculus [1994]: LJT and LKT as a λ-calculus

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

- Danos-Joinet-Schellinx’s analysis of the LK to LL embeddings [1995,1997]

- Urban-Bierman’s extension of Barbanera-Berardi’s strong normalisation method to an LK syntax [2000]

- Curien-Herbelin \overline{λ}μμ̃-calculus [2000]

- Lengrand’s λ_{ξ}-calculus [2003]: application of the duality-of-computation paradigm to Urban-Bierman’s LK syntax

- Wadler’s variant of \overline{λ}μμ̃-calculus based on disjunctions and conjunctions [2003]

The intuitionistic constraint

evaluation context variables are bound linearly

In extensions that don’t bind ev. context variables (e.g. the constructors of implication), this implies one can take a unique ev. context variable, say ⋆.

Example:

Syntax of intuitionistic μμ̃^{→}

Commands  c ::= ⟨v||e⟩ || ⟨v||⋆⟩
Terms  v ::= μ ⋆ .c v(e) || x || λx.v
Evaluation contextse ::= μ̃x.cv || v · ⋆ || v · e

In the intuitionistic case, =_{v} is a strict subset of =_{n}.

The μμ̃-subsystem

(η-conversions)

(η_{μ}) μα.⟨V ||α⟩ = V  α not free in V
(ημ̃) μ̃x.⟨x||E⟩ = E  x not free in E

Each extension comes with its own η-conversions. E.g., for the constructors of implication, we have

(η_{→}) λx.μα.⟨y||x · α⟩ = y

from which we derive

(η_{→n}) λx.μα.⟨v||x · α⟩ = v  x and α not free in v
(η_{→v}) λx.μα.⟨V ||x · α⟩ = V  x and α not free in V

Focus on \overline{λ}μ_{n}-calculus and \overline{λ}μ̃_{v}-calculus

\overline{λ}μ_{n}-calculus

\begin{aligned}c & ::= & ⟨v||E⟩ \\ v & ::= & μα.c || x || λx.v \\ E & ::= & α || v · E \end{aligned}

Reduction

(μ_{n}) ⟨μα.c||E⟩  → c[α ← E]
(→_{n}^{β}) ⟨λx.v||v′ · E⟩ → ⟨v[x ← v′]||E⟩

η-reduction (with usual constraints)

(η_{μ}) μα.⟨v||α⟩  → v
(η_{→n}^{R}) v  → λx.μα.⟨v||x · α⟩

Prop: \overline{λ}μ_{n}, David-Py λμ, and μ_{n}μ̃^{→}-calculi have isomorphic equations on commands and terms.

\overline{λ}μ̃_{v}-calculus

\begin{aligned}c & ::= & ⟨V ||e⟩ \\ V & ::= & x || λx.μα.c \\ e & ::= & α || V · e || μ̃x.c \end{aligned}

Reduction

(μ̃_{v}) ⟨V ||μ̃x.c⟩  → c[x ← V]
(→_{v}^{β}) ⟨λx.μα.c||V · e⟩ → c[x ← V][α ← e]

η-reduction (with usual constraints)

(ημ̃) μ̃x.⟨x||e⟩  → e
(η_{→v}^{R}) λx.μα.⟨V ||x · α⟩ → V

Prop: \overline{λ}μ̃_{v} and μμ̃\overrightarrow{v}-calculi have isomorphic equations on commands, values and contexts.

Consequences for call-by-value λ-calculus

Call-by-value interprets the “dark side” of sequent calculus. Conversely, sequent calculus gives to call-by-value its nobility. Call-by-value λ-calculus (natural deduction style) is complex to study_{A complete reduction system cbv λ-calculus operational rule (Plotkin [1975]) (β_{v}) (λx.v) V → v[x ← V] cbv λ-calculus sub-operational rule (Moggi [1988]) (let_{lift}) F [(λx.v) v′] → (λx.F [v]) v′ cbv λ-calculus observational rules (Moggi [1988]) (η_{v}) λx.(V x) → V x not free in V (η_{let}) (λx.E[x]) v → E[v] x not free in E cbv λμ-calculus extra operational rules (∗) (μ_{v}) F [μα.c] → μα.c[α ← [α]F] (μ_{var}) [α]μβ.v → v[β ← [α][ ]] cbv λμ-calculus extra sub-operational rule (∗) (μ_{let}) (λx.μα.[β]v) v′ → μα.[β]((λx.v) v′) cbv λμ-calculus extra observational rule (∗) (η_{μ}) μα.[α]v → v α not free in V Extra rule for confluence (μ_{v}^{η}) v μα.c → (λx.μα.c[α ← [α](x [ ])]) v (∗) inspired by Sabry-Felleisen [1993], Hofmann [1995] and Selinger [2000] complete axiomatics} . Can the duality foster further theoretical research on call-by-value? Böhm theorem, standardisation, complete confluent systems, ...

A dual to call-by-need ?

lazy call-by-value (call-by-need)

Commands  c ::= ⟨v||e⟩
Linear terms (= values)V ::= x || …
Terms  v ::= μα.c || V
Linear ev. contexts E ::= α || …
Evaluation contexts e ::= μ̃x.c || E

(μ_{n}) ⟨μα.c||E⟩ →_{lv} c[α ← E]
(μ̃_{v}) ⟨V ||μ̃x.c⟩  →_{lv} c[x ← V]
(μ_{lv}) ⟨μα.c||μ̃x.c′⟩ →_{lv} c[α ← μ̃x.c′] (∗)
(μ̃_{lv}) ⟨μα.c||μ̃x.c′⟩ →_{lv} c′  (∗∗)

(∗) if x “needed” in c′ (∗∗) if x ∉ F V (c′)

intuitionistic restriction observationally collapses to call-by-name

lazy call-by-name

Commands  c ::= ⟨v||e⟩
Linear terms (= values)V ::= x || …
Terms  v ::= μα.c || V
Linear ev. contexts E ::= α || …
Evaluation contexts e ::= μ̃x.c || E

(μ_{n}) ⟨μα.c||E⟩ →_{ln} c[α ← E]
(μ̃_{v}) ⟨V ||μ̃x.c⟩  →_{ln} c[x ← V]
(μ_{ln}) ⟨μα.c||μ̃x.c′⟩ →_{ln} c  (∗∗)
(μ̃_{ln}) ⟨μα.c||μ̃x.c′⟩ →_{ln} c′[x ← μα.c] (∗)

(∗) if α “needed” in c (∗∗) if α ∉ F V (c)

intuitionistic restriction operationally collapses to call-by-name

with control, all four reduction systems are observationally different

?

The proof-as-strategy approach

strategies in game model of computations are polarised normal proofs in some sequent calculus Lorenz-Lorenzen’s game semantics of provability strategies = cut-free proofs in LJQ/LKQ (Herbelin’s PhD [1995]) different possible polarisations of μμ̃-systems normal proofs decompose normal proofs along commands: yields (abstract) Böhm trees (Curien-Herbelin [1998]) ⟨x||E⟩ = “(” (question) with possible reactions determined by E ⟨V ||α⟩ = “]” (answer) with possible reactions determined by V game interaction = head reduction in an abstract machine (Danos-Herbelin-Regnier [1996])

= head reduction in μμ̃

intuitionistic restriction = well-bracketed parentheses (Lorenzen’s school [see Felscher 1986])

Simply-typed μ_{n}μ̃^{→ℕ}-system (μPCF) (Herbelin [1997], Laird [1997])

N → N interpreted as ?N^{⊥}⅋N ℕ interpreted as ? ⊕_{n} 1 maximal η_{→n}-expansion maximal η_{μ}-expansion of atoms

c ::= ⟨x_{i}^{j}||v_{1} · . . . · v_{p} · [n↦c_{n}]⟩ || ⟨n||α_{i}⟩

where v ::= λx_{1} … x_{n}.μα.c

c ::= \begin{matrix}(_{i}^{j} \\ ↙ ↘↘ \\ [_{0}^{1} … [_{0}^{p} )_{0}^{n} \end{matrix} || ]_{i}^{n}

Initial state

⟨x|| \overbrace{v_{1} · . . . · v_{p} · [n↦c_{n}]}^{Opponent}⟩ [x← \overbrace{|v|}^{P layer}]

Interaction rules

(→ μ_{n}) ⟨x_{i}^{j}||v⃗ · [n↦c_{n}]⟩ [σ] → c [x⃗←v⃗; α←[n↦c_{n}]; σ′]
(ℕ)  ⟨n||α_{i}⟩  [σ] → c_{n} [σ′]
σ(x_{i}^{j}) = (λx⃗.μα.c)[σ′] σ(α_{i}) = ([n↦c_{n}])[σ′]

Simply-typed μμ̃_{v}^{→ℕ}-system (μPCF_{v})

(Abramsky-McCusker [1997], Honda-Yoshida [1997], Laird [1998])

P → P interpreted as P^{⊥}⅋!P ℕ interpreted as ? ⊕_{n} 1 maximal η_{→v}-expansion and ημ̃-expansion needs new constructions λλn.v_{n} and n · e

c ::= ⟨x_{i}||V_{λ} · e⟩ || ⟨x_{i}||n · e⟩ || ⟨V_{λ}||α_{i}⟩ || ⟨n||α_{i}⟩

where \begin{matrix}V_{λ} ::= λx.μα.c || λλn.μα.c_{n} \\ e ::= μ̃x.c || [n↦c_{n}] \end{matrix}

c ::= \begin{matrix}(_{i}^{λ} \\ ↙ ↘ \\ [_{0}^{V}  )_{0}^{V} \end{matrix} || \begin{matrix}(_{i}^{n} \\ ↓ \\ )_{0}^{V} \end{matrix} || ]_{i}^{λ} || ]_{i}^{n}

Initial states

\begin{matrix}⟨ \overbrace{[ n ]}^{P layer} ||α⟩ & [α← \overbrace{[n↦c_{n}]}^{Opponent}] \\ ⟨λx.μα.c ||α⟩ & [α←V_{λ} · e] \\ ⟨λλn.μα.c_{n}||α⟩ & [α←n · e] \end{matrix}

Interaction rules

(→ μ) ⟨x_{i}||V_{λ} · e⟩ [σ] → c [x←V_{λ}; α←e; σ′]
(→^{ℕ} μ) ⟨x′_{i}||n · e⟩ [σ] → c_{n} [α←e; σ′]
(μ̃_{v})  ⟨V_{λ}||α_{i}⟩  [σ] → c [x←V_{λ}; σ′]
(ℕ)  ⟨n||α′_{i}⟩  [σ] → c_{n} [σ′]

\begin{matrix}σ(x_{i}) = (λx.μα.c)[σ′] & σ(α_{i}) = (μ̃x.c)[σ′] \\ σ(x′_{i}) = (λλn.μα.c_{n})[σ′] & σ(α′_{i}) = ([n↦c_{n}])[σ′] \end{matrix} 26

Abstract Computing Devices

(collecting the ingredients)

Hardin-Maranget-Pagano [1996] relevance of explicit substitution to represent environments in abstract devices Abstract machines characterised by reducing at the root of the computation The μμ̃-system:

• has a primitive notion of evaluation contexts (“stacks”)

• has a primitive notion of “states” (the commands)

• redex of non head normal states are at the root

Add an (ad hoc) variable numbering schemes All ingredients are here to simulate abstract machines

Duality and dependent types

(when left-right symmetry meets left-right dependency)

call-by-name  call-by-value

implicit dependent product (intersection)

OK

OK (but restricted to lin. ev. ctx.)

implicit dependent sum (union)

OK (but restricted to values - cf Pierce [1991])

OK

explicit dependent sum (stand-alone domain)

OK OK

explicit dependent sum (stand-alone domain)

OK OK

explicit dependent product (type-theoretic)

OK (but bypass μ̃)

OK (but applied to value only)

explicit dependent sum (type-theoretic) classical case degenerated (Herbelin [2005])

Conclusions and problems

The μμ̃-subsystem is an elegant tool to investigate the duality properties of the computation, and to revisit the foundations of λ-calculus.

The \overline{λ}μ̃_{v}-calculus, good candidate for studying classical call-by-value computation.

Can we give a symmetric (non substitution-based) semantics Add command {c, c} and take rules (∪) ⟨μα.c||μ̃x.c′⟩ → {c[α ← μ̃x.c′], c′[x ← μα.c]} (μ_{n})  ⟨μα.c||E⟩ → c[α ← E] (μ̃_{v})  ⟨V ||μ̃x.c⟩ → c[x ← V] Which valid equations about {c, c′} (associativity, commutativity, distributivity)? for system μμ̃ (see e.g. Došen-Petrić categories

of distributive lattices – see also Führmann-Pym and Lamarche-Straßburger “boolean” categories)?

How to interpret Gentzen’s cross-cuts^{\begin{matrix}Γ ⊢ A, \overline{A}, Δ Γ, \overline{A}, \overline{A} ⊢ Δ \\ Γ ⊢ A, Δ \end{matrix} \begin{matrix}Γ ⊢ \underline{A}, \underline{A}, Δ Γ, \underline{A}, A ⊢ Δ \\ Γ, A ⊢ Δ \end{matrix} Γ ⊢ Δ ↑ (Cross-cuts) \begin{matrix}Γ ⊢ A, A, Δ Γ, A, A ⊢ Δ \\ Γ ⊢ Δ \end{matrix} (CBN) ↙ ↘ (CBV) Γ ⊢ A, \overline{A}, Δ \begin{matrix}Γ ⊢ \underline{A}, \underline{A}, Δ Γ, \underline{A}, A ⊢ Δ \\ Γ, \overline{A} ⊢ Δ \end{matrix} Γ ⊢ A, Δ \begin{matrix}Γ ⊢ \underline{A}, \underline{A}, Δ Γ, \underline{A}, A ⊢ Δ \\ Γ, A ⊢ Δ \end{matrix} Γ ⊢ Δ \begin{matrix}Γ ⊢ A, \overline{A}, Δ Γ, \overline{A}, \overline{A} ⊢ Δ \\ Γ ⊢ A, Δ \end{matrix} \begin{matrix}Γ ⊢ A, \overline{A}, Δ Γ, \overline{A}, \overline{A} ⊢ Δ \\ Γ ⊢ \underline{A}, Δ \end{matrix} Γ, \underline{A}, A ⊢ Δ Γ, A ⊢ Δ Γ ⊢ Δ} ? (see also Coquand-Herbelin symmetric product, Raghunandan-Summers’s symmetric cut-elimination of a primitive “iff” connective)?

The duality finds limits in dependent type theory.

French manuscript available at http://pauillac.inria.fr/˜ herbelin/habilitation/memoire.ps

30

Extra material

31

Coinductive and inductive types

(Paulin-Mohring’s fixpoint-based decomposition)

Coinductive type  Inductive type
= term constructors  = term constructors
+ ev. ctx. constructors  + ev. ctx. constructors
+ term recursion guarded by a term constructor + ev. ctx. recursion guarded by an ev. ctx. constructor

E x a m p l e s

A coinductive type (possibly infinite lists)  An inductive type (lists)
V ::= … || nil || cons(v, v) || ν_{x}.V_{c}
E ::= … || [nil.c, cons(x_{a}, x_{l}).c]

V ::= … || nil || cons(v, v)
E ::= … || [nil.c, cons(x_{a}, x_{l}).c] || ν̃_{α}.E_{c}
(nil) ⟨nil||[nil.c, cons(x_{a}, x_{l}).c′]⟩  → c
(cons) ⟨cons(v_{a}, v_{l})||[nil.c, cons(x_{a}, x_{l}).c′]⟩ → ⟨v_{a}||μ̃x_{a}.⟨v_{l}||μ̃x_{l}.c′⟩⟩
(ν) ⟨ν_{x}.V_{c}||E_{c}⟩ → ⟨V_{c}[x ← ν_{x}.V_{c}]||E_{c}⟩  (ν̃) ⟨V_{c}||ν̃_{α}.E_{c}⟩ → ⟨V_{c}||E_{c}[α ← ν̃_{α}.E_{c}]⟩

V_{c} means constructed V E_{c} means constructed E