``` ```

# Mixed Embedding of Simply Typed Lambda-Mu Calculus.

This file is an introduction to the simply typed version of Parigot's calculus. It implements Curry-Howard paradigm in classical propositional logic.

I prove here that the logic is consistent. I also give a weak result on the completeness of the proof system. I emulate in Coq an interpreter of this lambda-calculus (I give small examples of reduction).

Technically, I use a higher-order abstract syntax technique to avoid the tedious handling of binders.

``` Set Implicit Arguments. ```
Preliminary: negation on Type
``` Definition neg (A: Type) := A -> False. ```

# Syntax of types (e.g. of classical propositions).

We consider here Coq propositions as atomic formulas.
``` Inductive type: Type :=   | ATOM: Prop -> type   | ARROW: type -> type -> type. Infix "==>" := ARROW (at level 80, right associativity). ```

# Derived types

``` Definition FALSE: type := ATOM False. Definition TRUE: type := ATOM True. Definition NOT (T: type): type   := T ==> FALSE. Definition OR (A B: type): type   := (NOT A) ==> B. Definition AND (A B: type): type   := NOT (A ==> (NOT B)). ```

# Syntax of Terms (e.g. of proofs)

``` Section TERMS. ```
I give the abstract syntax of terms before to explain there informal meaning (see "logical intuitions" below). The calculus is a usual lambda-calculus extend with a continuation-handling mechanism.
• In order to avoid the encoding of variable substitution, a bound variable is represented directly as a Coq function (see `LAMBDA` and `MU` binders).
• Terms are parameterized by the (meta)type of variables.
• Here, we represent only "well-typed" terms (typing of lambda-mu calculus is emulated by Coq typing).
• The meta-type of variables is itself parameterized by a type (the type of term abstracted by the given variable).
• In this language, there are two syntactic categories of variable:
• `vV` (variable for "values") introduced by `LAMBDA`.
• `vC` (variable for "continuations") introduced by `MU`.
``` Variable vV: type -> Type. Variable vC: type -> Type. Inductive term: type -> Type :=   (** usual constants: we embed here double negation of Coq proofs *)   | CTE (P:Prop): neg (neg P) -> (term (ATOM P))   (** usual variables *)   | VAR (A:type): (vV A) -> (term A)   (** usual lambda- y"">abstraction *)   | LAMBDA (A B:type): ((vV A) -> (term B)) -> (term (A ==> B))   (** usual application *)   | APP (A B:type): (term (A ==> B)) -> (term A) -> (term B)   (** application of a term to a continuation (branch to this continuation) *)   | BRA (A:type): (vC A) -> (term A) -> (term FALSE)   (** abstraction of a continuation *)   | MU (A:type): ((vC A) -> (term FALSE)) -> (term A). ```

There are two binders in the language:
• `LAMBDA` is the usual binder (introduction of a "usual" hypothesis in the logic).
• `MU` is the binder used in double-negation elimination: it introduces an hypothesis that we want to show inconsistent in the proof.

For instance, in the translation of the informal reasoning << Assuming "`x`" a proof of "`(not A)`", ... thus, "`FALSE`" is provable. Hence, "`A`". >> variable "`x`" is formally introduced my "`MU`" binder and it has type "`(vC A)`".

Basically, the "`FALSE`" introduction rule is the following. if "`x:(vC A)`" and "`p`" of proof "`A`" then "`BRA x p`" is a proof of "`FALSE`".

From a cut-elimination point of view, we have the following rule (if "`x`" is not free in "`p`"): "`MU (fun x => BRA x p)`" reduces to "`p`"

Hence, computationally
• `x` is a branch label.
• `BRA` is a jump to a label.
• `MU` declares a branch label.

Actually, this is not so simple, because extending naively this rule may break confluence. Here, the calculus is still deterministic (see `eval` function on closed terms below) but it is no simple to figure out the computational behavior of terms (see `mu_handle`* lemmas below).

``` ```
The lift derived term: lift a continuation variable into a lambda-abstraction
``` Definition LIFT (A: type) (x:(vC A)): (term (A ==> FALSE))   := LAMBDA (fun p:(vV A) => BRA x (VAR p)). End TERMS. Implicit Arguments CTE [vV vC P]. Implicit Arguments VAR [vV vC A]. Implicit Arguments LAMBDA [vV vC A B]. Implicit Arguments APP [vV vC A B]. Implicit Arguments BRA [vV vC A]. Implicit Arguments MU [vV vC A]. Implicit Arguments LIFT [vV vC A]. ```

