SPECIAL TOPICS ECEN 5023
Popular in Course
Popular in ELECTRICAL AND COMPUTER ENGINEERING
This 189 page Class Notes was uploaded by Mrs. Lacy Schneider on Thursday October 29, 2015. The Class Notes belongs to ECEN 5023 at University of Colorado at Boulder taught by Staff in Fall. Since its upload, it has received 18 views. For similar materials see /class/231800/ecen-5023-university-of-colorado-at-boulder in ELECTRICAL AND COMPUTER ENGINEERING at University of Colorado at Boulder.
Reviews for SPECIAL TOPICS
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 10/29/15
References gt So far the languages that we39ve looked at do not include operations that change state gt For example we did not include a way to change the value of the first element of a pair gt Today we add references pointers to the simply typed lambda calculus gt The new operations are gt allocate a location in memory and initialize it with a value such as new int 3 in C gt read the value from a memory location such as p in C gt change the value in a memory location such as p 6 in C References Syntax and Type Rules e l ref 9 allocate l e dereference l e 9 update v l I locations T l Ref T Type rules I39FeT I39FeRefT I39FrefeRefT I39FleT FFeyRefT I39FegT I39Feleg Unit References Operational Semantics Change to the framework need to model the heap Abstractly we can use a function from locations to values denoted by u MAHMM l WW M0V refvlluallUHvLu lllpavlp Ivlugtunitllwvlu Evaluation contexts ElrefEllElEelvE Towards Type Safety gt If this language is to satisfy progress then all intermediate steps need to be well typed gt With the addition of references we now have a new kind of value locations that can appear during intermediate steps gt We introduce a store typing X to keep track of the type allowed at each location XI T I l X h I Ref T Definition A store In is well typed written I l X h u if domu domX and for every I E domu I l X h MU XI Towards Type Safety Lemma Subject Reduction Ifl39iXFe Tandl39iXFLandeiluae ilu thenforsome X WhereXgX I39iX Fe Tandl39iX Flu Proof By cases on e i u a e i u I domm refviL MHIHvM39 Since I i X F ref v T T Ref T for some T Pick some I where I domu and therefore I dom and let X Igt gtT X Thenl39iX FLRef T and I39iX FIgt gtvu Case Towards Type Safety Case ILL u l M a v l M 39 So I l X F ll T By inversion I l X F I Ref T and then XI T Then because u is well typed we have I l X F v T Case Ivlugtunitllwvu We have I l X F I v T then by inversion T Unit and for some T I l XFIRef T and I l XF v T Then again by inversion XI T and then because u is well typed we have I l X F MU T Then because v has the same type as MU we have I l X F I l gt vu And of course I l X F unit Unit Remaining cases are unchanged from the previous proof e raiseelttyewithe Type Rules I39heTexn I39he1T I39hegTeanT I39hraiseeT I39htryelwithegT There are several possible choices for Tex 1 Set Tex to something like Int or String 2 Use an extensible type such as extensible variants in ML or a base class like Throwable in Java Exceptions Operational Semantics The main computational rules are try v With e a v try raise v With e a e v We also need to specify how an exception propagates up In a small step semantics with congruence rules we have the following for propagating through function applications raise v e a raise v v1 raise V2 raise V2 You also need similar rules for propagating through every other kind of expression Exceptions Propagation with Contexts We can39t add a case for trywith to E because then an exception could skip over a surrounding trywith Instead we use two kinds of contexts E iraiseE Eh i Eh e i v Eh i raise Eh i try Eh With e A e 1 e 2 Ehe gt Ehe Eraise v gt gt raise v 1 I Ehtry Eraise v With e gt Ehtry raise v With e 2 is needed for uncaught exceptions Source Programming Languages and Lambda Calculi by Felleisen and Flatt Normalization Definition A program is normalizable if evaluation halts after a finite number of steps Theorem Every well typed program of the simply typed lambda calculus is normalizable The proof of this theorem demonstrates a proof technique called logical relations Logical Relations gt Motivation need a stronger induction hypothesis than just e is normalizable gt We define for each type T a predicate RT on programs closed expressions of type T gt The predicate RTe will be stronger then e is normalizable gt The definition for R7 we39ll use is e is normalizable e is quot quot RT19 RTJe e Rheae RT Tglel gt The family of relations RT for all the types T in the langauge is called a logical relation Normalization proof outline 1 Show that every well typed program is in R7 2 Show that every program in R7 is normalizable This step is immediate from the definition of RT Every well typed program is in R7 Lemma Ifh e T then RTe We39ll want to prove this by rule induction on F e T but when we look at subderivations we39ll be considering open expressions with non empty environments so the induction hypothesis will not apply The solution is to generalize the lemma Lemma Ifl39 h e T then RTe Where 5 maps every variable X E dom39 to a closed value v Where letting T l X we have h v T and RTv Every well typed program is in R7 Proof X 39 T E I Case 1 rpx T Because X T E I we have F X T and RTX C ase 2 I F true bool We have F true bool and Rheatrue because true is already a value I39X T1 F e T2 39FX T1e T1gtT2 39 To show that RTIHT2XI T1e we need to show that 1 X2 T1e is normalizable and 2 for any e RTle implies RT2XI T1e e We have 1 because a is already a value It remains to address 2 Because RTle there is a value v such that e v In order to apply the induction hypothesis on the body e we need to show that RTlv Case 4 Interlude Lemma Ifh e T and e a e then RTe iffR e Proof By induction on T First it is clear that e halts ifF e halts If T bool then there is nothing more to show If T T1 a T2 then we need to show 1 RTe RTe and 2 RTe lt RTe For 1 suppose 5 T1 and R71 By definition we have RTQe 5 Using the assumption 9 a e we have e s a e 5 Then by the induction hypothesis for T2 we have RTQe s We therefore have RTe Direction 2 is similar D Back to Every well typed program is in R7 80 now we know that RTlv and can apply the induction hypothesis so RT2SX gt gt ve 5 But AX T1 59 9 X gt gt ve and then using the lemma again gives us RT2XI T1e 9 Then by definition we have RTIHT2XI T1 9 rheliTnHTlQ i hfgiTn i i 81 82 T12 I From the induction hypotheses we have RTHHTIQ91 and RT11582 Then by the definiton of RTHHT12 we have RT12sel 92 Case 5 Decomposition Lemma Lemma Decomposition Ife T then either e is a value or there is an E and r Where eEr andE Tandr andrisa redex Proof by rule induction on e T Case 1 Case 5 O is a value Subcase 5a Suppose e1 is a value From e1 nat we know that e1 is a numerical value by the canonical forms lemma Therefore succ e1 is a value Subcase 5a Suppose e1 is not a value From the induction hypothesis there is an E1 and r such that e1 E1r E1 nat r 5 and r is a redex Then we let E succ E1 so e Er and E 5 nat and we use the same r to conclude Decomposition Lemma continued e1bool e2T e3T case 4 if e1 then e2 else e3 T Subcase 4a Suppose e1 is a value Then by the canonical forms lemma e1 is either true or false Subsubcase 4ai Suppose e1 true Then let E and r e SowehaveeEr E T T r Tand raeg Subsubcase 4ai Suppose e1 false Same as 4ai except r e3 Subcase 4b Suppose e1 is not a value From the induction hypothesis there is an E1 and r such that e1 E1r E1 bool r S and r is a redex Then we let E if E1 then e2 else e3 so e EM and E S a T and we use the same r to conclude Subject Reduction Lemma Lemma Subject Reduction Ife Tandeae thene T Proof by case analysis on e T Case 1 There is no 9 such that O a e Case 6 pred s Proof by case analysis on e a e Subcase 6a So 9 O and O nat Subcase 6b So 9 nv and nv nat Replacement Lemma Lemma Replacement IfETandethenEeT By rule induction on E 5 a T Case 1 T T So E and e T Since e e we have Ee T E1 5 bool case 2 if E1 then e1 else e2 5 a T So E if E1 then e2 else e3 By the induction hypothesis we have E1e bool Therefore Ee T E1 5 nat So E succ E1 By the induction hypothesis we have E1e nat Therefore Ee nat Progress Lemma Lemma Progress lfe T then either e is a value or an evaluation rule applies to e ie 3e e i gt e Proof From the decomposition lemma either either e is a value OR there isan Eand rwhereeErand ETand randrisa redex Case 1 Suppose e is a value Then we are done Case 2 Suppose there is an E and r where e Er and E 5 a T and r 5 and r is a redex By definition of redex there is an r such that r a r Then we have e gt Er and we are done Subterm Typing Lemma Lemma Subterm Typing Ife T and e Er then there is an 5 such that E 5 a T and 5 f Proof By rule induction on e T case 1 So E and r 0 and we have E hat a hat and r nat 39 1 Case 5 By case analysis on E E is either or succ E1 Subcase 5a E Then r e E hat a hat and r nat Subcase 5b e succ E1 Applying the induction hypothesis there is an 5 such that E1 hat and r 5 So succ E1 5 a hat and we conclude with the same r Preservation Lemma Lemma Preservation IfeTandegt gte thene T Proof By case analysis on e gt 9 There is just one case r a r Er gt Er So 9 EM and by the subterm typing lemma there is an 5 such that E 5 a T and r 5 Then by subject reduction lemma we have r 5 Then by the replacement lemma we have Er T and we are done D The Simply Typed Lambda Calculus STLC e X l true l false l X2 T e l e e v true l false l X T e T bool l T a T The constants true and false technically aren39t part of the STLC but you have to introduce some type other then function types to get off the ground P XITEl T 3 lrhxT l39htruebool Fhfalsebool 4 I397XT1heT2 l hXIT1SIT1gtTQ m I39helzTnHle FhfziTn l l 81 82 T12 STLC Evaluation AX T e v xgt gt ve EiiEeVE Ee gt Ee Properties of the STLC Type System Lemma Environment Weakening fl he Tandx dom39 then 39Xhe T Lemma Subsitution Ifl39xheTandl39he thenl39hxwe eT Theorem Type Safety Ifl39 h e T and e gt e then e is not stuck and e T Proof By the same sequence of lemmas as before decomposition subterm typing subject reduction replacement progress and preservation However the details of the proofs change which is left to you D The Curry Howard Correspondence From logic recall the rule of modus ponens If P implies Q and P then Q Compare this to the typing rule for function application I39he1T11HT12 I39htgT11 l he1 82 I T12 and think T11 x P T12 x Q Also from logic recall the rule for implication introduction lfyou can prove Q assuming P then P implies Ql Compare this to the typing rule for s 39X T1 h e T2 l hX2 T1e T1HT2 and think T1 x P and T2 x Q So it turns out types correspond to propositions and programs correspond to proofs Simple Types for Arithmetic Expressions gt Types are a way to categorize bits according to how they should be interpreted gt What does 0110101010 mean We could interpret those bits as an integer or as a memory address or gt A type system is something that filters out bad programs programs that may produce untrapped errors that write off the end of an array dereference a dangling pointer etc gt A type system restricts programs so that they may only use bits according to their intended interpretation Errors Getting Stuck and Type Safety Definition A program e is stuck if e is not a value and there is no evaluation rule that applies to it More formally stuck e E not value e A not Hee l gt e which is equivalent to not value e V Hee gt e Note getting stuck is how we model untrapped exceptions Definition A language is type safe if no well typed program can get stuck and the result is the same type as the original program More formally if e T and e gt e then e is not stuck and e T A Language of Arithmetic Expressions true false if e then e else e succ e pred e iszero e v true l false l nv nv O l succ nv T boollnat The Operational Semantics for Arithmetic Expressions Reduction rules e a e precl O a O precl succ nv nv iszero succ nv false iszero O a true if true then e2 else e3 8 e2 if false then e2 else e3 8 e3 Evaluation contexts E l succ E l pred E l iszero E l if E then e else e Evaluation rules El gt5 Ee gt gtEe Rt 5 gt gt 5 5 gt gt E e 5H A Type System for Arithmetic Expressions Type rules O nat true bool false bool e1bool e2T e3T if e1 then e2 else e3 T enat enat enat SLICC e 2 at pred e nat iszero e bool Exam ple derivation O nat 0 nat 0 nat M iszero O bool succ O nat P E d 5 0 3 quotat if iszero 0 then succ 0 else pred succ 0 nat Towards Proving Type Safety Lemma Progress lfe T then either e is a value or an evaluation rule applies to e ie He e gt gt e Lemma Preservation lfe T and e gt gt e then e T We39ll come back to these and prove them Proving Type Safety Theorem Ife T and e l gtT 9 then 9 is not stuck and e T Proof By rule induction on e l gtT 9 Case 9 l gtT 9 By the progress lemma 9 is either a value or an evaluation rule applies to e In either case 9 is not stuck by definition Case 9 l gt 9191 gt e The induction hypothesis is that for any 82 if el T and el l gtT 82 then 82 is not stuck and 82 T Because 9 T we have el T by the preservation lemma Then by the induction hypothesis 9 is not stuck and e T El O tline for Progress and Preservation subject reduction rrgtrr decompose replacem ent e T79 EM 9 T76 Er Well typed Evaluation Contexts Ebool elT e QIT ifEthenel elseegT TT Enat Enat succEnat predEnat E 5 nat iszero E 5 bool The Major Lemmas Lemma Decomposition Ife T then either e is a value or there is an E and r Where e Er and E 5 a T and r 5 andr is a redex Lemma Subject Reduction Ife T and e a e then e T Lemma Replacement IfE 5 a T ande 5 then Ee T We39ll prove these lemmas next time Inversion Lemmas and Canonical Forms Inversion lemmas answer the question if we have an expression of a certain form what do we know about its type 1 If true T then T bool 2 If succ e T then T nat and e nat 3 Canonical form lemmas answer the question if we have a value of a certain type what form does the value have 1 lfv bool then v true or v false 2 lfv nat then v nv for some nv Recall the nv is the grammar for natural numbers Uniqueness of typing In this language of arithmetic expressions an expression is well typed only with respect to just one type Theorem Ife T1 ande T2 then T1 T2 Explicit Casts The basis for this extension is the simply typed lambda calculus with support for subtyping and exceptions Syntax e leasT Type rule I F e 5 I F e as T T Evaluation contexts E lEasT Reduction rule F v T V V 3 T v as T a v v as T a raise cast error Type Tests alternative to using exceptions Syntax iifein TthenXeelsee Type rule I39Fe1 I397XT1he2T2 I39Fe3Tg I h if e1 in T1 then X e2 else e3 T2 Evaluation contexts E if E in T1 then X e2 else e3 Reduction rules F v T1 if v in T1 then X e2 else e3 X gt gt ve2 i7Z v T1 if Vin T1 then X e2 else e3 e3 Coercion Semantics for Subtyping V Suppose we want int lt float gt With the semantics given for subtyping so far this would mean integers would have to be represented in the same way as floats V For efficiency reasons we probably want integers and floats to have different representations V To allow for this we can associate run time coercions with uses of the subsumption rule for example to convert an integer into a float Coercion Semantics for Subtyping For each subtype derivation we39ll associate a function that coerces a value of the left hand type to a value of the right hand type Given a derivation D we write 0 for the coercion function l 800 lt 800 ll AX BOOI X l Int lt Float ll mrTOFOat D1T1 lt51 D2152 ltT2 7 Sl szltT1HT2 iAfSlgtSzixT1l 02 f 01 X w e domR2i R1 R2 R1 lt R2 domR2 Q domR1 Ar R1i riIEdOmlel Coercion Semantics for Subtyping Define a translation from the language with subtyping to the language with explicit coercions The fran Iatinn rule cm I tO quotlquot quotmPllm inserts a coercion FFee DltT FFeDe T Implementing a Type Checker for Subtyping gt Recall the subsumption rule I h e 5 5 lt T I h e T gt This rule can be applied anywhere anytime So how do we know when to use it in the type checker gt The problem with this rule is that it is not syntax directed gt Can we get rid of the rule by using 5 lt T in the other rules Syntax Directed Type System gt The basic idea is to sprinkle uses of lt in all the places that you would use type equality gt For example in function application rh611T11gtT12 l h821T2 T2ltIT11 I h el eg T12 Algorithmic Subtyping gt There39s also a problem with the definition of subtyping we don39t know when or in what order to apply the record width and depth rules domR2 Q domR1 VI 6 domR2 R1I R2I R1 lt2 R2 domR1 domR2 for I E domR1 R1I lt R2I R1 lt2 R2 gt These two rules can be repaced by the following rule domR2 Q domR1 for I E domR2 R1I lt R2I R1 lt2 R2 Transitivity of Subtyping Suppose for the moment we have defined subtyping by the following syntax directed rules 800 lt 800 Int lt Int T lt Top T1 lt2 51 2 lt2 T2 1gt2lt2 T1gt T2 Can we prove that this subtype relation is transitive Transitivity of Subtyping Proposition IfRltandlt TthenRlt T Proof by induction on 5 Case 5 Int Then R Inf and T Int or T Top In either case R lt T Case 5 300 Similar Case 5 Top So T Top and then R lt T Transitivity of Subtyping continued Case 5 1 a 52 Then R R1 a R2 with 51 lt R1 and R2 lt 52 and either a T T1 a T2 with T1 lt 51 and 52 lt T2 or else b T Top The following diagram shows the proof for case a R1 gt R2 IH 1 IH 2 For case because T Top we immediately have R lt T Handling Conditional Expressions gt What type should the following expression have if true then Xtrueyfase else Xfaseztrue gt Should it be X Top X2 300 orjust In some sense any type that is supertype of both branches will work But which is best gt We don39t want to throw information away so the best type is the least upper bound of the types of the two branches gt e if the two branches have type 5 and T we want the type R such that 5 lt R and T lt R and for any other type R R lt R gt Does such a type always exist The SECD Virtual Machine The SECD Virtual Machine is the great grandfather of the Java Virtual Machine JVM S Stack the operand stack contains values E Environment maps variables to values C Control the sequence of instructions to be performed D Dump the procedure call stack The machine has three kinds of instructions for 1 referencing a variable 2 creating a function and 3 applying calling a function I varx l X C l app The SECD Virtual Machine The following function compile translates an lambda calculus expression into a sequence of instructions for the SECD machine compilex var X compilee1 e2 compilee1 compilee2 app compileX e compilee The notation a is a singleelement sequence whose element is a The notation 3 Is adds the element a to the front of the sequence Is The SECD Virtual Machine gt variable lookup S7 E7x C D i gt Ex 5 E7 C7 D gt closure creation S7 E7 C C7 D i gt ltx CZ E S7 E7 C7 D gt function application VltX CZ E 7 E7 appC7 D i gt EX a v7 C2 57 E7 C D gt function return V 57 E7 7 57 E7 C7 i gt V 39 57 E7 C7 The CEK Abstract Machine 6 e7 Egt closures k larg c k l fun v k continuations gt variable lookup ltX7 Egt7 k gt 5le k gt application start evaluating the function expression lt91 92 Egt7 k H lt917 Egt7 3 lt927 B k gt application start evaluating the argument expression ltv7 Egt7 arg e7 E k gt lte7 El7 fun v E k gt function call start evaluating the body ltv7 Egt7 fun ltX e7 E k gt gt lte7 EX a v7 Egtgt7 k Unification case st y in correctness gt What does it mean for a unification algorithm to be correct gt What is the relationship between the input and output gt Input a set of equations gt Output a solution which maps type variables to types it is a substitution gt Does the algorithm terminate Unification correctness gt A substitution 5 is a unifier of an equation T1 i T2 if T1 T2 ie the results of substitution are syntactically equal gt Example 1 l gt bool l gt int unifies a a int i bool a B gt A unifier ofa set ofequations E is a substitution 5 that unifies every equation in E The Output of the Unification Algorithm gt The unification algorithm takes one step at a time simplifying a set of equation E to a new set E We write E a E for one of these steps gt The unification algorithm ends when none of the rules applies to the current equation set ie HE E a E gt We can read offa solution from a set of equations E if it is on solved form 1 All the equations have the form a T 2 Ifa variable occurs on the left of an equation it does not occur anywhere else 041 T1704n Tngt 041 gt gt T17704ngt gt Tn Is the output in solved form Lemma If HE E a E then E is in solved form Is the output a unifier of the equations gt The output 5 is obviously a unifier for the final set of equations call it Ef Ef 041 T17704n Tn 5 041 gt gt T17704ngt gt Tn 5Ef T1 T1Tn Tn gt But is 5 a unifier for the initial set of equations E0 E0 A Ef gt How can we prove that it is Is the output a unifier of the equations Lemma IfE E and 5 unifies E then 5 unifies E Theorem Soundness of the unification algorithm IfE E and 5 unifies E then 5 unifies E If there is a solution will the algorithm find it gt Suppose there is a solution 5 that unifies E When we run the algorithm will it stop with a set Ef that is in solved form gt What is the relationship between Ef and 7 Most general unifier gt A most general unifier of E is a substitution 5 that unifies E and for any other substitution R that unifies E there exists U such that UoS R gt Example let E be 04 i 37y i 04 a 3 Then Oz l gt 37y l gt B a B is a most general unifier of E gt Another solution of E is R a gt gt int gt gt intq gt gt int A int but have 3 gt gt int 0 S a gt gt int gt gt inty gt gt int A int R gt Another solution of E is R a gt gt bool gt gt boolq gt gt bool A bool but have 6 gt gt bool o 5 a gt gt bool gt gt boolgy gt gt bool a bool R If there is a solution will the algorithm find it Lemma lfS is a unifier of E then either E is in solved form or there is an E such that E a E and 5 is a unifier of E Lemma lfS is a unifier ofE and E is in solved form then the solution 5 read from E is more general than 5 there is an R such that R o 5 5 Theorem Completness lfS is a unifier ofE then there exists an Ef such that E Ef such that Ef is in solved form and the solution Sf read from Ef is the most general unifier Does the process terminate gt Most proofs of termination associate a number with all the state used by an algorithm and show that this number shrinks with each step of the algorithm gt This association is call a measure function gt We need to come up with a measure function In on a set of equations and the prove the following lemma Lemma IfE gt E then mE lt mE Measure function mE n17 n2 In gt n1 is the number of variables in E that do not occur only once as the left hand side of some equation gt n2 is the total size of all the equations in E gt n3 is the number of equations of the form 04 04 int int and T a The ordering relation lt that we use to compare tuples is the lexicographical ordering n17 n2 n2 lt n17 n27 nQ n1 lt n1 V n1 n1 A n2 lt nQ n1n1An2n2An3ltn3 Termination Theorem For any E there exists an n and E such that E a E and HE E E Language Support for Object oriented Programming Multiple representations of the same interface Encapsulation D D gt Subtyping gt Inhertance D Open recursion in a method you can call other methods on self this ects Here39s an object that represents a counter We use lexical scoping references and records c etgtltref1in get AUnit ix inc AUnit X succ ix gt c get Unit A Nat inc Unit A Unit cinc unit gt unit Unit cget unit gt 2 Nat O ject Constructors Counter get Unit A Nat inc Unit A Unit newCounter Unit let X ref1 in get A4Unit ix inc AUnit X succ lx gt newCounter Unit A Counter newCounter unit gt get inc Counter Subtyping gt Suppose we also have some objects with the following type ResetCounter getUnitgt Nat incUnitgt Unit resetUnitgt Unit gt The subtype rule for record width allows an object of type ResetCounter in a place that expects a Counter Counter get Unit A Nat inc Unit A Unit inc3 A cCounter cinc unit cinc unit cinc unit newResetCounter AinitUnit let X ref init in get AUnit lX inc AUnit X succ X reset AUnit X init rc inc3 newResetCounter unit gt rc ResetCounter rcget unit gt 4 Nat O jects with Multiple Data Members newResetCounter AiniUnit let r X refini init ini in get AUnit lrlt inc AUnit rlt succ lrlt reset AUnit rlt rinit rc newResetCounter O gt rc ResetCounter Simple Classes gt The definition of newCounter and newResetCounter are rather similar gt Wouldn39t it be nice to reuse the code from newCounter when defining newResetCounter CounterRep X Ref Nat counterClass AhCounterRep get AUnit lrlt inc AUnit rlt succ lrlt newCounter AUnit let r Xref1 in counterClass r Simple Classes ResetCounterRep X Ref Nat init Nat resetCounterClass AhResetCounterRep let super counterClass r in get superget inc superinc reset AUnit rlt rinit newResetCounter AiniNat let r Xref ini init ini in resetCounterClass r M ually Recursive Methods via References SetCounter getUnitgt Nat setNatgt Unit incUnitgt Unit setCounterClass AhCounterRep Aself Source SetCounter get AUnit lrlt set AiNat rlt i inc AUnit lsel set succ lrx dummySetCounter get AUnit 0 set AiNat unit inc AUnit unit newSetCounter L Unit let r X refl in let cAux ref dummySetCounter in cAux setCounterClass r cAux chux sc newSetCounter unit scinc unit scget unit Method Overridi InstrCounterRep XRef Nat aRef Nat InstrCounter getUnitgt Nat setNatgt Unit IncUnitgt Unit accessesUnitgt Nat instrCounterClass ArnstrCounterRep Aself Source InstrCounter let super setCounterClass r self in get superget set AiNat La succ ire superset i inc superinc accesses AUnit lra dummylnstrCounter get AUnit 0 set AiNat unit inc AUnit unit accesses AUnit O newlnstrCounter A Unit let r X ref 1 a refO in let cAux ref dummylnstrCounter in cAux instrCounterClass r cAux chux ic newlnstrCounter unit icinc unit icinc unit icaccesses unit Why not Objects via Self Application gt Why don39t we do the normal thing of passing the object as the first parameter of each method gt We would need recursive types for this Counter get Counter A Nat inc Counter A Unit gt We39ll study recursive types in a few weeks Extensions the the Simply Typed Lambda Calculus VVVVVV unit and sequencing let binding pairs records variants recursive functions Unit and Sequencing iunitiee T iUnt FD Typing rule for unit I F unit Unit Definition of sequencing 91 82 by translation el 82 E AX Unit 6 2 91 where X is a fresh variable not in FV82 Let Binding local variables e lletxe1ine2 For evaluation purposes we can use let X e1 in e2 E Xe2 e1 However notice that the parameter X wasn39t given a type We can give it a type but we don39t know that type until we39ve type checked e1 So we can39tjust expand a let into an application and before we do type checking I39he1T1 I397XT1he2T2 I39hletxe1ine2T2 Pairs e eefstesnde T TXT Reduction rules fst v17 V2 v1 5nd v17 v2 gt v2 Evaluation contexts E EevE Typing rules I39Felle I FSQITQ I F81782IT1gtlt T2 I39FeT1XT2 I39FeT1XT2 I39FfsteT1 FandeT2 e il1ellneniel T il1T1lnTn Reduction rules I1v1lnvnIgtv lg n Evaluation contexts E il1 V17I EI1 e1In en Typing rules FFeyTl I39FenTn I39FI1ellnenll T17In Tn I39FeI1T1InTn 1 i n I39FeIT TltIegtcaseeofI1X191Inxnen ltI12 T1Jni Tngt e T Reduction rules case TltI vgt of 1 X1 91 In Xn en xi gt gt ve lg n Typing rules I39FeT 1 i n TltI1T1InTngt FFTltIegtT I39FeltI1T1In Tn Vi 1n I397X TFe T I39FcaseeofUlX191InxnenT Recursive Functions e ifixeiletrecx Teine Reduction rules fix Af T e a f gt gt fiXf T ee Evaluation contexts E ifixE Typing rules I F e T a T I F fix 9 T Definition of letrec by translation Ietrec X T el in 82 E let X fiXX Tel in 82 Example the sum function letrec sum nat A nat let sum fix sum nat A nat n nat A n nat if iszero n then if iszero n then else else n sum pred n n sum pred in in sum 2 sum 2 Example running the sum function B E A n nat if iszero n then 0 else n sum pred n S E fix A sum nat A nat B sum 2 gt gt S 2 H sum gt gt S B 2 A n nat if iszero n then 0 else n S pred n 2 H if iszero 2 then 0 else 2 S pred 2 gt gt 2 S pred 2 gt gt 2 sum gt gt S B pred 2 Example typing the sum function B E n nat if iszero n then 0 else n sumpred n I397 sum nat a nat F B nat a nat I F sum nat a nat B nat a nat a nat a nat I F fix sum nat a nat B nat a nat Featherweight Java Syntax P a e program CL class C extends CC 7 Km class definition K CC 7super7 this 7 constructor M 39 C mC Yreturn e method e expressions X variables ef field access em method invocation new Ce object creation Ce cast Notes C is for class names m is for method names and f is for field names This syntax is literally a subset of Java A Featherweight Java program can be run by a standard Java interpreter Subtyping Clt C C lt D D lt E C lt E CTC class C extends D Clt D Auxiliary Functions fieldsObject fieldsC let CTC class C extends D f E K W return fieldsD f7 mbodymC let CTC class C extends D f E K M if B m xreturn 5 E M then return 2 e se return mbodym D More Auxiliary Functions mtypem C let CTC class C extends D f E K M if B m Yreturn 5 E W then return E A B else return mtypem D overridemDf A CD if mtypemD 5 A Do then return 6 5 and C0 D0 e se return true Evaluation Values v new CV Evaluation contexts E EfEm E new CV7 E Reduction rules mbodym7 C Y e new CVmU Y gt gt U this gt gt new CVe EInvk C lt D DneW CV nevu CV ECast Type Rules X3C r I39FeC fieldsCf7 MW WWW I39FeC mtypemC5HC Elt5 TInvk 7 I F eme C TM fieldsC 5 FF E flt5 w W I39Fnew CE C I39FeD CltDorDltC mica I F Ce C Type Rules for Methods and Classes YCthisCFeCe CeltC CTC class C extends D overridem7 RCA C C mCYreturn e OK in C COK K CO EC7super this 7 fieldsD OE W OK in C class C extends DC 7 KW OK Lemma Preservation fl h e C ande gt gte then I39h e C forsome D Where C lt C Definition A bad cast is an expression of the form CneW DV where mac Lemma Progress Suppose e is closed well typed and in normal form Then either e is a value or there is an evaluation context E such that e Eb Where b is a bad cast Subtyping motivation gt Recall that type systems are conservative predicates that filter out bad programs but also some good programs gt Much of the research on more advanced type systems tries to allow more good programs while still filtering out the bad ones gt Example of a good program that is filtered out by the type systems we39ve seen so far A r XNat rlt XOy1 Subtyping gt The subtype relation is a binary relation on types usually written T1 lt T2 that is meant to capture when values of type T1 can be safely used in contexts that expect values of type T2 gt It is often helpful to think of types as describing sets of values and subtyping as the subset relation between these sets gt Different languages provide different definitions for which pairs of types are in the subtype relation gt The type system is extended with a subsumption rule that allows an expression of type T1 to be treated as if it has type T2 provided T1 lt T2 I39heT1 T1ltIT2 I39heT2 Defining the Subtype Relation b V b For the moment the setting is the simply typed lambda calculus with naturals Booleans and records And of course a value of type 800 can be used as a 800 and similarly for Nat 800 lt 800 Nat lt Nat We want to allow records with more fields to be used in contexts that expect fewer fields This is called width subtyping Common fields must have the same type In the following we view a record type as a partial function from labels to types domR2 Q domR1 VI 6 domR2 R1I R2I R1 lt2 R2 For example X Naty Nat lt X Nat V Subtyping for Records gt We also want to allow subtyping between records whose fields may differ according to the subtype relation This is called depth subtyping domR1 domR2 for I E domR1 R1I lt R2I R1 lt2 R2 For example X a Nat7 b Naty Nat lt X a Naty Nat Subtyping for Functions 5152 7 T1 T2 T1 lt2 51 2 lt2 T2 51H2ltI T1HT2 Functions are contravariant in their parameter types and covariant in the return types Properties of the Subtype Relation Proposition Basic Properties 1 Subtyping is reflexive for any T T lt T 2 Subtyping is transitive for any R7 5 T ifR lt 5 and 5 lt T then R lt T Proposition Inversion 1 1 5 lt2 T1 H T2 then S 51 H 52 T1 lt2 51 and 2 lt2 T2 for some 1 and 2 2 1 5 lt R and R is a record type then 5 is a record type and domR Q dom and for I E dom I lt RI Properties of the Subtype Relation Lemma Lambda Typing Ifl39be1eT1H T2 then T1lt1 andl39x1be T2 Let p range over record values and R over record types A record value is a partial function from labels to values Lemma Record Typing Ifl39 F p R then domR Q domp and for I E domR I39 F pl RI Properties of the Subtype Relation Lemma Substitution Ifl39xFe TandI39Fe thenI39FXHe e T Proof By induction on I39X 5 F e T i i e I T1 T1 lt2 T2 From the induction hypothesis we have I F x gt gt e e T1 Then by the subsumption rule we have I F x gt gt e e T2 Case 1 Proof of Type Safety Lemma Subject Reduction fl Fe Tandeae thenI39Fe T Proof By cases on e a 9 Case X 51 sh v a x gt gt veb Because 9 is well typed we have T T1 a T2 39 F X 51 sh T1 a T2 and I F v T1 From the lambda typing lemma we have T1 lt 51 and I39X 51 F eb T2 Because T1 lt 51 we have I F v 51 Then by the substitution lemma I F X gt gt veb T2 Subject Reduction continued Case pt A IOU Because 9 which is pl is well typed we have I F p R for some record type R and I E domR and T RU Then by the record typing lemma for everyj E domR we have I F pj RU Therefore I F pl RU for I E domp pl is a value I E domp Recursive Types gt Suppose you want to write an interpreter for the simply typed lambda calculus gt How would you represent expressions using the tools we have studied so far gt We could use a variant type Expr ltvar string lam string gtlt Expr app Expr gtlt Exprgt but note that the type we are defining Expr appears within the definition of EXpr It is circular Recursive Types Syntax T types A type variables uA T recursive types Example Expr M A ltvar string lam string X A app A X Agt Equi recursive and iso recursive types gt A recursive type can be unfolded by replacing it with its body substituting the bound variable for the type itself MA TgtAHIMA TT For example Expr u A ltvar stringlam string X A app A X Agt Expr gt ltvar stringam string gtlt Expr app Expr gtlt Exprgt gt There are two main approaches to integrating recursive types into the type system of a language gt Equi recursive types the type an its unfolding are considered equal gt lso recursive types there are unfold and fold operators that convert back and forth between the recursive type and its unfolding ISO recursive Types Syntax e ifoldTe i unfoldTe v ifoldTv Evaluation contexts E ifoldTE Reduction rules unfoldfoldTv v Typing rules Fld UuX T I39FeXHUT I F foldUe U Un d UuXT I39FeU I F unfoldUe X i gt UT Equi recursive Types gt The type system for equi recursive types is more complicated gt Also without to much extra complication we39ll consider subtyping over equi recursive types gt We39ll need to learn some theory and techniques to handle equi recursive types gt In particular we39ll need to learn about coinduction which is like induction but works for recursive structures Induction and Coinduction gt Suppose we have the set 3 b c The power set of 3 b c written 733 b c is the set of all subsets of 3 b c 7337 b7 6 07 BL bk CL 37 b7 37 CL b7 CL 37 b7 6 gt We39ll be concerned with functions that map sets to sets ie whose domain and codomain are power sets gt F is monotone ifX Q Y implies FX Q FY Example FW FCD Fa7b FC Fa FCD Fa7c Fb7c Fb FCD Fb7c Fa7b7c FCD Fb7c Fa7b7c Fa7b7c gt F can be compactly represented by inference rules 6 e X b e X c e X c FX beFX 376 FX Induction and Coinduction gt A set X is closed with respect to function F it is F closed if FX Q X gt A set X is F consistent if X Q FX gt A set X is the fixed point of F is FX X gt Find some sets in 7337 b7 6 that are F closed F consistent and are fixed points of F Theorem Knaster Tarski 1 The intersection of all F closed sets is the least fixed point of 2 The union of all F consistent sets is the greatest fixed point of We refer to F as the generating function for the least and greatest fixed points Induction and Coinduction Corollary 1 Principle of induction le is F closed then the least fixed point ofF is a subset ofX 2 Principle of coinduction le is F consistent then X is a subset of the greatest fixed point of F What Principle of induction If X is F closed then the least fixed point of F is a subset of X To prove PX for all X E N show 1 PO 2 Pn gt Pn l 1 Correspondence X is P F is represented by the inference rules nEX 0 FX n1eFX and the least fixed point of F is N Saying that N Q P is the same as saying that X E N implies X E P Recall that F closed means FP Q P So the principle of induction says that you need to show that applying F to stuff in P results in stuff that is also in P Recall that an inductively defined set is the least fixed point of some inference rules A coinductively defined set is the greatest fixed point of some rules Principle of coinduction If X is F consistent then X is a subset of the greatest fixed point of F VF In other words if you want to show that some element X is in a coinductively defined set VF then find some set X such that X E X and X is F consistent ie X Q FX or everything in the input shows up in the output Subtyping gt Subtyping rules defining the generating function S T17T3 X T2T4 X T7TOPESX T1gtlt T27T3gtlt T4 X T3771 EX T27T4 EX T1 gt T27 T3 gt T4 6 5X TL7 A H uA T2T2 E X A H uA T1T1T2 E X T17MAT2 MA T17 T2 6 gt The subtyping relation lt is the greatest fixed point of S gt For some given T1 and T2 how do we know if T1 lt T2 gt The coinduction principle says find some relation R on types such that T17 T2 6 R and R is S consistent ie R Q R Subtyping Via Coinduction gt The main idea behind finding this set R is that we start off with R0 71775 and then run 5 backwards so that R1 R U 5 1R until 5 1Rj Q for somej We then let R and we know that R is S consistent by the following reasoning S 1R g R 5571R Q 5R by monotonicity R Q 5R by definition of inverse gt Suppose T1 int a int and T2 int a Top R0 int a int7 int a Top R1 int a int7 int a Top7 int7 int7 int7 Top R2 R1 Subtyping Via Coinduction Suppose T1 luX int HX x int and T2 uY int a Y x Top R0 IuX int a X x intuY int a Y x Top R1 MX int a X x intHuY int a Y x Top7 int a IaX x intuY int a Y x Top MX int a X x intHuY int a Y x Top7 int a IaX x intuY int a Y x Top7 int a IaX x int7int a MY x Top R3 MX int a X x intHuY int a Y x Top7 int a IaX x intuY int a Y x Top7 int a IaX x int7int a MY x Top7 int nt7 int7 Top R4 R3 R2 D namic Semantics The dynamic semantics of a language defines what happens when you run a program There are many approaches to defining the dynamic semantics of a language gt Small step operational semantics gt Big step operational semantics gt Abstract machines gt Translation to another language gt Denotational semantics translation to a mathematical system gt AXiomatic semantics In this class we will primarily be concerned with the small step operational semantics which is the most widely used approach Recall the language of Arithmetic Expressions e true false if e then e else e O succ e pred e iszero e v true false nv nv 0 succnv Small step operational semantics In a small step semantics we take textual rewriting view of running a program That is we evaluate a program by changing the program text a little bit at a time Example if iszero pred succ 0 then 0 else succ O gt gt if iszero E then 0 else succ 0 if then 0 else succ 0 if then 0 else succ 0 if true then 0 else succ O gt gt E Definition of small step semantics We define a relation between two expressions that says when one expression evaluates to the other expression We39ll call this the ReducesTo relation and define the relation inductively with the following rules The first bunch of rules do some real computation 1 2 I precl 00 6 ReducesTo I precl succ nv7 W E ReducesTo 3 iszero succ nv7 false 6 ReducesTo 4 iszero O7 true 6 ReducesTo 5 I if true then e2 else e37 e2 6 ReducesTo E I if false then e2 else e3e3 E ReducesTo Before defining the rest of the rules for ReducesTo we introduce the following notation e gt e E e7 e E ReducesTo Congruence Rules The second bunch of rules called congruence rules define the evaluation order by saying where you can reach inside a large expression to evaluate a subexpression Bi gt8 ell gt8 7 8 succ e gt succ e pred e l gt pred e e i gt e iszero e l gt iszero e e i gt 1r 1 A if e1 then e2 else 93 l gt if ei then e2 else e3 Inversion Lemmas Suppose you know that for some e and e e l gt e What further information can you glean from this based on the rules for ReducesTo We can do case analysis on the rules For example suppose if true then e2 else 93 gt e4 Then you know that e2 e4 because the only rule that could have appeared as the final step in the derivation is rule Why not rule 10 Because then there would need to be a rule of the form true gt 7 but there is no such rule A Proof by Rule Induction on ReducesTo Theorem Ife l gt e and e l gt e then e e Proof by rule induction on e l gt e Case 1 So e pred 07e O and by assumption we have pred O l gt e There are two rules that could have applied 1 and but 8 can39t apply because there are no rules of the form 0 l gt 7 Thus e O and we conclude that e e A Proof by Rule Induction on ReducesTo continued ell gt81 Case 7 succ e1 l gt succ e1 So e succ e1 and e succ e1 From the induction hypothesis we have a VX e1 l gt X implies X e1 Also by assumption we have succ e1 l gt e The only rule that could have applied is so we know there was some ei such that e1 gt ei Then using a we have ei e1 Thus e succ e1 succ ei e The other cases are left as an exercise Definition An expression e is in normal form if le 9 i gt 9 Definition Multi step reduction written i is the relation inductively defined by the following rules 81 i gt 82 82 i gt 6 3 1 2 u 8 u 81 sea This is an alternate but equivalent definition than the one in the textbook The Untyped Lambda Calculus Syntax X Variables e X l Xe l e e Expressions Xe Values gt An expression of the form X 9 create an anonymous function The X is the one parameter of the function and e is the function body gt An expression of the form el 82 is a function call The expression el should evaluate to a function which is then called using the result of 82 as the argument Call by value Small step Semantics 1 Axel V2 i gt X i gt V2e1 6 1 i gt e1 82 i gt e 2 2 I 81 82 i gt e1 82 V1 82 i gt V1 e Note where we use v instead of e to restrict the order of evaluation iv equivalence The variable name associated with a doesn39t really matter The meaning of the program remains unchanged if you change the variable name and consistently replace the occurrences of that variable in the ye zy l gt ze provided 2 is not in e Substitution and Free Variables We write X l gt e e to say that e is substituted for the free occurrences of X in e For example in the following we substitute the expression y z for the variable X in the expression AX X X X H y ZlX X X X X y 2 A free occurrence of a variable X within an expression e is an occurrence of X in e that does not have a surrounding in e that binds X The the following examples free occurrences are enclosed in a box Free Variables The function FV computes the set of free variables in a given expression FVX X FV81 6 2 FV81 U FV82 FVx 9 FVe 7 X Capture avoiding Substitution gt We need to be careful when defining substitution X H e e to make sure that free variables in e don39t get captured by s in e gt The following is an example of what happens if you don39t define substitution correctly Ay AX Ay X y H Ay Ay y gt Here39s a correct definition of substitution XHe y ifXy then e elsey X H e y e ZX H e y H ze where z is fresh X H e e1 e2 X H e e1 X H e e2 Evaluation Contexts Congruence rules are a verbose way to specify evaluation order A more succinct way is to use evaluation contexts Recall the small step textual rewriting view of semantics if iszero pred succ 0 then 0 else succ O i gt if iszero iii then 0 else succ 0 An evaluation context is everything not inside an evaluation box We can use a grammar to define where the boxes are allowed and what the surrounding evaluation context looks like E The evaluation box forms a hole in the context Ee vE Filling an Evaluation Context fille e fillE e 7 e fillEe e fillv E7 e v llE7 9 Notation Ee E llE7 9 Example Ay y AX X Ay y AX X Small step Semantics with Evaluation Contexts We separate out the computational reduction rules into the relation L For the lambda calculus there isjust one rule 6 Xel v2 x l gt i2e1 We then define top level reduction using evaluation contexts e a e Ee gt gt Ee Type Inference V V V V Instead of writing type annotations can we use an algorithm to infer what the type annotations should be That depends on the type system For simple type systems the answer is yes and sophisticated type systems the answer is often no it39s undecidable We39ll first look at type inference for the simply typed lambda calculus Then we39ll look at type inference in ML ie Hindley Milner inference The Simply Typed Lambda Calculus xzrel39 39X71he72 l hXIT l hXeIT1gtT2 rh812T1HT3 I39heQM39l l h 81 82 2 T3 The main constraint on the inferred types is that the type of 82 needs to be equal to the parameter type of el An alternative presentation from Milner attaches types to every subexpression and expresses all the constraints as equalities XTEF I397Xphea 70Ha I h X7 I h AX190 I39hep I39hef p039gt739 I39hepe 7 Type Inference gt First initialize all the attached types with unique unknowns that is type variables gt For example Af f 1 X X becomes Afay fag 1043044045 May Xa7asozg gt We can change the type system to generate a set of equalities over these variables Xaer l 7Xahe gtc l hX gtOz I39hXae 739yaa UC l l eagtC1 l l ebC2 Fheaeb7a gtyUC1UC2 For this program Afay fth 1043044045 AXDt 39 X047048049 we generate the following equations 043 int 041 042 042 043 H 044 045 a1 a 044 046 047 048 046 H 047 045048H049 Solving equations by unification gt We can solve the equations by a process of normalization that simplifies the set of equations gt The two main rules are gt Reduction replace an equation of the form 7391 A 7392 7393 A 7394 with two equations 7391 7393 an 7392 7394 gt Variable elimination suppose there is a equation of the form a 739 Ifa E ftv739 then report an error Otherwise substitute 739 for a in all the other equations gt The auxiliary rules are gt Replace 739 a with a 739 gt Remove equations of the form a 1 int int bool bool etc gt If there is an equation 739 7quot where the head type constructor differs on each side then stop and report failure eg int int A int 041 0427042 Ho 4ya5a1quota47a6a77 048 046 047045 048HOZ9 variable elimination gt 043 int 042int044045 H 0447 046 0477 043 046 047045 048049 variable elimination gt 043 int041 042 045 042 044046 047 043 046 047045 048049 variable elimination gt 048 046 047045 048049 variable elimination gt 043 int041 int 044042 int 044045 int 044 044 043 int041 A 0447046 0477 046047043O46gt047045048gt049 Example C tinued 043 int 041 int gt 044042 int gt 044 045 nt gt 044 gt 044 variable elimination gt 043 39nt041 int a 044042 int a 044045 int a 044 a 044 043gt047intgt044gt044048gt049 variable elimination gt 043 int 041 int a 044042 int a 044045 int a 044 a 044 046 047 int gt 044 gt 044 gt 049 variable elimination gt 043 int 041 int gt 044042 int gt 044045 int gt 044 gt 044 046 047043 047 gt 047 int gt 044 gt 044 047 gt 047 gt 049 reduction gt 043 int 041 int a 044042 int a 044045 int a 044 a 044 046 047 043 047 gt 047 int gt 044 047 gt 047 044 049 Example continued a3 inta1 int gt 14042 int gt 14045 nt gt a4 gt a4 a5a7a8a7gta7 Imam anaan a4ag reduction a3inta1intgta4a2 intaa4a5 intgtamgta4 70440477044049 a3inta1intgta4ag intgta4 15 a5 innag int a Inta7 int variable elimination a3 inta1 int a innag int a inta5 as innas int gt inta7 int 14 flip a3 inta1 int gt intag int gt inta5 int a int a int 15 Inta8 Int gt Inta7 Int 14 Innag Int Example the solution So for this program Afay fag 1043a4045 Xae39 Xa7asag the solution is 11 int a int 12 int a int 13 int 14 int 15 int a int a int 15 int as int a Int 17 int 19 int So we have Afintaint fintaint lintinfintaintaint Xint Xintint4gtintint Most general unifier b V V V V V Sometimes the solution is underconstrained and there are many solutions for example AXa1Xa2a3 gives rise to the following equations 041 042043 041 gt 042 Here39s some solutions 1 a1 inta2 inta3 int A int 2 a1 booa2 booa3 bool A bool 3 a1 a27a3 12 A 12 Which solution is the best The most general unifier is the solution that can be instantiated to match any other solution Solution 3 is the most general unifier lnstantiate a2 l gt int to get solution land 12 l gt bool to get solution 2 The unification algorithm always returns the most general unifier Hindley Milner ML like Inference gt The family of ML languages provide let polymorphism which is a restricted form of the parametric polymorphism in System gt Not only does the inference algorithm figure out the types but it also figures out what should be generic and where instantiation should happen gt Example let f A X X in f true fl is equivalent to the following in System F letfaxaxin fboo true fint 1 The Hindley Milner Type System Universal quantification V is only allowed at the top of a type T booIlTHT 5 T lVE T The right hand side of a let is inferred to be polymorphic ThelT1 FXVET1heQT2 EOFTV Fhletxelineg T2 and instantiation happen implicitly when a variable is used XVET 39 l l XIEl gtTT Generalization generalizeU39 739 et a ftv739 in let 3 ftv39 in let 7 E 7 B in V7 739 Algorithm J infer39 e E case 5 of X gt let Val T 39X and B be fresh type variables in 57 5 H B T i 51 52 let Rm infer39 51 E in let 50 inferR39 52 R in let U unifyp a A B U S where B is fresh in u Um i Axi 5 let Rm infer39x B e E where B is fresh in R Rm a p i letx 51 in 92 let Rm infer39 51 E in let 739 generalizeR39 p in let 50 inferR39X 739 52 R in 57a Algorithm W infer39 e case 5 of X gt let Val T 39X and B be fresh type variables in 07 5 H B T i 51 52 let Rm infer39 51 in let 50 inferR39 52 in let U unifyp 039 A B where B is fresh in U o S 0 R7 i Axi 5 let Rm infer39x B e where B is fresh in R7 R16 A P i letx 51 in 92 let Rm infer39 51 in let 739 generalizeR39 p in let 50 inferR39X 739 e in S 0 R70 Types and Programming Languages Isabelle Formalization of Chapter 3 Jeremy Siek February 27 2008 Contents 1 Boolean Expression 2 Arithmetic Expressions theory Booleans imp orts M am begin 1 Boolean Expression datatype trm Tru Fls IF trm trm trm inductive evalBooleans trm A trm A bool in x A 51 W ere E IfTrueintr0lz IF Tru t2 755 A 752 E IfFalseintr0lz IF Fls t2 755 A 755 E I intml 751 A 751 gt IF 5 t2 753 A IF t1 t2 t3 lemma IF Tru Tru IF Fls Fls Fls A Tm by auto Inversion rules are generated by Isabelle inductivecases inversion Tm Try A 75 TM A t gt P inductivecases inversionFla Fls A t Fls A t gt P inductivecases inversion2f Tm IF Tm t2 755 A 75 IF Tru t2 755 A 75 t2 t gt P t1 C t IFtZ tQ t3 Tru A 751 gt P gt P inductivecases inversionifFls IF Fls t2 755 A 75 IF Fls t2 755 A 75 t3 t gt P t14 t IF t1 t2 t3 Fls A tl j gt P gt P inductivecases inversionif IF t1 t2 t3 A 75 IF t1 t2 755 A t 751 Tru t2 t J gt P 751 Fls t3 t gt P t14 t Fm752753 t A t1 gt P gt P theorem thm354determinacy tzztrm A tgt 757 t A t gt t t proof induct rule evalBooleansiinduct x t2 7537f assume IF Tru t2 755 A t thus t2 t by blast elim inversion2f Tru inversizm Tm next x t2 t3 t assume F Fls t2 t3 A t thus t3 t by blast elim inversionifFls inversionFls next x t122trm and t1 t2 t t assume t1t12 t1 A tl and H2 t 2 t1 At gt t1 t and iftp IF t1 t2 t3 A t from z39ftp show F t t2 t3 t proof rule inversionif assume t1 Tm with tltl have False using inversion Tm by simp thus chesz39s by simp next assume t1 Fls with tltl have False using inversionFls by simp thus chesz39s by simp next x t1 assume tpp t F t1 t2 t3 and t1t1p2 t1 A t1 from tltlp H have tl t by simp with tpp show F t t2 t3 t by simp qed qed constdefs normalfm39m 22 tm bool normalfm39mt E i 3 t 22trm2 t A t isvalue 22 tm d bool isvalue t E t Tru V t Fls theorem thm3572 isvalue t gt normalform t proof induct t show normalform Tm using normalform def by blast elim inversizm Tru ne t show normalform Fls using normalfurmdef by blast elim inversionFls next x t1 t2 t3 assume z39svalue F t1 t2 t3 hence False using z39svaluedef by simp thus normalform F t1 t2 t3 by simp qed lemma novalnotnormal isvalue t gt n normalform t proof induct t assume z39svalue Tm thus normalform Tm using z39svaluedef by blast next assume z39svalue Fls thus normalform Fls using z39svaluedef by blast next x t1 t2 t3 assume H12 z39svalue t1 gt normalfurm t1 and H22 isvalue t gt n normalform t2 and H32 isvalue t3 gt n normalform t3 show i normalform F t1 t2 t3 proof cases t1 assume t1 Tm thus normalfurm F t1 t2 t3 using normalform def by blast next assume t1 Fls thus normalfarm IF t1 t2 t3 using normalfarm def by b ast next x trml trm trmf assume t1 IF trml trm trmf hence z39svalue t1 using isvaluedef by simp with IHJ have X 3 t l t A t using normalfurmdef by simp from X obtain t where t a t by blast hence IF t1 t2 t3 A IF t t2 t3 by blast thus normalfurm IF t1 t2 t3 using normalfarmdef by blast qed qed theorem thm358 normalfarm t gt isvalue t using navalnatnarmal by blast 7 The following works7 but is different from Peirce s cleft inductive evalsB trm trm baal in x 51 W ere ebrefl t t and ebstep t t t 8 t gt t t inductivecases evalsB inv t 8 t t 9 t t t gt P t ai t t a t a 8 t gt P gt P lemma evals narmalz39d t 8 t normalfm39m t gt t t proof induct rule evals Blinduct x t show t t by simp next x tzztrm and t t assume t t and normalfarm t hence False using normalfurm def by simp thus t t by simp qed theorem thm3511 t 8 u gt normalfarm u A V ul t 8 u normalfarm 118 14 u proof induct rule evals Blinduct x t show normalfarm t Val t u normalfarm u t 14 using evals narmalid by simp next x tzztrm and t t u assume ttp t a t and tptpp t t and IH normalfm39m t gt Witi t u normalfarm 118 t 14 show normalfarm t gt Vai t 9 u normalfarm u t u proof clarify x u assume nftpp normalfm39m t and tap t u and nfup normalfarm u from IH nftpp have IHZ Vul t x u normalfarm 118 t u by simp from tap show t u proof rule evals B inv assume a t With nfup have normalfarm t by simp With ttp have False by simp add normalfarmdef thus t u by simp next x w assume tw t A w and wap w A u from ttp tw have t w by rule thm 354determz39nacy with wup have t A u by simp with H2 nfup show t u by simp qed qed qed theorem progress isvalue t V 3 t 2 t A t proof induct t have z39svalue Tm using z39svaluedef by simp thus isvalue Tru V Ht2 Try A t by simp next have z39svalue Fls using z39svalue def by simp thus isvalue Fls V Ht2 Fls A t by simp next x t1 t2 t3 assume H12 z39svalue t1 V Ht2 t A t and H22 isvalue t2 V Ht2 t2 A t and H32 isvalue t3 V Ht2 t3 A t from H1 have 3t 2 F t1 t2 t3 A t proof assume z39svalue t1 hence t1 Tm V t1 Fls using z39svalue def by simp thus chesz39s proof assume t1 Tm hence F t1 t2 t3 A t2 by blast thus chesz39s by blast next assume t1 Fls hence F t1 t2 t3 A t3 by blast thus chesz39s by blast qed next assume X2 3 t 2 t1 A t from X obtain tl where t1t1p2 t1 A t1 by blast hence F t1 t2 t3 A Ft t2 t3 by blast thus 37 F t1 t2 t3 A tby blast qed thus isvalue F t1 t2 t3 V Ht2 F t1 t2 t3 A t39 by simp qed end theory Naturals imports Main begin 2 Arithmetic Expressions datatype trm Tru F ls IF trm trm trm Pred trm IsZem trm inductive numval trm bool Where NumZerointr0iz Humval Zero NumSuccintroiz numvalt gt Humval Sum 75 inductivecases numzfelimz num val IF t1 t2 t3 inductivecases numsuccelimz num val Succ t inductivecases numpredelimz num val Fred t inductivecases numiszemelimz num val IsZem t constdefs val trm bool val t E t Tru V t Fls V Humval t declare valde simp inductive evalNatumls trm trm gt bool in x lt gt 5 Where E IfTrueintmiz IF Tru t2 t3 lt gt 752 E fFalseintroiz F Fls t2 t3 lt gt 755 E I intmi t gt 751 gt F t1 t2 t3 lt gt F 751 t2 t3 E Succintr0iz t lt gt t gt Succt lt gt Sues t E PredZerointr0iz Pred Zero lt gt Zero E PredSuccintmiz num valt gt Pred Sum 75 lt gt t E Predintmiz t lt gt t gt Predt lt gt Pred t E IsZeroZerointr0Iz IsZero Zero lt gt Tm E IsZeroSuccintmiz Humval t gt IsZem Sum 75 lt gt Fls E IsZer0introiz t lt gt t gt IsZem t lt gt IsZem t inductivecases inversizm Truelimz Tru lt gt t inductivecases inversionSuesTruelimz Succ Tm lt gt t inductive multi evals trm trm bool in x lt gt 51 Where me Te introiz t lt gt t and me stepintmiz II t lt gt t t gt t gt t lt gt t 7 Counter example theorem 3 ti Succ Tm lt gt t by blast inductive bigstep trm trm gt bool in x U 5 Where B Value ntmi val v gt 1 it v B IfTrueintroiz 751 U TM 752 U 112 gt F t1 t2 755 U 112 B IfFalseintmiz 751 U Fls 755 U v3 gt F t1 t2 755 U 1 B Succintr0z t U m Humval m gt Sum 75 U Sues m B PredZer0introiz t it Zero gt Predt U Zero B PredSuccintr0iz t it Sues m Humval m gt Pred t U m B IsZemZer0intmiz t it Zero gt IsZem t it Tru B lsZemSucciutral t U Sues m uumval m l gt IsZero t U Fls inductivecases z39fz39nv F t1 t2 t3 U u inductivecases suesmu Succ t U u inductivecases predz39nv Predt U u inductivecases iszemz39uv IsZem t U u inductivecases zeromu Zero U u inductivecases tru z39nv Tru U u inductivecases fls z39nv Fls U u lemma valifiuv val IF e1 e2 e3 gt P by auto lemma valiuvrulef0rmat V t val v a u U t A t 1 apply induct 1 apply clarify apply erule truz39nv apply simp apply clarify apply erule fls inv apply simp apply clarify apply erule valifinv apply clarify apply erule zeromu apply simp apply clarify apply erule succz39nv apply blast apply simp apply erule uumsucc apply blast apply clarify apply simp apply blast apply clarify apply simp apply blast done lemma smallbig bigrulef0rmatz t lt gt t gt V u t U u a t U 1 apply induct rule evalNaturalsiz39uduct apply clarify using valdef apply blast apply clarify using valdef apply blast apply clarify apply erule ifz39nv apply simp apply erule numz39f apply rule B IfTrue apply blast apply simp apply rule B IfFalse apply blast apply simp apply clarify apply erule succz39nv apply simp apply erule uumsucc apply erule tac xt in allE apply erule impE apply rule 13 Value apply simp apply rule B Succ apply simp apply simp apply eruletac xnv in allE apply simp apply rule BSucc apply simp apply simp apply 39rule allI apply rule impl apply erule zeromu apply simp apply rule B PredZem apply rule 13 Value apply simp apply clarify apply rule B PredSucc apply rule B Succ apply simp using val2m apply simp apply blast using valmu apply simp apply blast apply 39rule allI apply rule impl apply erule pred inv apply simp apply erule numpred apply simp apply eruletac xZer0 in allE apply simp apply rule B PredZem apply simp apply rule B PredSucc apply simp apply simp apply rule allI apply rule impl apply erule truz39nv apply simp apply rule BIsZemZero apply rule 13 Value apply simp apply blast apply 39rule allI apply rule impl apply erule fls z39nv apply simp apply rule BIsZemSucc apply rule 13 Value apply simp apply blast apply simp apply rule allI apply rule impl apply erule iszemz39uv apply simp apply erule uumiszem apply simp apply blast apply blast clone lemma smallimplies bigrulef0rmatz t lt gt v gt val v H t ll 1 proof induct rule multi evalslz39nduct x t show val t A t ll t by blast next x tzztrm and t t assume e t lt gt t and e2 t lt gt t and H2 val t gt t ll t from e show val t t it t proof rule evalNaturalslcases x t2 t3 assume t t F Tm t2 t3 and tp t t2 show val t a t ll t proof assume vtpp val t with H tp have e3 t2 it t by blast have tru Tm ll Tm apply rule 3 Value by simp from t tru e3 show t ll t apply simp apply rule B fTrue by blast qed next x 5 t3 assume t t F Fls t2 t3 and tp t t3 show val t a t ll t proof assume vtpp val t with H tp have e3 t3 ll t by blast have fls Fls ll Fls apply rule 3 Value by simp from tfls e3 show t it t apply simp apply rule B fFalse by blast qed next x t 751 t2 t3 assume t t Ft t2 t3 and tp t F tl t2 t3 and t1 t1 lt gt 751 show val t a t it t proof assume vtpp val t with H have tptpp t ll t by blast with tp have e3 F t1 t2 t3 ll t by simp from t11 t tp have ttp t lt gt t by blast from ttp tptpp show t it t by rule smallbigbig qed next x tt t a assume t t Succ tt and tp t Succ t a and ttp tt lt gt t a show val t A t ll t proof assume vtpp val t with H have tptpp t ll t by blast with tp have Succ t a ll t by simp from ttp t tp have ttp t lt gt t by blast from ttp tptpp show t U t by rule smallbigbig qed next assume t t Fred Zero and tp t Zero show val t a t U t proof assume vtpp val t with H have tptpp t U t by blast with tp have Zero U t by simp hence tpp t Zero using zeromu by blast with t show t U t apply simp apply rule BPredZera apply rule 3 Value apply simp apply blast clone qed next x tt assume t t Pred Succ tt and tp t tt and nut uumval tt show val t a t U t proof assume vtpp val t with H have tptpp t U t by blast with tp have tttpp tt U t by simp with nut have t tt using valmu by simp with t tp vtpp tttpp nut show t U t apply simp apply rule B PredSucc apply rule BSucc by auto qed next x tt t a assume t t Pred tt and tp t Pred t a and ttp tt gt t a show val t a t U t proof assume vtpp val t with H have tptpp t U t by blast with tp have Pred t a U t by simp from ttp t tp have ttp t lt gt t by blast from ttp tptpp show t U t by rule smallbigbz39g qed next assume t t IsZera Zero and tp t Tru show val t a t U t proof assume vtpp val t with H have tptpp t U t by blast from tp tptpp have tpp t Tru using truz39nv by blast from t tpp tptpp show t U t apply simp apply rule BIsZemZem apply rule 13 Value apply simp apply blast clone qed next x tt assume t t IsZem Succ tt and tp t Fls and nut Humval tt show val t a t U t proo assume vtpp val t with H have tptpp t U t by blast with tp have tttpp Fls U t by simp hence tpp t Fls using fls z39uv by blast from nut have val tt by simp hence tttt tt U tt by rule 13 Value hence Succ tt U Succ tt by rule BSucc with t tpp nut show t U t apply simp apply rule BIsZemSucc by auto qed next x tt t a assume t t IsZem tt and tp t IsZem t a and ttp tt gt t a show val t a t U t proof assume vtpp val t with H have tptpp t U t by blast with tp have IsZem t a U t by simp from ttp t tp have ttp t lt gt t by blast from ttp tptpp show t U t by rule smallbigbig lemma Abz39 ruleformat t1 t t1 gt V t2 ta IF t1 t2 t3 lt gt IF t1 t2 t3 proof induct rule multi evalsiz39uduct x t show Vt t3 Ft t2 t3 t gt Ft t2 t3 using merefl by blast next xtt t assume ttp t lt gt t and t lt gt t and H2 Vt2 t3 Ft t2 t3 lt gt IFt t2 t3 show V752 753 Ft t2 755 V Ft t2 755 proof clarify x t2 755 from ttp have a Ft t2 t3 lt gt F t t2 t3 by rule E If from H have b Ft t2 t3 lt gt IFt t2 t3 by simp from a b show Ft t2 t3 lt gt IFt t2 t3 by rule mestep qed qed lemma A6succrulef0739matz t1 lt gt t1gt Succ t1 lt gt Sues tl applyz39uduct rule multievalsiinduct using merefl apply blast using E Succ mestep by blast lemma A predrulef0rmatz t1 lt gt t1gt Pred t1 lt gt Pred tl applyz39uduct rule multievalsiiuduct using merefl apply blast using E Pred mestep by blast lemma A6iszer0rule f0rmatz t1 lt gt tl gt IsZero t1 lt gt IsZero tl applyz39uduct rule multievalsiiuduct using merefl apply blast using E IsZem mestep by blast lemma multi sz39nglemultiruleformatz t1 lt gt t2 gt V t3 t2 lt gt t3 a t lt gt t3 apply induct rule multievalsiiuduct apply clarify using mestepaft t3 t3 apply blast apply clarify apply eruletac xt5 in allE apply simp using mestep by blast 10 lemma multitransitive ruleformat t lt gt t2 gt V t3 t2 gt t3 A t lt gt t3 apply induct rule multievalsinduct apply simp apply clarify apply eruletac xt5 in allE apply simp using mestep by blast lemma bigimpliesvalue t U u gt val 1 apply induct rule bigstepinduct by auto lemma bigimpliessmallruleformat2 t U u gt val v A t lt gt v proof induct rule bigstepinduct x 1 assume val 1 show val v A v lt gt 1 using merefl by blast next x t1 t2 v2 t3 assume t1 U Tru and H12 val Tru t1 lt gt Tru and t2 U v2 and H22 val v2 x t2 lt gt 112 show val 112 a F t1 t2 t3 lt gt v2 proo assume W22 val v2 from H1 have t1 t gt Tru by simp hence a2 F t1 t2 t3 lt gt F Tru t2 t by rule A if have 22 F Tru t2 t3 lt gt t2 by rule E fTrue from a b have c2 F t1 t2 t3 lt gt t2 by rule multisinglemulti from vv2 H2 have t2 lt gt v2 by simp With c show F t1 t2 t3 lt gt 112 by rule multitransitive qed next x t1 t3 1 t2 assume t1 U Fls and H12 val Fls x t1 lt gt Fls and t3 U v3 and H22 val vi a ti lt gt 1 show val vi a F t1 t2 t3 lt gt v3 proo assume vv val v3 from H1 have t1 t gt Fls by simp hence a2 F t1 t2 t3 lt gt F Fls t2 t by rule A if have 72 F Fls t2 t3 t gt t3 by rule E fFalse from a b have c2 F t1 t2 t3 lt gt t3 by rule multisinglemulti from vv H2 have t3 lt gt v3 by simp With c show F t1 t2 t3 V 1 by rule multitransitive assume t U 1 and H2 valv a t lt gt 1 show val Succ v Succ t lt gt Succ v proof assume val Succ 1 hence val v by auto with H have t lt gt v by clarify thus Succ t lt gt Succ v by rule A succ qed next x t assume t U Zero and H2 val Zero A t lt gt Zero show val Zero Predt V Zero proof 11 assume val Zero with H have t t gt Zero by simp hence a Pred t lt gt Pred Zero by rule A6 pred have Fred Zero lt gt Zero by rule E PredZero with a show Predt lt gt Zero by rule multi singlemulti assume tsv t it Succ v and H2 val Succ v A t lt gt Succ 1 show val v A Predt t gt v proof assume vv val u from tsv have val Sues v by rule bigimpliesvalue hence av uum val v by auto with H have ts t t gt Succ 1 apply simp apply erule impE by auto from ts have pp Pred t lt gt Pred Sues v by rule AE pred from m have pv Pred Sues v lt gt v by rule E PredSucc from pp pv show Predt lt gt v by rule multi singlemultz39 qed next x t assume t it Zero and H2 val Zero A t lt gt Zero from H have t lt gt Zero apply simp apply erule impE apply blast by simp hence zz IsZero t V IsZero Zero by rule A iszero have zt IsZero Zero lt gt Tru by rule E IsZeroZero from 22 at show val Tru A sZero t lt gt Tru apply clarify apply rule multisingle multi by auto next x t m assume t it Succ m and H2 val Succ up A t lt gt Succ m and m uum val m from m have val Succ av by auto with H have t lt gt Succ m by simp hence zz IsZero t V IsZero Sues nu by rule AE iszero have 2f IsZero Sues 7w lt gt Fls by rule E IsZeroSucc from 22 zf show val Fls A IsZero t lt gt Fls apply clarify apply rule multisingle multi by auto qed theorem bigeqsmall val v gt t it v t lt gt 1 apply rule z39 l apply rule bigimplies small apply simp apply simp apply rule smallimplies big apply auto clone end 12 Big step Semantics The following is a big step semantics for the lambda calculus that uses substitution to handle variables X e ll X e e1 ll x e3 e2 ll V1 X H V193 ll V2 e1 e2 ll v2 Big step Semantics Another approach to handling variables is to use an environment a mapping from variables to values This approach introduces a new kind of value a closure which is a expression together with an environment The notation Ex a v updates the environment E so that X maps to v E h e ll ltX e7 Egt EthlEX EhelllltXe3E gt Ehegllvl EXHV1h83llVQ Eh 81 ezllv2 Variable Representations gt Motivation a disadvantage of using symbols for variables is that that are equivalent aren39t necessarily syntactically identical XX yy zz gt One solution is to represent variables as pointers XX X y x y p O l l l DeBruijn Indices gt Another solution is to represent variables with relative addresses called DeBruijn indices gt Syntax for the lambda calculus e k l e l e e gt We use an integer that says which enclosing is the binding For example AX Ay X y A A 10 7 l l l DeBruijn Indices gt When we perform substitution X H e e we need to make sure that the indices in e sti point to the right place even though we are putting copies of e further down in the AST gt So we define a shift operator T that shifts the indices by d with a cutoff of c The cutoff is so that when we shift under a we don39t shift the variables bound by the x Tgk ifkltcthenkelsekd T Ax e A T e i 91 92 ige1 i 92 Substitution with DeBruijn Indices gt Definition of substitution UHe M ifkjthene elsek JaeMA e U1HT e e U H 991 92 U H 9191 U H 919 gt The B reduction rule e v a 0 gt gtT1ve gt Example X yx z E y gt gt zx X X 1 1 31 0 HT511HA0 Substitution with DeBruijn lndices continued The problematic example that had freevariable capture is no problem here w W W x y Al or Al 1 0 w x H mm X Al ial 0 e no 1 w M X e W A if A 1 e 211 l M AuD A if A 2 AM All Y AA AA lfl 2 we M y Al Al 1 Locally Nameless Representation gt Motivation the shifting business for DeBruijn indices is messy and makes it hard for humans to read the lemmas and theorems gt A new alternative is a hybrid approach that uses DeBruijn indices for bound variables and symbols for free variables gt Syntax for the lambda calculus e X l k l e l e e gt Substitution for bound variables k H ui if k i then u else i k H ux X k H u e k 1 H ue AA k H ue1 e2 k H ue1 k H U82 Locally Nameless Representation gt Substitution for free variables X H e i 39 X H e y if y X then 9 else y X H e e X H e e X H e el 82 X H e el X H 882 gt red uction rule e v H O H ve Existential Types gt Provide a form of first class information hiding abstract data types gt Example p pack Nat 5 AXNat succ X as aagtlt aaa open p as x in 5nd X fst X Existential Types Syntax 39 Ha T e pack T79 as T open 9 as 04X in 9 Evaluation contexts E pack T7E as T open E as 04X in 9 Reduction rule open pack T17 v as T2 as 04X in e a a gt gt T1X gt gt ve Type rules I39Feozgt gtUT FFewaTl FozxT1FegT2 I F pack U7 9 as HOLT I F open el as 04 X in 822 T2 Encoding Existentials with Universals 304 T EVB VaT gt gt 3 pack The as 3047 E AB f Va T2 a fT1e open el as 04x in 82 E elT2 Aa XI T1 92 where 822 T2 and 91304 T1 Using Existentials to Model Objects Counter 3a state 1 methods get a A Nat7 inc a A a c Nat state 5 methods get AXNat X inc AXNat succ as Counter open c as abody in bodymethodsgetbodystate gt 5 Nat sendinc AcCounter open c as abody in a state bodymethodsincbodystate methods bodymethods as Counter gt sendinc Counter A Counter Untyped Arithmetic Expressions Context free grammar in BNF notation expr quottruequot i false quotifquot expr then expr else expr i 0 i quotsuccquot expr i quotpredquot expr i quotiszeroquot expr value quottruequot i false i numvalue numvalue 0 i succ numvalue The same context free grammar in the textbook39s notation e true i false i if e then e else e i O i succ e i pred e i iszero e v true i false i nv nv 0isuccnv Inductive Definitions A context free grammar is an example of an inductively defined set Definition An inductively defined set is the smallest set that obeys a particular set of rules Example Here39s the set of rules for the set expr 1 true 6 expr 2 false 6 expr 3 Velezegv e1 6 expr and e2 6 expr and e3 6 expr implies if e1 then e2 else e3 6 expr 4 O E expr 5 Vet e E expr implies succ e E expr 6 Vet e E expr implies pred e E expr 7 Vet e E expr implies iszero e E expr Horiz ntal bar means implication We often use a horizontal bar to mean implication Also we leave implicit the variable quantification the Vs Example Here39s the same set of rules 1 2 l true 6 expr false 6 eXpr e1 6 expr e2 6 expr e3 6 expr 1 l I if e1 then e2 else e3 6 expr e 6 ex r e 6 ex r 4 5 p a p O E expr SUCC 6 6 exp pred e E expr e E expr iszero e E expr Derivations The presense of a particular element in an inductively defined set is justified by a tree of rule applications which is called a derivation We label each rule application with the rule number Example We know that if iszero 0 then 0 else succ 0 E expr because we can build the following derivation 4 O E expr 4 O E expr 7 M iszero O E expr 4 O E expr 5 succ O E expr if iszero 0 then 0 else succ 0 E expr Inductive Definitions Why do we say that an inductively defined set is the smallest set that obeys a given set of rules Answer to preventjunk from being allowed in the set Example quothello world expr because there is no derivation thatjustifies the presense of hello world in the set expr Recursive functions We can define a recursive function on terms by writing a sequence of equations Here39s a function that computes the size of an expression sizetrue 1 sizefalse 1 sizeif e1 then 92 else 93 1 sizeel sizeeg sizee3 size0 1 sizesucc e 1 sizee sizepred e 1 sizee size iszero e 1 sizee Recursive functions Here39s another function that computes the depth of an expression depthtrue 1 dept7fase 1 dept7if e1 then e2 ese e3 1 maxdepthe17 dept39hez7 depthe3 dept70 1 dept7succ e 1 dept7e depthprecl e 1 dept7e depthiszero e 1 dept7e We know this function terminates because the recursive calls are applied to arguments that are strictly smaller than the parameter to the recursive function For example on line 5 above the e in depthe is smaller than the succ e in depthsucc e Proof by Rule Induction We can prove properties of inductively defined sets using a special kind of induction called rule induction Suppose we want to prove some property P about elements of an inductively define set 5 VXX E 5 implies PX We can prove this by proving something for each rule that defined 5 In particular for a rule of the form beS 65 deF 365 we have to prove that b E 5 and c E 5 and d E F and Pb and Pc implies Pa We refer to Pb and Pc as the induction hypotheses Example Proof by Rule Induction Theorem V9 9 E expr implies depthe sizee Proof by rule induction on e E expr Case MW so 9 true We have depthtrue 1 and sizetrue 1 so depthe sizee Example Proof by Rule Induction continued so e succ e In this case we know that e E expr and from the induction hypothesis we have e E expr implies depthe sizee So we have depthsucc e 1 depthe 1 sizee by the induction hypothesis sizesucc e Therefore depthe sizee Example Proof by Rule Induction continued e1 6 expr e2 6 expr e3 6 expr if e1 then e2 else e3 6 expr i so e if e1 then e2 else e3 6 expr From the induction hypotheses we have depthe1 sizee1 depthe2 sizee2 and depthe3 sizee3 Then we have 3 depthif e1 then e2 else e3 1 maxdept he17 dept he27 depthe3 1 maxsizee1sizee27 sizee3 1 sizee1 sizee2 sizee3 sizeif e1 then e2 else e3 Therefore depthe sizee Inductively Defined Relations Definition A relation is a set of tuples So everything we39ve said about sets also applies to relations For example suppose you have an inductively defined relation R and the following is one of the defining rules for R aef R e65 fET 37 b7 6 E R Suppose you want to prove VXyz Xyz E R implies PXyz Then for the above rule you39d need to prove aef E Rande E 5 and f E Tand Paef implies Pa7 b7 6
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'