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