# Closed terms: `expr` is the type of "closed" (well-typed) terms.

``` Definition expr (t:type) : Type := forall (vV vC: type -> Type), (term vV vC t). ```
With the following coercion, we embed "type" as a sort of Coq...
``` Coercion expr: type >-> Sortclass. ```

# Proof of the usual rules of classical propositional logic

``` ```
`TRUE` introduction
``` Definition NIL: TRUE := fun vV vC => CTE (fun h => (h I)). ```
`FALSE` elimination
``` Definition CASE_FALSE (A:type): FALSE ==> A   := fun vV vC =>      (LAMBDA        (fun p:(vV FALSE) => MU (fun x:(vC A) => (VAR p)))). Implicit Arguments CASE_FALSE [A]. ```
double-negation elimination
``` Definition TX (A:type): (NOT (NOT A)) ==> A   := fun vV vC =>       (LAMBDA         (fun p:(vV (NOT (NOT A))) =>           (MU (fun x:(vC A) => APP (VAR p) (LIFT x))))). Implicit Arguments TX [A]. ```
`OR` left-introduction
``` Definition LEFT (A B: type): A ==> (OR A B)   := fun vV vC =>       (LAMBDA (fun a:(vV A) =>         (LAMBDA (fun na:(vV (NOT A)) =>            (MU (fun d:(vC B) => APP (VAR na) (VAR a))))))). Implicit Arguments LEFT [A B]. ```
`OR` right-introduction
``` Definition RIGHT (A B: type): B ==> (OR A B)   := fun vV vC =>       (LAMBDA (fun b:(vV B) =>         (LAMBDA (fun y"">d:(vV (NOT A)) => VAR b)))). Implicit Arguments RIGHT [A B]. ```
`OR` elimination
``` Definition CASE_OR (A B C:type): (A ==> C) ==> (B ==> C) ==> (OR A B) ==> C   := fun vV vC =>      (LAMBDA (fun ha: (vV (A ==> C)) =>      (LAMBDA (fun hb: (vV (B ==> C)) =>      (LAMBDA (fun h: (vV (OR A B)) =>       (MU (fun nc:(vC C) =>         (BRA nc           (APP (VAR ha)             (MU (fun na:(vC A) =>                  (BRA nc                    (APP (VAR hb)                      (APP (VAR h)                           (LAMBDA (fun a:(vV A) => (BRA na (VAR a))))))))))))))))))). Implicit Arguments CASE_OR [A B C]. ```
Exculed-Middle
``` Definition EM (A:type): (OR (NOT A) A)  := TX (A:=A). ```
`AND` introduction
``` Definition PAIR (A B: type): A ==> B ==> (AND A B)  := fun vV vC =>      (LAMBDA (fun a: (vV A) =>      (LAMBDA (fun b: (vV B) =>      (LAMBDA (fun h: (vV (A ==> (NOT B))) =>        (APP (APP (VAR h) (VAR a)) (VAR b)))))))). ```
`AND` left-elimination
``` Definition PROJ1 (A B: type): (AND A B) ==> A  := fun vV vC =>      (LAMBDA (fun h: (vV (NOT (A ==> (NOT B)))) =>         (MU (fun na: (vC A) =>                (APP (VAR h)                   (LAMBDA (fun a:(vV A) =>                   (LAMBDA (fun b:(vV B) =>                      (BRA na (VAR a))))))))))). ```
`AND` right-elimination
``` Definition PROJ2 (A B: type): (AND A B) ==> B  := fun vV vC =>      (LAMBDA (fun h: (vV (NOT (A ==> (NOT B)))) =>         (MU (fun nb: (vC B) =>                (APP (VAR h)                   (LAMBDA (fun a:(vV A) =>                   (LAMBDA (fun b:(vV B) =>                      (BRA nb (VAR b))))))))))). ```

# Semantics

