Any Questions?More on TypesThe Simply Typed Lambda-CalculusCIS 500Software FoundationsFall 2006October 4Any Questions?More on TypesReview: Typing Rulestrue : Bool(T-True)false : Bool(T-False)t1: Bool t2: T t3: Tif t1then t2else t3: T(T-If)0 : Nat(T-Zero)t1: Natsucc t1: Nat(T-Succ)t1: Natpred t1: Nat(T-Pred)t1: Natiszero t1: Bool(T-IsZero)Review: 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, t2: R, andt3: R.4. If 0 : R, then R = Nat.5. If succ t1: R, then R = Nat and t1: Nat.6. If pred t1: R, then R = Nat and t1: Nat.7. If iszero t1: R, then R = Bool and t1: Nat.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 Nat, then v is a numeric value.Proof:Recall the syntax of values:v ::= valuestrue true valuefalse false valuenv numeric valuenv ::= numeric values0 zero valuesucc nv successor valueFor part 1, if v is true or false, the result is immediate. But vcannot be 0 or succ nv, since the inversion lemma tells us that vwould then have type Nat, not Bool. Part 2 is similar.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 Nat, then v is a numeric value.Proof: Recall the syntax of values:v ::= valuestrue true valuefalse false valuenv numeric valuenv ::= numeric values0 zero valuesucc nv successor valueFor part 1,if v is true or false, the result is immediate. But vcannot be 0 or succ nv, since the inversion lemma tells us that vwould then have type Nat, not Bool. Part 2 is similar.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 Nat, then v is a numeric value.Proof: Recall the syntax of values:v ::= valuestrue true valuefalse false valuenv numeric valuenv ::= numeric values0 zero valuesucc nv successor valueFor part 1, if v is true or false, the result is immediate.But vcannot be 0 or succ nv, since the inversion lemma tells us that vwould then have type Nat, not Bool. Part 2 is similar.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 Nat, then v is a numeric value.Proof: Recall the syntax of values:v ::= valuestrue true valuefalse false valuenv numeric valuenv ::= numeric values0 zero valuesucc nv successor valueFor part 1, if v is true or false, the result is immediate. But vcannot be 0 or succ nv, since the inversion lemma tells us that vwould then have type Nat, not Bool.Part 2 is similar.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 Nat, then v is a numeric value.Proof: Recall the syntax of values:v ::= valuestrue true valuefalse false valuenv numeric valuenv ::= numeric values0 zero valuesucc nv successor valueFor part 1, if v is true or false, the result is immediate. But vcannot be 0 or succ nv, since the inversion lemma tells us that vwould then have type Nat, not Bool. Part 2 is similar.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof: By induction on a derivation of t : T.The T-True, T-False, and T-Zero cases are immediate, sincet in these cases is a value.Case T-If: t = if t1then t2else t3t1: Bool t2: T t3: TBy the induction hypothesis, either t1is a value or else there issome t01such that t1−→ t01. If t1is a value, then the canonicalforms lemma tells us that it must be e ither true or false, inwhich case either E-IfTrue or E-IfFalse applies to t. On theother hand, if t1−→ t01, then, by E-If,t −→ if t01then t2else t3.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof:By induction on a derivation of t : T.The T-True, T-False, and T-Zero cases are immediate, sincet in these cases is a value.Case T-If: t = if t1then t2else t3t1: Bool t2: T t3: TBy the induction hypothesis, either t1is a value or else there issome t01such that t1−→ t01. If t1is a value, then the canonicalforms lemma tells us that it must be e ither true or false, inwhich case either E-IfTrue or E-IfFalse applies to t. On theother hand, if t1−→ t01, then, by E-If,t −→ if t01then t2else t3.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof: By induction on a derivation of t : T.The T-True, T-False, and T-Zero cases are immediate, sincet in these cases is a value.Case T-If: t = if t1then t2else t3t1: Bool t2: T t3: TBy the induction hypothesis, either t1is a value or else there issome t01such that t1−→ t01. If t1is a value, then the canonicalforms lemma tells us that it must be e ither true or false, inwhich case either E-IfTrue or E-IfFalse applies to t. On theother hand, if t1−→ t01, then, by E-If,t −→ if t01then t2else t3.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof: By induction on a derivation of t : T.The T-True, T-False, and T-Zero cases are immediate, sincet in these cases is a value.Case T-If: t = if t1then t2else t3t1: Bool t2: T t3: TBy the induction hypothesis, either t1is a value or else there issome t01such that t1−→ t01. If t1is a value, then the canonicalforms lemma tells us that it must be e ither true or false, inwhich case either E-IfTrue or E-IfFalse applies to t. On theother hand, if t1−→ t01, then, by E-If,t −→ if t01then t2else t3.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof: By induction on a derivation of t : T.The T-True, T-False, and T-Zero cases are immediate, sincet in these cases is a value.Case T-If: t = if t1then t2else t3t1: Bool t2: T t3: TBy the induction hypothesis, either t1is a value or else there issome t01such that t1−→ t01. If t1is a value, then the canonicalforms lemma tells us that it must be e ither true or false, inwhich case either E-IfTrue or E-IfFalse applies to t. On theother hand, if t1−→ t01, then, by E-If,t −→ if t01then t2else t3.ProgressTheorem: Suppose t is a well-typed term (that is, t : T for sometype T). Then either t is a value or else there is some t0witht −→ t0.Proof: By induction on a derivation