Minimal Classical Logic and Control Operators

Zena M. Ariola  Hugo Herbelin
University of Oregon  INRIA-Futurs
USA  France

ICALP - 3 July 2003

Outline

• Introduction – Minimal, Intuitionistic and Classical Logic – λ-calculus control operators

• Minimal Classical Logic

• Computational interpretation of ⊥ → A • A new variant of Felleisen λC calculus Minimal Logic and λ-calculus

A ::= X | A → A t, u ::= x | λx.t | tu

Γ, \begin{matrix}Ax \\ x : A \end{matrix} ⊢ \begin{matrix}Ax \\ x : A \end{matrix}

\begin{matrix}Γ, \begin{matrix}Ax \\ x : A \end{matrix} ⊢ \begin{matrix}Bt \\ t : B \end{matrix} \\ Γ ⊢ \begin{matrix}A → Bλx.t \\ λx.t : A → B \end{matrix} \end{matrix}  \begin{matrix}Γ ⊢ \begin{matrix}A → Bt \\ t : A → B \end{matrix} Γ ⊢ \begin{matrix}Au \\ u : A \end{matrix} \\ Γ ⊢ \begin{matrix}Btu \\ tu : B \end{matrix} \end{matrix}

Control Operators

• K (callcc): λx.K(λk.1 + (if x = 0 then k2 else 3)) + 8 Name k is bound to the continuation which adds 8:

           acc := 1 + if x=0 then {acc:=2;goto k} else 3
 label k  : acc := acc+8
           return acc

returns 2 + 8 if x = 0 and (1 + 3) + 8 otherwise

• C: λx.C(λk.1 + (if x = 0 then k2 else 3)) + 8 Additional “Abort” to “toplevel” in case of non exceptional result

           acc := 1 + if x=0 then {acc:=2;goto k} else 3
           goto top
 label k  : acc := acc+8
 label top: return acc

returns 2 + 8 if x = 0 and 1 + 3 otherwise Intuitionistic - Classical Logic and Control Operators (Griffin ’90)

• Intuitionistic: Minimal Logic + Ex Falso Quodlibet (⊥ → A)

\begin{matrix}Γ ⊢ \begin{matrix}⊥t \\ t : ⊥ \end{matrix} \\ Γ ⊢ \begin{matrix}AAbort(t) \\ Abort(t) : A \end{matrix} \end{matrix}

• Classical: Intuitionistic + Double Negation (¬¬A → A)

\begin{matrix}Γ ⊢ \begin{matrix}¬¬At \\ t : ¬¬A \end{matrix} \\ Γ ⊢ \begin{matrix}AC(t) \\ C(t) : A \end{matrix} \end{matrix}

Logic and Computation

• Equivalent formulations of Classical Logic in Intuitionistic Logic

Excluded Middle A ∨ ¬A
Pierce law  ((A → B) → A) → A
Double negation ¬¬A → A

• Felleisen: C is more expressive than K (C can’t be defined from K)

\begin{matrix}K(λk.M) = C(λk.kM) \\ C(λk.M) = K(λk.Abort(M)) \end{matrix}

Are those axioms really equivalent? ⟹ We study them in the context of Minimal Logic

¬¬A → A

⇓ ⇑̸ ((A → B) → A) → A

⇓ ⇑̸ A ∨ ¬A

⟹ Minimal Classical Logic

Minimal Classical Logic

• Minimal Classical Logic: Minimal Logic + Pierce law λ-calculus + K (callcc)

• Classical Logic:

Minimal Logic + \overbrace{Peirce law + (⊥ → A)}^{= ¬¬A→A} λ-calculus + \underbrace{K + Abort}

= C

Minimal Classical Logic

Minimal Intuitionistic Classical Minimal Classical Peirce law EFQ

K (call-cc)

Abort?

