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