Extending Higher-Order Unification to SupportProof IrrelevanceJason ReedCarnegie Mellon UniversitySeptember 11, 20031What is Proof Irrelevance?• The idea that all proofs of a proposition are equal.• (The term appears in the literature occasionally meaning‘irrelevance everywhere’, of all proof equality becoming trivial,especially in proofs of the form ‘X and Y imply proofirrelevance’ — this is not what we are talking about)• “Intensionality, Extensionality and Proof Irrelevance in ModalType Theory” [Pfenning ’01] treats irrelevance as amodality.• Compare with fact that both logic “linear everywhere” andlogic with linearand intuitionistic variables are possible.2OutlineI. MotivationII. Type TheoryIII. UnificationIV. Patterns3What good is Proof Irrelevance?• A couple examples, using the dependent type theory LF[Harper, Honsell, Plotkin ’93] as a starting point.• Examples shaped and motivated throughout by the designchoices oftwelf, [Pfenning, Sch¨urmann ’99] an implementationof LF and associated algorithms.• Motivation #1: adequate encodings• Motivation #2: proof compaction4Motivation #1: Adequate Encodings• Desirable property for an encoding of a theory into a logic likeLF isadequacy, existence of a compositional bijectionbetween object-language terms and (canonical) LF objects.• Compositional, i.e. substitution commutes with translation.• Proof irrelevance as a modality makes adequate encodings ofcertain concepts much easier.5Adequate Encodings (2)• Take the standard encoding of the untyped λ-calculus:tm : type lam : (tm → tm) → tmapp : tm → tm → tm• How to get ‘strict lambda calculus’, each λ var to occur at leastonce? (Historical footnote: Church’s original calculus like this)• Easy to code up a definition of occurrence:occurs : (tm → tm) → typeoccurs app1 : occurs (λx.app (M x) (N x)) ← occurs (λx.(M x))occurs app2 : occurs (λx.app (M x) (N x)) ← occurs (λx.(N x))occurs var : occurs (λx.x)...• So occurs (λx.M x) type of proofs that x occurs in M6Adequate Encodings (3)• We would try lam : Πt:(tm → tm).(occurs t) → tm but itdoesn’t work right.• Generally lots of proofs that x occurs, as many as occurrences!• lam t P16= lam t P2for P16= P2• Failure of adequacy!• Don’t want to care about which proof of occurrence.• That is, we want an ‘irrelevant arrow’. We’ll write bracketsaround the argument to suggest:lam : Πt:(tm → tm).[(occurs t)] → tm• Need lam t [P1] = lam t [P2] for any proofs P1, P2to recoveradequacy.7Motivation #2: Proof Compaction• Domain: Proof-Carrying Code [Necula, Lee ’96]• Problem: proofs are big — There’s a market for ways ofmaking them smaller.• Maybe we can omit subterms that can be recovered by theconsumer?• This is realistic; big proofs of undecidable properties can havelots of space-consuming little subproofs of (efficiently)decidable properties.• Assert the existence of the little subproofs, let the consumerreconstruct them.8Proof Compaction (2)• But what if the consumer reconstructs a different proof of thesame fact?• Coordinating reconstruction algorithms at both ends possible,but a headache• Instead useirrelevant subproof requirements in the signature.• This permits the receiver to safely reconstructany validsubproof.• There’s a result that states that after replacing an irrelevantsubterm with another of the same type, the whole term is stillwell-typed.• Not true in ordinary LF because of dependent types.• Another win: avoiding constructing intermediate proof terms9Extending LF Type Theory• Normally, we can check applications for equality with the ruleΓ ` M = M0: Πx:A.B Γ ` N = N0: AΓ ` M N = M0N0: {N/x}B• For irrelevant functions, we want the arguments not to matter.So we have:Γ ` M = M0: Πx:[A].B Γ ` N = N0: [A]Γ ` M [N] = M0[N0] : {N/x}Band say that any two objects at [A] are equal.• (Just as A → B abbreviates Πx:A.B where x doesn’t occur inB, we’ll say [A] → B means Πx:[A].B)10Extending LF (2)• Naturally, we get terms at irrelevant-Π type from irrelevantlambdas:Γ, x : [A] ` M : BΓ ` λx:[A].M : Πx:[A].B• Forces us to consider whatirrelevant hypotheses mean.• Answer: x : [A] assumes that some object at type A exists, butwe are not allowed to analyze its structure, only use the barefact that its type is inhabited.• Knee-jerk reaction to a new kind of hypothesis: what kind ofobjects can we substitute for it?• New typing judgment: Γ ` M : [A]. Think “M is an irrelevantobject at type A” or “M is an inhabitation witness for type A”11Irrelevance Rules• Defining inference rule: ([Γ0] just means x1: [A1], . . . xn: [An])Γ, Γ0` M : A Γ, [Γ0] ` A : typeΓ, [Γ0] ` M : [A]Note hypothesis rule is still merely Γ, x : A ` x : A notanything that would allow Γ, x : [A] ` x : A. (Γ, x : [A] ` x : [A]is admissible)• x : [A] is a weaker hypothesis than x : A, and M : [A] is aweaker assertion than M : A; When judging M : [A] one gets touse irrelevant hypotheses ‘unbracketed’.• Γ ` M : A implies Γ ` M : [A].• See the tech report for why Γ, [Γ0] ` A : type needed.12Higher-Order Pattern Unification• How twelf, for instance, thinks of unification. Used for typereconstruction, logic programming queries.•Higher-order: allow variables to be of function type.• Restricted to thepattern fragment [Miller ’91], because wewant unification to bedecidable and have unique mostgeneral unifiers.• The fact that type reconstruction relies on unification is a bigmotivation for this: don’t want type-checking to beundecidable or have an ambiguous answer.•[Dowek, Hardin, Kirchner, Pfenning ’96] worked out an algorithmfor this case; we extended it to cover LF with irrelevance.• Just few interesting corner cases — see paper for details13Unification• Stepping back a bit, a unification problem looks like∃U1. . . ∃Un.M1.= N1∧ · · · Mn.= Nn• Find terms for U1, . . . , Unso all equations satisfied, ordetermine that no such exist.• Must allow open (allowing ∃-quantified variables to occur)instantiations, or else immediate undecidability! For instance,∃U.∃V.U.= c V . Answer: U ← c V• Otherwise, exists closed term at V ’s type? Undecidable.14Unification (2)• Irrelevance means that equations that look straightforward areactually trivial in the same way as the above one.• Consider∃U.c [k].= c [U] (∗)• If this were∃U.c k.= c