Minimal Classical Natural Deduction and Parigot λμ-calculus Sequents: \{ \begin{matrix}Γ ⊢ A“stoup” ; Δ set of conclusions & t, u ::= x | λx.t | tu | μα.c & (terms) \\ Γ ⊢ A empty “stoup” ; Δ set of conclusions & c ::= [α]t & (commands) \end{matrix}

Γ, x : A ⊢_{MC} x : A; Δ

Γ, x : A ⊢_{MC} t : B; Δ Γ ⊢_{MC} λx.t : A → B; Δ Γ ⊢_{MC} t : A → B, Δ Γ ⊢_{MC} u : A, Δ

Γ ⊢_{MC} tu : B, Δ
c : (Γ ⊢_{MC}; Aα, Δ)
Γ ⊢_{MC} μα.c : A; Δ

Activate

Γ ⊢_{MC} t : A; Aα, Δ
[α]t : (Γ ⊢_{MC}; A, Δ)

Passivate

Properties of Minimal Classical Natural Deduction

Prop: Γ ⊢_{MC} A iff Γ, P L ⊢ A Prop: there is no t of type ¬¬A → A

But we can derive ⊢_{MC} λy.μα.[γ](y λx.μδ.[α]x) : ¬¬A → A; ⊥γ where a free continuation variable γ of type ⊥ is needed. Possible solution (Parigot, de Groote, Ong) : hide the variables of type ⊥ in the typing system. Our interpretation: this free variable denotes abortion to the “toplevel”.

Minimal Classical Natural Deduction and Parigot λμ-calculus λμ-top-calculus

Γ, x : A ⊢_{MC} x : A; Δ

Γ, x : A ⊢_{MC} t : B; Δ Γ ⊢_{MC} λx.t : A → B; Δ Γ ⊢_{MC} t : A → B, Δ Γ ⊢_{MC} u : A, Δ

Γ ⊢_{MC} tu : B, Δ
c : (Γ ⊢_{MC}; Aα, Δ)
Γ ⊢_{MC} μα.c : A; Δ

Activate

Γ ⊢_{MC} t : A; Aα, Δ
[α]t : (Γ ⊢_{MC}; A, Δ)

Passivate

Γ ⊢_{MC} t : ⊥; Δ
[top]t : (Γ ⊢_{MC}; Δ)

Abort, ⊥, and the toplevel

Our analysis puts in the light the existence of an implicit continuation variable of type ⊥

• its logical interpretation is the false formula

• its computational interpretation is the type of the toplevel

It allows to precisely decompose Felleisen’s Abort operator as a “throw” to the toplevel:

Abort = λx.μd.[top]x : ⊥ → A for d fresh

It pushes also to identify the logical formula ⊥ with the toplevel type of a program (as done by Griffin). This conforms with the standard A-translation trick where ⊥ is precisely replaced by the top statement of a proof.

Minimal Classical Logic

Minimal Intuitionistic Classical Minimal Classical Peirce law EFQ

K (call-cc)
In fact: just P assivate

Abort? No: top

From λμ-calculus to a variant of λC-calculus

Parigot λμ-calculus:

• ⊥ not needed to express minimal classical logic

• ⊥ interpreted as an abstract type (which may be empty like in the standard logical interpretation, or inhabited as is the toplevel type in the standard computational interpretation).

One-conclusion classical logic needs another kind of ⊥ to mimic the role of multiple conclusions. Let’s call it ⊥^{c}. This leads to a refinement of classical logic obtained by constraining the axiom scheme ¬¬A → A to be of the form ¬_{c}¬_{c}A → A.

The formal formula ⊥^{c} is naturally interpreted as an empty type.

Prawitz Natural Deduction revisited (an introduction to λ-C−-top calculus)

Γ, x : A ⊢_{RAA} x : A

Γ, x : A ⊢_{RAA} t : B Γ ⊢_{RAA} λx.t : A → B

Γ ⊢_{RAA} t : A → B Γ ⊢_{RAA} u : A
Γ ⊢_{RAA} tu : B

Γ, k : ¬cA ⊢_{RAA} c : ⊥c Γ ⊢_{RAA} C−(λk.c) : A

RAA_{c} Γ ⊢_{RAA} t : ⊥c

Γ ⊢_{RAA} C−(λd.c) : A

RAA′_{c}
Γ ⊢_{RAA} t : ⊥
Γ ⊢_{RAA} top t : ⊥c

The λ-C−-top calculus

t, u ::= x | λx.t | tu | C−(λk.c) c ::= kt | top t

Felleisen’s operators in λ-C−-top calculus K = λx.C−(λk.k(xk)) C = λx.C−(λk.top (xk)) Abort = λx.C−(λk.top x)

Call-by-value reduction in λ-C− and λ-C−-top calculi (v ::= x | λx.t)

\begin{aligned}β : & (λx.t)v & → & t[x := v] \\ C{− \atop elim} : & C−(λk.kt) & → & t k ∉ F V (t) \\ C− L : & C−(λk.t)u & → & C−(λk.t[k (wu)/k w]) \\ C− R : & vC−(λk.t) & → & C−(λk.t[k (vw)/k w]) \\ C{− \atop idem} : & C−(λk.k′C−(λq.u)) & → & C−(λk.u[k′/q]) \end{aligned}

Prop: The reduction rules are typable and enjoy subject reduction. They are confluent. Similarly for call-by-name.

The end (made by advi)