``` Inductive mult (A B:Type) : Type :=   | pair: A -> B -> (mult A B). ```
The `dual` of type represents the semantics of a "classical" negation whereas `neg` is the usual "intuitionistic" negation (see above). The classical negation of `ARROW` is a product (e.g. a "and")
``` Fixpoint dual (T: type): Type :=   match T with   | (ATOM P) => neg P   | (ARROW A B) => (mult (neg (dual A)) (dual B))   end. ```
Hence, roughly, types are interpreted by their double negation.
``` Definition value (A:type) : Type := neg (dual A). ```
Semantics of terms (a continuation semantics)
``` Fixpoint eval (T:type) (t: term value dual T) {struct t}: (value T) :=   match t in (term _ _ T) return (value T) with   | (CTE P p) =>       fun k: (neg P) => p k   | (VAR A x) =>       fun k:(dual A) => x k   | (LAMBDA A B f) =>       fun (x: mult (value A) (dual B)) =>         match x with         | (pair k1 k2) => eval (f k1) k2         end   | (APP A B t1 t2) =>       fun kb:(dual B) => (eval t1) (pair (fun ka => eval t2 ka) kb)   | (BRA A x t0) =>       fun k => (eval t0) x   | (MU A f) =>       fun k:(dual A) => eval (f k) (fun x:False => x)    end. ```
Semantics of "closed" terms
``` Definition sem (T:type) (e: T) := eval (e value dual). ```
The logic is sound: `FALSE` can not be proved.
``` Theorem lambda_mu_consistency: FALSE -> False. Proof.   intros e; generalize (sem e).   unfold value, neg.   simpl.   unfold neg; simpl.   tauto. Qed. ```
The proof system is complete: any inhabited type in the semantics has a corresponding term. Here we have only a weak form because, we do not prove the existence of a "closed" term.
``` Theorem proof_complete_weak:  forall (T:type), (value T) -> (term value dual T). Proof.   unfold value, neg; simpl.   induction T; simpl; unfold neg, expr. ```
ATOM case
```   intros; apply CTE; tauto. ```
LAMBDA case
```   intros; apply LAMBDA.   intros x.   apply IHT2.   intros H1; apply H.   apply pair; auto. Qed. ```

# Computational behavior of `eval` on some examples

``` Notation "{[ e ]}" := (e _ _). ```
Basic beta-reduction
``` Lemma beta: forall (A B:type) (f: A ==> B) (a:A) (k: dual B),   (sem (fun vV vC => APP (LAMBDA (fun x:(vV A) => APP {[ f ]} (VAR x)))                           {[ a ]})        k)   = (sem (fun vV vC => APP {[ f ]} {[ a ]}) k). Proof.   intros; apply refl_equal. Qed. ```
Basic `MU`/`BRA` reduction
``` Lemma mu_handle1: forall (A:type) (a: A) (k: dual A),   (sem (fun vV vC => MU (fun x:(vC A) => BRA x {[a]})) k)   = (sem a k). Proof.   intros; apply refl_equal. Qed. ```
Branch out of a `MU`
``` Lemma mu_handle2: forall (A:type) (a: A) (k : dual A),   (sem (fun vV vC => MU (fun exit:(vC A) =>                            MU (fun y:(vC FALSE) => BRA exit {[a]}))) k)   = (sem a k). Proof.   intros; apply refl_equal. Qed. ```
Here, beta-reduction wins against branch out
``` Lemma mu_handle3: forall (A:type) (a b: A) (k: dual A),   (sem (fun vV vC => MU (fun exit: (vC A) =>                       APP (LAMBDA (fun x:(vV FALSE) => (BRA exit {[ a ]} )))                          (BRA exit {[ b ]})))         k)   = (sem a k). Proof.   intros; apply refl_equal. Qed. ```
Here again !
``` Lemma mu_handle4: forall (A:type) (a b: A) (k: dual A),   (sem (fun vV vC => MU (fun exit: (vC A) =>                       APP                         (APP (LAMBDA (fun x:(vV FALSE) =>                                LAMBDA (fun y:(vV FALSE) => (VAR y))))                              (BRA exit {[ a ]} ))                         (BRA exit {[ b ]})))         k)   = (sem b k). Proof.   intros; apply refl_equal. Qed. Unset Implicit Arguments. ```
Copyright 2007 Sylvain Boulmé (web page)

``` ```