Typed Arithmetic Expressions CS 550 Programming Languages Jeremy Johnson TAPL Chapters 3 and 5 1 Types and Safety Evaluation rules provide operational semantics for programming languages. The rules provide state transitions for an abstract machine that evaluates terms in the language. Evaluating a term can result in a value or get stuck in an erroneous state. We would like to be able to tell, without actually evaluating the term, whether or not it will get stuck. Type rules are introduced to associate types with terms. A term t is

well-typed if there is some type T such that t has type T. The safety property says that well-typed terms do not lead to erroneous states, i.e. do not go wrong Safety is progress plus preservation. A well-typed term is either a value or it transitions to another well-typed term. 2 Outline Arithmetic Expressions Syntax and evaluation rules Untyped arithmetic expressions Typed arithmetic expressions Safety well typed terms do not get stuck

3 Boolean Expressions Syntax Evaluation t ::= if true then t2 else t3 t2 (E-IfTrue) true false

if t then t else t v ::= true false if false then t2 else t3 t3 (E-IfFalse) t1 t1 if t1 then t2 else t3 if t1 then t2 else t3 (E-If)

Derivation s = if true then false else false t = if s then true else true u = if false then true else true E-IfTrue E-If E-If s false tu if t then false else false if u then false else false

Determinacy Theorem [Determinacy of one-step evaluation]. If t t and t t, then t = t. Proof. By induction on a derivation of t t. Determinacy Proof. By induction on a derivation of t t. Three cases: E-IfTrue, E-IfFalse and E-If. The first two are base cases. 1) E-IfTrue. t = if true then t2 else t3 and t = t2 E-IfFalse and E-If are not applicable, so t = t = t2

Determinacy Proof. By induction on a derivation of t t. Three cases: E-IfTrue, E-IfFalse and E-If. 2) E-IfFalse. t = if false then t2 else t3 and t = t3 E-IfTrue and E-If are not applicable, so t = t = t3 Determinacy Proof. By induction on a derivation of t t. Three cases: E-IfTrue, E-IfFalse and E-If. 3) E-If. t = if t1 then t2 else t3 and t = if t1 then t2 else t3 and t1 t1 E-IfTrue and E-IfFalse are not applicable since t1

is not a normal form. Determinacy Proof. By induction on a derivation of t t. 3) E-If. t = if t1 then t2 else t3 and t = if t1 then t2 else t3 with t1 t1 E-IfTrue and E-IfFalse are not applicable since t1 is not a normal form, so t = if t 1 then t2 else t3 with t1 t1. By induction t1 = t1 and t = t. Normal Forms Definition. A term t is in normal form if no evaluation rule applies to it.

Theorem. Every value is in a normal form and every term t that is in normal form is a value. Proof. Immediate from rules. Show contrapositive by induction on t. Normal Forms Theorem. Every value is in a normal form and every term t that is in normal form is a value. Show contrapositive by induction on t. If t is not a value then it is not a normal form t = if t1 then t2 else t3

1. t1 = true E-IfTrue applicable 2. t1 = false E-IfFalse applicable 3. else by induction t1 t1 and E-If is applicable Multi-step Evaluation Definition. Multistep evaluation * is the reflexive, transitive closure of one step evaluation. Uniqueness of Normal Forms Theorem [Uniqueness of normal forms]. If t * u and t * v, where u and v are normal forms, then u = v.

Proof. Corollary of determinacy. Termination of Evaluation Theorem [Termination of evaluation]. For every term t, there is a normal form t such that t * t. Proof. Each evaluation step decreases the size and since size is natural number and the natural numbers are well founded the size must reach 1. Arithmetic Expressions Syntax

Evaluation t ::= t1 t1 0 succ t pred t iszero t nv ::= 0

succ nv (E-Succ) succ t1 succ t1 pred 0 0 pred (succ nv1) nv1 (E-PredZero) (E-PredSucc) t1 t1

(E-Pred) pred t1 pred t1 iszero 0 true iszero (succ nv1) false (E-IsZeroZero) (E-IsZeroSucc) t1 t1 (E-IsZero)

iszero t1 iszero t1 Derivation pred (succ (pred 0)) * 0 pred (succ (pred 0)) pred (succ 0) 0 E-PredZero pred 0 0 E-Succ succ (pred 0) succ 0 E-Pred pred (succ (pred 0)) pred (succ 0)

Stuck Terms Definition. A stuck term is a term that is in normal form but is not a value. E.G. pred false if 0 then true else false Typing Relation Definition. A typing relation, t : T, is defined by a set of inference rules assigning types to terms. A term is well-typed if there is some T such that t : T. For arithmetic expressions there are two types: Bool and Nat

Insisting that evaluation rules are only applied to proper types prevents things from going wrong (getting stuck). Typing Relation Syntax Typing Rules T ::= true : Bool

(T-True) false : Bool (T-False) Bool t1 : Bool, t2 : T, t3 : T if t1 then t2 else t3 : T (T-If)

Typing Relation Syntax Typing Rules T ::= 0 : Nat (T-Zero) t1 : Nat

(T-Succ) Nat *The typing relation is conservative. I.E. some terms that do not get stuck are not well-typed. if (iszero 0) then 0 else false Want type checking to be easy succ t1 : Nat t1 : Nat

(T-Pred) pred t1 : Nat t1 : Nat iszero t1 : Bool (T-IsZero) Inversion Lemma 1. If true : R, then R = Bool. 2. If false : R, then R = Bool. 3. If if t1 then t2 else t3 : R, then t1 : Bool and

