C’est maintenant qu’on calcule

It’s time to compute

Au cœur de la dualité

Deep in the duality

Préambule

Je remercie avant tout Jean-Pierre Jouannaud. Sans sa gentille insistance, nous ne serions peut-être pas réuni ensemble ici présent.

J’ai profité de l’occasion de l’habilitation pour approfondir ce qui est sans doute ma contribution scientifique principale, à savoir mon travail avec Pierre-Louis Curien sur la dualité du calcul.

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

The syntactic duality of computation

(The μμ̃-subsystem and its extensions)

The μμ̃-subsystem: the heart 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 extension 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 \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 \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]

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

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
μ-binder  / μ̃-binder

Semantical duality

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

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 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 · α⟩

\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

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 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]

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

?

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

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} 27

Control delimiters

Felleisen [1988], Danvy-Filinski [1989] control delimiters Sitaram-Felleisen [1990] PCF with control and delimiters is complete wrt domains (up to parallel-if) Filinski [1994] control and delimiters have the expressiveness of monads Ariola-Herbelin-Sabry [2004] λμ-calculus + control delimiters delimiter = dynamic binding of the “toplevel continuation”

Would the addition of delimiters and (intuitionistic restrictions of) control be the right way to provide direct-style monadic extensions in intuitionistic type theory?

David-Py [2001] call-by-name λμ-calculus with η is not complete (separation contexts missing) Saurin [2005] call-by-name λμ-calculus extended with operators “similar” to delimiters is complete

Are delimiters the ingredients for a Böhm theorem for call-by-name and call-by-value λ-calculus with control?

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

The μμ̃-subsystem

(non-deterministic union)

\begin{aligned}c & ::= & ⟨v||e⟩ || \{c, c\} \\ V & ::= & x || … \\ v & ::= & μα.c || V \\ E & ::= & α || … \\ e & ::= & μ̃x.c || E \end{aligned}

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

Open questions

- Which valid equations about {c, c′} (associativity, commutativity, distributivity)?

- Relation with Kosta Došen and Zoran Petrić’s categories of distributive lattices?

Beyond substitution-based computation: cross-cuts

Cross-cuts have been introduced by Gentzen [1938]. They provide some form of computational optimisation. They are not reducible to substitution. Can they smoothly be taken into account in the system μμ̃?

(see also Coquand-Herbelin’s unpublished analysis of symmetric !/! critical pair [1994])

Duality and dependent types

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

call-by-name  call-by-value

explicit dependent product (type-theoretic)

OK (but bypass μ̃)

OK (but applied to value only)

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

Summary

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

The duality finds limits in dependent type theory.

Et maintenant...

(and now...)

Arrêté du 23 novembre 1988 relatif à l’habilitation à diriger des recherches (article 7, extraits) « La présentation des travaux est publique. »

“The presentation of works is public.”

« Le candidat fait devant le jury un exposé sur l’ensemble de ses travaux (...). Cet exposé donne lieu à une discussion avec le jury. »

“The candidate gives a talk on his whole works (...). The talk is followed by a discussion with the the committee.”

« Le jury procède à un examen de la valeur de candidat, évalue sa capacité à concevoir, diriger, animer et coordonner des activités de recherche et de valorisation et statue sur la délivrance de l’habilitation. »

“The committee conducts an examination of the value of the candidate, evaluates its ability to conceive, head, animate and arrange research and valorisation activities and gives a decision on the delivery of the habilitation”

What about Coq?

(Mister Hyde)

Strong involvement in the Coq development projects (1999-2004)

- Coq version 7 (enforcement of de Bruijn principle, re-appropriation of Coq code)

- Coq version 8 (uniform and scalable revision of the concrete syntax) A few visible features (induction tactics, let-in construct, nested pattern-matching, mathematical notations)

and more discrete ones (general maintenance, bug fixes). Many projects for improvements now stem from outside the LogiCal team. How to make the Logical contribution to the Coq project evolves?