Library SimplyTypedLambdaMu

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).

Some "Logical Intuitions" about this language:



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)

This file is distributed under the terms of the "GNU LESSER GENERAL PUBLIC LICENSE" version 3. See http://www.gnu.org/licenses.


This page has been generated by coqdoc