t2 : R and t3 : 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 Uniqueness of Types Theorem. Each term t has at most one type. Proof. By induction on t using the inversion lemma. The inversion lemma provides a recursive algorithm for computing types.

Safety = Progress + Preservation Progress. A well-typed term is not stuck (either it is a value or it can take a step according to the evaluation rules). Preservation. If a well-typed term takes a step of evaluation, then the resulting term is well-typed. Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T.

Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T. Base Cases: T-True, T-False, T-Zero, then t is a value. Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T. Case: T-If t = if t1 then t2 else t3, t1 : Bool, t2, t3 : T

By induction either t1 has a value E-IfTrue or E-IfFalse is applicable. Else t1 t1 and E-If is applicable Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T. Case: T-Succ t = succ t1 and t1 : Nat By induction either t1 has a value t is a value else t1 t1 and E-Succ is applicable

Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T. Case: T-Pred t = pred t1 and t1 : Nat By induction either t1 has a value E-PredZero or E-PredSucc is applicable else t1 t1 and EPred is applicable Progress Theorem. If t : T, then t is a value or there is a t such that t t. Proof. By induction on the derivation of t : T.

Case: T-IsZero t = iszero t1 and t1 : Nat By induction either t1 is a value either EIsZeroZero or E-IsZeroSucc is applicable else t1 t1 and E-IsZero is applicable Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Case T-True, T-False, and T-Zero.

t = true and T = Bool. t = false and T = Bool. t = 0 and T = Nat In all of these cases, t is a value and there is no t t and theorem is vacuously true. Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Case T-If t = if t1 then t2 else t3, t1 : Bool, t2, t3 : T E-IfTrue t1 = true t = t2 : T

E-IfFalse t1 = false t = t3 : T E-If t1 t1 and by induction t1 : Bool t = if t1 then t2 else t3 : T (by T-If) Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Case T-Succ t = succ t1

T = Nat t1 : Nat E-Succ t1 t1 and by induction t1 : Nat t = succ t1 : Nat (by T-Succ) Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Case T-Pred t = pred t1

T = Nat t1 : Nat E-PredZero t1 = 0 and t = 0 : Nat (by T-Zero) E-PredSucc t1 = succ nv1 and t = nv1 : Nat (by TZero or T-Succ) E-Pred t1 t1 and by induction t1 : Nat t = pred t1 : Nat (by T-Pred) Preservation Theorem. If t : T and t t, then t : T. Proof. By induction on t : T. Case T-IsZero t = iszero t1

T = Bool t1 : Nat E-ZeroZero t1 = 0 and t = true : Bool (by T-True) E-IsZeroSucc t1 = succ nv1 and t = false : Bool (by T-False) E-IsZero t1 t1 and by induction t1 : Nat t = iszero t1 : Bool (by T-IsZero) Untyped Lambda Calculus Syntax

t ::= x x.t tt v ::= x.t Evaluation terms: variable abstraction application

values abstraction value t1 t1 (E-App1) t1 t2 t1 t2 t2 t2 (E-App2) v1 t2 v1 t2

(x.t12)v2 [x v2] t12 (E-AppAbs) Call by value Substitution Definition. [x s] x = s [x s] y = y [x s] (y.t1) = y. [x s] t1 if y x if y x &

yFV(s) [x s] (t1 t2) = [x s] t1 [x s] t2 Function Types Extend types to include functions x:true [returns Bool] x. y.y [returns function]

x.if x then 0 else 1 [returns Nat, expects Bool] TT Definition. T ::= T T | Bool Bool Bool, (Bool Bool) (Bool Bool) T1 T2 T3 T1 (T2 T3) Typing Relation Type rules for functions x : T1 t2 : T2

x:T1.t2 : T1 T2 Need three term relation, t : T, that includes typing context (set of assumptions on free variables) , x : T1 t2 : T2 x:T1.t2 : T1 T2 Simply Typed Lambda Calculus Syntax t ::= x

x:T.t tt v ::= x:T.t Evaluation terms: variable abstraction application values abstraction value

t1 t1 (E-App1) t1 t2 t1 t2 t2 t2 (E-App2) v1 t2 v1 t2 (x:T11.t12)v2 [x v2] t12 (E-AppAbs)

Lambda Calculus Typing Syntax T ::= T T ::= , x:T Type Rules types: function types

contexts empty context term variable binding x:T x:T (T-Var) , x : T1 t2 : T2 x:T1.t2 : T1 T2

t1 : T1 T2 t1 t2 : T2 (T-Abs) t2 : T1 (T-App) Substitution Lemma Theorem. If , x : S t : T and s : S, then [x s]t : T. Safety

Theorem [Progress]. Suppose t is a closed (no free variables), well-typed term (i.e. t : T). Then either t is a value or else there is some t with t t. Theorem [Preservation]. If t : T and t t, then t : T. Erasure Definition. The erasure of a simply typed term t is defined by erase(x) = x erase(x:T1.t2 ) = x.erase(t2)

erase(t1t2) = erase(t1) erase(t2) Theorem. If t t, then erase(t) erase(t). If erase(t) m, then there is a simply typed term t such that t t and erase(t) = m. Curry-Howard Correspondence Logic 1. Propositions 2. P Q 3. P Q 4. Proof of P

5. Prop P is provable Programming Languages 1. Types 2. Type P Q 3. Type P Q 4. Term t of type P 5. Type P is inhabited by some term A term of - is a proof of a logical proposition corresponding to its type.