CIS 500Software FoundationsFall 2006October 9ReviewChurch encoding of lists... will not be on the exam. :-)Briefly, though, here’s the intuition:c4= λs. λz. s (s (s (s z)))[v1;v2;v3;v4] = λs. λz. s v1(s v2(s v3(s v4z)))Church encoding of lists... will not be on the exam. :-)Briefly, though, here’s the intuition:c4= λs. λz. s (s (s (s z)))[v1;v2;v3;v4] = λs. λz. s v1(s v2(s v3(s v4z)))Church encoding of lists... will not be on the exam. :-)Briefly, though, here’s the intuition:c4= λs. λz. s (s (s (s z)))[v1;v2;v3;v4] = λs. λz. s v1(s v2(s v3(s v4z)))Typing derivationsExercise 9.2.2: Show (by drawing derivation trees) that thefollowing terms have the indicated types:1. f:Bool→Bool ` f (if false then true else false) :Bool2. f:Bool→Bool `λx:Bool. f (if x then false else x) : Bool→BoolThe two typing relationsQuestion: What is the relation between these two statements?1. t : T2. ` t : TFirst answer: These two relations are completely different things.IWe are dealing with several different small programminglanguages, each with its own typing relation (between terms inthat language and types in that language)IFor the simple language of numbers and booleans, typing is abinary relation between terms and types (t : T).IFor λ→, typing is a ternary relation between contexts, terms,and types (Γ ` t : T).(When the context is empty — because the term has no freevariables — we often write ` t : T to mean ∅ ` t : T.)The two typing relationsQuestion: What is the relation between these two statements?1. t : T2. ` t : TFirst answer: These two relations are completely different things.IWe are dealing with several different small programminglanguages, each with its own typing relation (between terms inthat language and types in that language)IFor the simple language of numbers and booleans, typing is abinary relation between terms and types (t : T).IFor λ→, typing is a ternary relation between contexts, terms,and types (Γ ` t : T).(When the context is empty — because the term has no freevariables — we often write ` t : T to mean ∅ ` t : T.)Conservative extensionSecond answer: The typing relation for λ→conservatively extendsthe one for the simple language of numbers and booleans.IWrite “language 1” for the language of numbers and booleansand “language 2” for the simply typed lambda-calculus withbase types Nat and Bool.IThe terms of language 2 include all the terms of language 1;similarly typing rules.IWrite t :1T for the typing relation of language 1.IWrite Γ ` t :2T for the typing relation of language 2.ITheorem: Language 2 conservatively extends language 1: If tis a term of language 1 (involving only booleans, conditions,numbers, and numeric operators) and T is a type of language1 (either Bool or Nat), then t :1T iff ∅ ` t :2T.Preservation (and Weaking,Per mutation, Substitution)Review: Proving progressLet’s quickly review the steps in the proof of the progress theorem:Iinversion lemma for typing relationIcanonical forms lemmaIprogress theoremInversionLemma:1. If Γ ` true : R, then R = Bool.2. If Γ ` false : R, then R = Bool.3. If Γ ` if t1then t2else t3: R, then Γ ` t1: Bool andΓ ` t2, t3: R.4. If Γ ` x : R, thenx:R ∈ Γ.5. If Γ ` λx:T1.t2: R, then R = T1→R2for some R2withΓ, x:T1` t2: R2.6. If Γ ` t1t2: R, then there is some type T11such thatΓ ` t1: T11→R and Γ ` t2: T11.InversionLemma:1. If Γ ` true : R, then R = Bool.2. If Γ ` false : R, then R = Bool.3. If Γ ` if t1then t2else t3: R, then Γ ` t1: Bool andΓ ` t2, t3: R.4. If Γ ` x : R, then x:R ∈ Γ.5. If Γ ` λx:T1.t2: R, thenR = T1→R2for some R2withΓ, x:T1` t2: R2.6. If Γ ` t1t2: R, then there is some type T11such thatΓ ` t1: T11→R and Γ ` t2: T11.InversionLemma:1. If Γ ` true : R, then R = Bool.2. If Γ ` false : R, then R = Bool.3. If Γ ` if t1then t2else t3: R, then Γ ` t1: Bool andΓ ` t2, t3: R.4. If Γ ` x : R, then x:R ∈ Γ.5. If Γ ` λx:T1.t2: R, then R = T1→R2for some R2withΓ, x:T1` t2: R2.6. If Γ ` t1t2: R, thenthere is some type T11such thatΓ ` t1: T11→R and Γ ` t2: T11.InversionLemma:1. If Γ ` true : R, then R = Bool.2. If Γ ` false : R, then R = Bool.3. If Γ ` if t1then t2else t3: R, then Γ ` t1: Bool andΓ ` t2, t3: R.4. If Γ ` x : R, then x:R ∈ Γ.5. If Γ ` λx:T1.t2: R, then R = T1→R2for some R2withΓ, x:T1` t2: R2.6. If Γ ` t1t2: R, then there is some type T11such thatΓ ` t1: T11→R and Γ ` t2: T11.Canonical FormsLemma:1. If v is a value of type Bool, then v is either true or false.2. If v is a value of type T1→T2, then v has the form λx:T1.t2.Canonical FormsLemma:1. If v is a value of type Bool, then v is either true or false.2. If v is a value of type T1→T2, then v has the form λx:T1.t2.ProgressTheorem: Suppose t is a closed, well-typed term (that is, ` t : Tfor some T). Then either t is a value or else there is some t0witht −→ t0.PreservationTheorem: If Γ ` t : T and t −→ t0, then Γ ` t0: T.Steps of proof:IWeakeningIPermutationISubstitution preserves typesIReduction preserves types (i.e., preservation)Weakening and PermutationWeakening tells us that we can add assumptions to the contextwithout losing any true typing statements.Lemma: If Γ ` t : T and x /∈ dom(Γ), then Γ, x:S ` t : T.Moreover, the latter derivation has the same depth as the former.Permutation tells us that the order of assumptions in (the list) Γdoes not matter.Lemma: If Γ ` t : T and ∆ is a permutation of Γ, then ∆ ` t : T.Moreover, the latter derivation has the same depth as the former.Weakening and PermutationWeakening tells us that we can add assumptions to the contextwithout losing any true typing statements.Lemma: If Γ ` t : T and x /∈ dom(Γ), then Γ, x:S ` t : T.Moreover, the latter derivation has the same depth as the former.Permutation tells us that the order of assumptions in (the list) Γdoes not matter.Lemma: If Γ ` t : T and ∆ is a permutation of Γ, then ∆ ` t : T.Moreover, the latter derivation has the same depth as the former.Weakening and PermutationWeakening tells us that we can add assumptions to the contextwithout losing any true typing statements.Lemma: If Γ ` t : T and x /∈ dom(Γ), then Γ, x:S ` t : T.Moreover, the latter derivation has the same depth as the former.Permutation tells us that the order of assumptions in (the list) Γdoes not matter.Lemma: If Γ ` t : T and ∆ is a permutation of Γ, then ∆ ` t : T.Moreover, the latter derivation has the same depth as the