-- Normalization for Intuitionistic Propositional Logic -- using hereditary substitutions. -- Andreas Abel, 21 May 2018 module NormalizationIPL where -- We assume a set of propositional variables aka atomic propositions. postulate Base : Set -- Propositional formulas data Form : Set where Atom : (P : Base) → Form -- Atomic proposition True : Form -- Truth False : Form -- Absurdity _∧_ : (A B : Form) → Form -- Conjunction -- \ wedge _∨_ : (A B : Form) → Form -- Disjunction -- \ vee _⇒_ : (A B : Form) → Form -- Implication -- \ r 2 -- Binding strength of connective in decreasing order infixl 8 _∧_ infixl 7 _∨_ infixr 6 _⇒_ -- The propositional calculus defines how we can derive the truth -- of a proposition C from a list of hypotheses Γ. -- C is called the conclusion and Γ is also called the context -- or the list of assumptions. -- -- The propositional calculus allows us to make judgments -- -- Γ ⊢ C -- -- meaning "if all the assumptions in Γ are true, then C must be true as well". -- To define this judgement and formal derivations of it, we first -- formalize hypotheses. -- Hypotheses are snoc-lists of formulas: most recent assumption is last. -- We can also consider hypotheses as stacks of formulas. data Cxt : Set where ε : Cxt -- Empty list -- \ G e ALT: \ epsilon _∙_ : (Γ : Cxt) (A : Form) → Cxt -- Extension -- \ . and \ G G for Γ infixl 4 _∙_ -- The indexed type Hyp Γ A gives evidence that formula A is element -- of the list of hypotheses Γ data Hyp : (Γ : Cxt) (A : Form) → Set where top : ∀{Γ A} → Hyp (Γ ∙ A) A -- Found A as the top element. pop : ∀{Γ A B} (x : Hyp Γ A) → Hyp (Γ ∙ B) A -- Remove the top element, search on. -- Derivations for the judgement Γ ⊢ C -- These are the proof rules of intuitionistic propositional logic. -- In type theory, we can define Γ ⊢ C as a set whose inhabitants -- are the derivations of Γ ⊢ C. -- Each element of the following list of constructors of Γ ⊢ C -- represents one proof rule for IPL. Each rule has a number of premises -- (in our case, between 0 and 3), and a consequence. -- For instance, the rule -- -- Γ ⊢ A Γ ⊢ B -- -------------- andI -- Γ ⊢ A ∧ B -- -- has two premises, that A is derivable from Γ and B as well, and allows us -- to conclude that A ∧ B is derivable as well. -- We distinguish introduction rules, postfixed I, from elimination rules, postfixed E. -- Introduction rules introduce a logical connective in the consequence, while -- elimination rules eliminate a logical connective in one of the premises. -- -- Above rule "andI" is an instance of an introduction rule, it constructs -- evidence for a conjunction from evidence for each of the conjuncts. -- An example for an elimination rule is: -- -- Γ ⊢ A ∧ B -- --------- andE₁ -- Γ ⊢ A -- -- It allows us to conclude the derivability of the first conjunct, A, from -- the derivability of the conjunction A ∧ B. -- -- If an elimination rule has several premises, we call the one with -- the eliminated connective the principal premise or main premise, -- and its formula the principal or main formula, and the connective -- the principal connective. -- -- For example: -- -- Γ ⊢ A ⇒ B Γ ⊢ A -- ------------------- impE -- Γ ⊢ B -- -- This rule, traditionally called "modus ponens", has principle connective ⇒, -- principle formula A ⇒ B, and principal premise Γ ⊢ A ⇒ B. -- The other premise, here, Γ ⊢ A, is called "side premise". -- -- Some rules add a hypothesis to the context of a premise, for example, -- the implication introduction rule: -- -- Γ ∙ A ⊢ B -- ---------- impI -- Γ ⊢ A ⇒ B -- -- This rule states that an implication A ⇒ B is derivable from hypotheses Γ, -- if its conclusion B is derivable from the extended context Γ ∙ A. -- -- Let's look at the Agda representation, and get explanations of -- the remaining rules then. infix 2 _⊢_ -- \ vdash data _⊢_ (Γ : Cxt) : (A : Form) → Set where hyp : ∀{A} (x : Hyp Γ A) → Γ ⊢ A trueI : Γ ⊢ True andI : ∀{A B} (t : Γ ⊢ A) (u : Γ ⊢ B) → Γ ⊢ A ∧ B andE₁ : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ A andE₂ : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ B impI : ∀{A B} (t : Γ ∙ A ⊢ B) → Γ ⊢ A ⇒ B impE : ∀{A B} (t : Γ ⊢ A ⇒ B) (u : Γ ⊢ A) → Γ ⊢ B orI₁ : ∀{A B} (t : Γ ⊢ A) → Γ ⊢ A ∨ B orI₂ : ∀{A B} (t : Γ ⊢ B) → Γ ⊢ A ∨ B orE : ∀{A B C} (t : Γ ⊢ A ∨ B) (u : Γ ∙ A ⊢ C) (v : Γ ∙ B ⊢ C) → Γ ⊢ C falseE : ∀{C} (t : Γ ⊢ False) → Γ ⊢ C -- Explanation: -- -- hyp: Γ ⊢ A is derivable since A ∈ Γ. -- trueI: Truth is trivially derivable (empty conjunction). -- orI: If one of the disjuncts is derivable, so is the disjunction. -- orE: If a disjunction A ∨ B is derivable, we can use it to derive -- an arbitrary formula C if we can derive C both from A and from B. -- falseE: The empty disjunction. Once we have derived False, everything -- is true (ex falsum quod libet). -- In the remainder of this file, we define normal forms -- and prove the normalization theorem. -- The following Flag indicates whether we deal with a -- -- lin) straight-line elimination using only impE and andE -- branch) an elimination that ends in a orE or falseE data Flag : Set where lin : Flag -- Just impE and andE branch : Flag -- lin followed by a single orE or falseE -- The following grammar defines normal derivations (Nf), -- which are constructed from introductions and then -- possibly an elimination from a hypothesis. mutual -- Normal derivations (Nf = normal form). -- We can recursively apply introduction rules -- and then switch to elimination from a hypothesis. data Nf (Γ : Cxt) : (A : Form) → Set where trueI : Nf Γ True impI : ∀{A B} (t : Nf (Γ ∙ A) B) → Nf Γ (A ⇒ B) andI : ∀{A B} (t : Nf Γ A) (u : Nf Γ B) → Nf Γ (A ∧ B) orI₁ : ∀{A B} (t : Nf Γ A) → Nf Γ (A ∨ B) orI₂ : ∀{A B} (t : Nf Γ B) → Nf Γ (A ∨ B) hyp : ∀{A C f} (x : Hyp Γ A) (es : Elims Γ A C f) → Nf Γ C -- Elims Γ A C f eliminates proposition A into C, using -- possibly several impE and andE steps first, and then -- possibly a final falseE or orE step. -- All side derivations are in Nf. data Elims (Γ : Cxt) : (A C : Form) (f : Flag) → Set where [] : ∀{A} → Elims Γ A A lin _∷_ : ∀{A B C f} (e : Elim Γ A B) (es : Elims Γ B C f) → Elims Γ A C f falseE : ∀{C} → Elims Γ False C branch orE : ∀{A B C} (t₁ : Nf (Γ ∙ A) C) (t₂ : Nf (Γ ∙ B) C) → Elims Γ (A ∨ B) C branch -- Elim Γ A C contains single a single impE or andE elimination. data Elim (Γ : Cxt) : (A C : Form) → Set where impE : ∀{A B} (t : Nf Γ A) → Elim Γ (A ⇒ B) B andE₁ : ∀{A B} → Elim Γ (A ∧ B) A andE₂ : ∀{A B} → Elim Γ (A ∧ B) B -- Normal derivations are trivially consistent: -- There is no normal proof of False in the empty context. nf-consistent : Nf ε False → ∀{A : Set} → A nf-consistent (hyp () _) -- The challenge is to show that Nf is still a complete proof system for IPL. -- That means that whenever t : Γ ⊢ C, there exists also a normal derivation v : Nf Γ C. -- This theorem is also called normalization, because it takes a proof t -- and returns its normal form. -- In the remainder of this file, we prove the normalization theorem. -- Proving the normalization theorem amounts to supply the "missing rules" for Nf. -- For instance, there is a rule impI on normal derivations, but no rule -- -- impE : (t : Nf Γ (A ⇒ B)) (u : Nf Γ A) → Nf Γ B -- -- We will show that this rule is admissible. It can be shown by -- lexicographic induction on (A, t). However, the inductive argument -- is not trivial, it requires us to define a normalizing substitution. -- First, we show the admissibility of conjucntion and absurdity elimination -- which are straightforward. -- Conjunction elimination (andE₁!). -- For admissibility of andE₁ on normal derivations, consider the cases -- for t : Nf Γ (A ∧ B). -- -- Either t is (andI t₁ t₂) with t₁ : Nf Γ A and t₂ : Nf Γ B. -- In this case we just return t₁. -- -- Otherwise t is (hyp x es) which means that the conjunction is -- proven from hypothesis (x : Hyp Γ X) by eliminations -- es : Elims Γ X (A ∧ B) f. -- -- In this case, we would simply wish to append a andE₁ elimination -- to es. This is possible if f = lin. In case f = Branch, we -- have to distribute andE₁ to the branches. -- For falseE, there are zero branches, and for orE, there -- are two branches of type Nf (Γ ∙ _) (A ∧ B). -- We turn these into Nf (Γ ∙ _) A by recursively applying andE₁!. -- Since the branches are subterms of the original term t, -- the recursion is valid (i.e., does not lead to infinite regression). mutual andE₁! : ∀{Γ A B} → Nf Γ (A ∧ B) → Nf Γ A andE₁! (andI t₁ _) = t₁ andE₁! (hyp x es) = hyp x (andElims₁ es) andElims₁ : ∀ {Γ X A B f} (es : Elims Γ X (A ∧ B) f) → Elims Γ X A f andElims₁ (e ∷ es) = e ∷ andElims₁ es andElims₁ [] = andE₁ ∷ [] andElims₁ falseE = falseE andElims₁ (orE t₁ t₂) = orE (andE₁! t₁) (andE₁! t₂) -- Admissibility of andE₂ is analogous. mutual andE₂! : ∀{Γ A B} → Nf Γ (A ∧ B) → Nf Γ B andE₂! (andI _ t₂) = t₂ andE₂! (hyp x es) = hyp x (andElims₂ es) andElims₂ : ∀ {Γ X A B f} (es : Elims Γ X (A ∧ B) f) → Elims Γ X B f andElims₂ (e ∷ es) = e ∷ andElims₂ es andElims₂ [] = andE₂ ∷ [] andElims₂ (falseE) = falseE andElims₂ (orE t₁ t₂) = orE (andE₂! t₁) (andE₂! t₂) -- Absurdity elimination (falseE!). -- The only normal derivation of False is from a hypothesis X -- using eliminations es : Elims Γ X False f. -- To eliminate False into a proposition A, we append falseE -- to es if f = Lin, or distribute it over the brances if -- f = branch. mutual falseE! : ∀ {Γ A} → Nf Γ False → Nf Γ A falseE! (hyp x es) = hyp x (falseElims es) falseElims : ∀ {Γ X A f} → Elims Γ X False f → Elims Γ X A branch falseElims (e ∷ es) = e ∷ falseElims es falseElims [] = falseE falseElims falseE = falseE falseElims (orE t₁ t₂) = orE (falseE! t₁) (falseE! t₂) -- First we have to prove some basic properties, for instance -- that normal derivations are stable under context extensions -- and permutations. -- Renaming -- If we can prove C from a context Δ we can also prove it -- from Γ if every hypothesis in Δ can also be found in Γ. -- Thus, Γ can be a permutation of Δ or extension of Δ or both. -- A "renaming" r : Ren Γ Δ is a map from the hypotheses of Δ -- to the hypotheses of Γ. -- -- If we apply r to an address x : Hyp Δ A of hypothesis A in Δ, -- we get the address r x : Hyp Γ A of this hypothesis in Γ. Ren : (Γ Δ : Cxt) → Set Ren Γ Δ = ∀{A} → Hyp Δ A → Hyp Γ A -- A renaming r from Δ to Γ can be lifted to a renaming -- liftr r from Δ ∙ A to Γ ∙ A which leaves the position -- of the new hypothesis A unchanged on the top. liftr : ∀{Γ Δ A} (r : Ren Γ Δ) → Ren (Γ ∙ A) (Δ ∙ A) liftr r top = top liftr r (pop x) = pop (r x) -- The following mutual functions prove that Nf, Elim, and Elims -- are stable under renaming. -- This is a routine induction. Whenever we go under a binder, -- like in impI or orE, we need to lift the renaming -- to account for the new hypothesis. mutual ren : ∀{Γ Δ A} (r : Ren Γ Δ) (t : Nf Δ A) → Nf Γ A ren r (hyp x es) = hyp (r x) (renElims r es) ren r trueI = trueI ren r (impI t) = impI (ren (liftr r) t) ren r (andI t u) = andI (ren r t) (ren r u) ren r (orI₁ t) = orI₁ (ren r t) ren r (orI₂ t) = orI₂ (ren r t) renElims : ∀{Γ Δ A B f} (r : Ren Γ Δ) (es : Elims Δ A B f) → Elims Γ A B f renElims r [] = [] renElims r (e ∷ es) = renElim r e ∷ renElims r es renElims r falseE = falseE renElims r (orE t₁ t₂) = orE (ren (liftr r) t₁) (ren (liftr r) t₂) renElim : ∀{Γ Δ A B} (r : Ren Γ Δ) (e : Elim Δ A B) → Elim Γ A B renElim r (impE t) = impE (ren r t) renElim r andE₁ = andE₁ renElim r andE₂ = andE₂ -- We will need the following three instances of renaming, -- called weakenings. These add an unused hypothesis on top -- (weak and weakElim) or just below the top (weak'). weak : ∀{Γ A C} (t : Nf Γ C) → Nf (Γ ∙ A) C weak = ren pop weakElim : ∀{Γ A B C} (e : Elim Γ B C) → Elim (Γ ∙ A) B C weakElim = renElim pop weak' : ∀{Γ A B C} (t : Nf (Γ ∙ B) C) → Nf (Γ ∙ A ∙ B) C weak' = ren (liftr pop) -- Hereditary substitution. -- When showing the admissibility of -- -- impE : (t : Nf Γ (A ⇒ B)) (u : Nf Γ A) → Nf Γ B -- -- we have to treat the case that t = impI t' with -- t' : Nf (Γ ∙ A) B. How do we get a Nf Γ B? -- We substitute all uses of the top hypothesis in t' by u. -- -- However, if A is not an atomic proposition, -- this hypothesis might be under eliminations es, -- thus, we have to normalize the elimination of u by es. -- This might in turn trigger a substitution, for instance, -- if u is itself an impI u' and the first elimination of es -- is an impE v. -- -- Thus, a substitution might trigger new substitutions, -- and this process is called "hereditary substitution(s)". -- How can we be sure this process ever terminates? -- It turns out at all subsequent substitutions triggered -- by a substitution of u : Nf Γ A for a hypothesis x : Hyp Γ A, -- are substitutions of a u' : Nf Γ' A' for an a' : Hyp Γ' A', -- where A' is a subproposition of A. -- Thus, we can define substitution of u : Nf Γ A into t' : Nf (Γ ∙ A) B -- by an outer recursion on A and an inner recursion on t'. -- As a first step, we define the type of substitutions -- Sub A Γ Δ of a Nf Γ A into something in context Γ. -- Such a substitution replaces each hypothesis Hyp Δ C -- by a "result" Res A Γ C where the result can be a -- Nf Γ A if A = C and must be a hypothesis otherwise. data Res A Γ : (C : Form) → Set where rnf : (t : Nf Γ A) → Res A Γ A rhyp : ∀{C} (x : Hyp Γ C) → Res A Γ C Sub : (A : Form) (Γ Δ : Cxt) → Set Sub A Γ Δ = ∀{C} → Hyp Δ C → Res A Γ C -- Routinely, we prove that results can be weakened. weakRes : ∀{Γ A B C} (t : Res A Γ C) → Res A (Γ ∙ B) C weakRes (rnf t) = rnf (weak t) weakRes (rhyp x) = rhyp (pop x) -- We construct substitutions by the following two methods. -- A singleton substitution sg t is constructed from a single normal form t. -- It replaces the top hypothesis by t and all other hypotheses by themselves. sg : ∀ {Γ A} (t : Nf Γ A) → Sub A Γ (Γ ∙ A) sg t top = rnf t sg t (pop x) = rhyp x -- We can lift a substitution to one more hypothesis which remains fixed. lift : ∀{A Γ Δ B} (s : Sub A Γ Δ) → Sub A (Γ ∙ B) (Δ ∙ B) lift s top = rhyp top lift s (pop x) = weakRes (s x) -- Substitution of (s : Sub A Γ Δ) into normal forms (t : Nf Δ C) -- is now defined by lexicographic induction on (A, t), -- mutually with many auxiliary functions like substitution -- into eliminations, elimination of a normal form, -- and admissiblity of impE and orE for normal forms. -- Thanks to the dependent typing, most cases are forced. -- And Agda's termination checker scrutinizes our definition, -- to ensure correct use of the induction hypotheses. mutual -- Substitution is homeomorphic except for the case (hyp x es) -- in which we have to apply the substitution s to hypothesis x -- and eliminate the result by es. subst : ∀ A {Γ Δ} (s : Sub A Γ Δ) {C} (t : Nf Δ C) → Nf Γ C subst A s trueI = trueI subst A s (impI t) = impI (subst A (lift s) t) subst A s (andI t₁ t₂) = andI (subst A s t₁) (subst A s t₂) subst A s (orI₁ t) = orI₁ (subst A s t) subst A s (orI₂ t) = orI₂ (subst A s t) subst A s (hyp x es) = elimsRes A (s x) (substElims A s es) substElims : ∀ A {Γ Δ} (s : Sub A Γ Δ) {B C f} (es : Elims Δ B C f) → Elims Γ B C f substElims A s [] = [] substElims A s (e ∷ es) = substElim A s e ∷ substElims A s es substElims A s falseE = falseE substElims A s (orE t₁ t₂) = orE (subst A (lift s) t₁) (subst A (lift s) t₂) substElim : ∀ A {Γ Δ} (s : Sub A Γ Δ) {B C} (e : Elim Δ B C) → Elim Γ B C substElim A s (impE t) = impE (subst A s t) substElim A s andE₁ = andE₁ substElim A s andE₂ = andE₂ -- If the result of substituting x is just an hypothesis y, -- we can just put the eliminations es back. -- Otherwise, if the result is a normal form t, we have -- to eliminate it recursively by es. -- This might trigger new substitutions in cases impE or orE. elimsRes : ∀ A {Γ B C f} (r : Res A Γ B) (es : Elims Γ B C f) → Nf Γ C elimsRes A (rhyp y) es = hyp y es elimsRes A (rnf t) es = elims A t es -- "elims" is the place where types are actually getting smaller -- but terms might get bigger by invokation of impE! and orE!. elims : ∀ A {Γ C f} (t : Nf Γ A) (es : Elims Γ A C f) → Nf Γ C elims A t [] = t elims .(A ⇒ B) t (impE {A} {B} u ∷ es) = elims B (impE! A t u) es elims .(A ∧ B) t (andE₁ {A} {B} ∷ es) = elims A (andE₁! t) es elims .(A ∧ B) t (andE₂ {A} {B} ∷ es) = elims B (andE₂! t) es elims .False t falseE = falseE! t elims .(A ∨ B) t (orE {A} {B} t₁ t₂) = orE! A B t t₁ t₂ -- The admissible eliminations of implication and disjunction, -- impE! and orE!, are invoked by "elims" and in turn invoke -- substitution. It is crucial that they are called with -- a strictly smaller proposition than the original call to subst had. -- Implication elimination -- Triggers new substitutions in case of (impI t). In the other case, -- we append the (impE u) to the eliminations es, distributing it to the -- branches in case of falseE or orE. impE! : ∀ A {Γ B} (t : Nf Γ (A ⇒ B)) (u : Nf Γ A) → Nf Γ B impE! A (impI t) u = subst A (sg u) t impE! A (hyp x es) u = hyp x (impElims A es u) impElims : ∀ A {Γ B X f} (es : Elims Γ X (A ⇒ B) f) (u : Nf Γ A) → Elims Γ X B f impElims A (e ∷ es) u = e ∷ impElims A es u impElims A [] u = impE u ∷ [] impElims A (falseE) u = falseE impElims A (orE t₁ t₂) u = orE (impE! A t₁ (weak u)) (impE! A t₂ (weak u)) -- Disjunction elimination -- Triggers new substitutions in case of orI. Otherwise, append -- an orE to the eliminations, possibly distributing it to the branches. orE! : ∀ A B {Γ C} (t : Nf Γ (A ∨ B)) (u : Nf (Γ ∙ A) C) (v : Nf (Γ ∙ B) C) → Nf Γ C orE! A B (orI₁ t) u v = subst A (sg t) u orE! A B (orI₂ t) u v = subst B (sg t) v orE! A B (hyp x es) u v = hyp x (orElims A B es u v) orElims : ∀ A B {Γ C X f} (es : Elims Γ X (A ∨ B) f) (u : Nf (Γ ∙ A) C) (v : Nf (Γ ∙ B) C) → Elims Γ X C branch orElims A B (e ∷ es) u v = e ∷ orElims A B es u v orElims A B [] u v = orE u v orElims A B (falseE) u v = falseE orElims A B (orE t₁ t₂) u v = orE (orE! A B t₁ (weak' u) (weak' v)) (orE! A B t₂ (weak' u) (weak' v)) -- Normalization. -- Finally, we can show that each derivation of Γ ⊢ A -- also has a normal derivation. -- -- The proof is by induction on the derivation, using -- the admissible elimination rules to compose the -- results of the induction hypotheses. nf : ∀{Γ A} (t : Γ ⊢ A) → Nf Γ A nf (hyp x) = hyp x [] nf trueI = trueI nf (andI t u) = andI (nf t) (nf u) nf (andE₁ t) = andE₁! (nf t) nf (andE₂ t) = andE₂! (nf t) nf (impI t) = impI (nf t) nf (impE t u) = impE! _ (nf t) (nf u) nf (orI₁ t) = orI₁ (nf t) nf (orI₂ t) = orI₂ (nf t) nf (orE t t₁ t₂) = orE! _ _ (nf t) (nf t₁) (nf t₂) nf (falseE t) = falseE! (nf t) -- QED -} -- Acknowledgements. -- -- I learned the trick of doing hereditary substitutions by just -- /structural/ recursion on types from Conor McBride. -- He sent me some Agda code that accomplished this for the STLC using -- the left-to-right elimination vectors we extended here to sum types. -- -- I could have learned it from Felix Joachimski and Ralph Matthes -- as well. The normalization algorithm presented here should be -- the computational content of their strong normalization proof -- for lambda-calculus with permutative conversions (AML 2003). -- However, I did not have the formalization skills back then -- I have now to translate their generous vector notation into -- the statically well-typed Elims. -- Literature. -- Dag Prawitz: -- Natural Deduction: A Proof-Theoretical Study -- Dover Publications (1965) -- Felix Joachimski, Ralph Matthes: -- Short proofs of normalization for the simply-typed lambda-calculus, -- permutative conversions and Gödel's T. -- Arch. Math. Log. 42(1): 59-87 (2003) -- Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker: -- A concurrent logical framework {I}: Judgements and properties. -- Technical report CMU-CS02-101, -- School of Computer Science, Carnegie Mellon University, Pittsburgh (2003) -- Andreas Abel: -- Implementing a normalizer using sized heterogeneous types. -- J. Funct. Program. 19(3-4): 287-310 (2009) -- Chantal Keller, Thorsten Altenkirch: -- Hereditary Substitutions for Simple Types, Formalized. -- MSFP@ICFP 2010: 3-10 -- Harley D. Eades III, Aaron Stump -- Exploring the Reach of Hereditary Substitution. -- International Conference on Types for Proofs and Programs, TYPES 2011, Bergen, Norway. -- Abstract: https://sites.google.com/site/types2011/program/types2011-talkswabstracts#Eades -- Talk: http://metatheorem.org/includes/talks/2012-TYPES.pdf -- Paper: http://metatheorem.org/includes/pubs/TYPES-2012.pdf