Popular in Course
verified elite notetaker
Popular in Computer Information Technology
verified elite notetaker
This 13 page Class Notes was uploaded by Kathleen Cartwright on Monday September 28, 2015. The Class Notes belongs to CIS500 at University of Pennsylvania taught by Staff in Fall. Since its upload, it has received 6 views. For similar materials see /class/215377/cis500-university-of-pennsylvania in Computer Information Technology at University of Pennsylvania.
Reviews for SOFTWAREFOUNDATIONS
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: 09/28/15
C18 500 7 Software Foundations Midterm 1 Review Questions Untyped lambdacalculus l 2 points We have seen that a linear expression like Ax Ply x y x is shorthand for an abstract syntax tree that can be drawn like this Ax l Ay l apply apply Draw the abstract syntax trees corresponding to the following expressions aabc b AX b c d 2 10 points Write down the normal forms of the following Aterins a At A F t At A F F AX X b AX X AX X AX X AX X c AX X AX X AX X d AX X AX X AX X AX XX e AX XXX AX XXX 3 4 points Recall the following abbreviations from Chapter 5 tru At Af t f39ls At A1 1 not Ab b f39ls tru Complete this definition of a lainbda term that takes two church booleans b and c and returns the logical exclusive or of b and c xor Ab Ac 4 8 points A list can be represented in the lambdacalculus by its Fo39l d function OCaml s name for this U1 function is Fo39l dr39i ght it is also sometimes called reduce For example the list xyz becomes a function that takes two arguments c and n and returns c x c y c Z n The definitions of n39i39l and cons for this representation of lists are as follows n39i39l Ac An n39 cons Ah At Ac An c h t c n Suppose we now want to define a Aterm append that when applied to two lists quotll and 12 will append quotll to 12 i ie it will return a Aterm representing a list containing all the elements of quotll and then those of 39I 2 Complete the following definition of append append All A39IZ Ac An 6 points Recall the callbyValue fixedpoint combinator from Chapter 5 x A1 Ax f Ay x x y Ax f Ay x x y We can use F39i x to write a function sumupto that given a Church numerals m calculates the sum of all the numbers less than or equal to m as follows 9 A1 Am 39iszro m Ax c0 Ax p39lus prd m U sumupto x 9 Fill in the two omitted subterms Nameless representation of terms 6 4 points Suppose we have de ned the naming context I a b c d What are the deBruijn represen tations of the following Aterms a Ax Ay xyd b Ax c Ply c y x d 7 4 points Write down in deBruijn notation the terms that result from the following substitutions a 0 e A0A 0 l l b 0 HA 0 l 0 l 0 Typed arithmetic expressions The full de nition of the language of typed arithmetic and boolean expressions is reproduced for your reference on page 10 00 9 points Suppose we add the following new rule to the evaluation relation succ true gt pred succ true Which of the following properties will remain true in the presence of this rule For each one write either remains true or else becomes false plus in either case a onesentence justi cation of your answer a Termination of evaluation for every term t there is some normal form t such that t 8 t b Progress if t is well typed then either t is a value or else t gt t for some t c Preservation if t has type T and t gt t then t also has type T 9 9 points Suppose instead that we add this new rule to the evaluation relation t gt if true then t e39l se succ Fa39l se Which of the following properties remains true Answer in the same style as the previous question a Termination of evaluation for every term t there is some normal form t such that t 8 t b Progress if t is well typed then either t is a value or else t gt t for some t c Preservation if t has type T and t gt t then t also has type T 10 9 points Suppose instead that we add a new type Funny and add this new rule to the typing relation if true then Fa39l se e39l se Fa39l se Funny Which of the following properties remains true Answer in the same style as the previous question a Termination of evaluation for every term t there is some normal form t such that t 8 t b Progress if t is well typed then either t is a value or else t gt t for some t c Preservation if t has type T and t gt t then t also has type T Simply typed lambdacalculus The de nition of the simply typed lambdacalculus with booleans is reproduced for your reference on page 12 ll 6 points Write down the types of each of the following terms or ill typed if the term has no type a AxBoo39 xx b Af Boo39laBoo39l AgBoo39Boo39 g F 9 true c AhBoo39 A39i Boo39laBoo39l 39i false AkBoo39 true Operational semantics 12 9 points Recall the rules for bigstep evaluation of arithmetic and boolean expressions from HW 3 t1U0 vUv pred t1 U0 t1Utrue tzUvz t1 U succ nvl 1ft1 then t2 e39lse t3 Uvz pred t1 U nvl t1 U false t3 U V3 I 1on 1ft1 then t2 e39lse t3 UV3 39iszero t1 U true t1 U nvl t1 U succ nvl succ t1 U succ nv1 39I szero t1 U Fa39l se The following OCaml de nitions implement this evaluation relation almost correctly but there are three mistakes in the eva39l functionione each in the TmI F TmSucc and TmPred cases of the outer match Show how to change the code to repair these mistakes Hint all the mistakes are omissions 39Iet rec 39isnumer39icva39l t match t with TmZero a true TmSucctl a 39isnumer39icva39l tl a false 39Iet rec 39isva39l t match t with TmTrue a true TmFa39Ise a true t when 39isnumer39icva39l t a true se 39Iet rec eva39l t match t with v when 39isva39l v a v TmIftlt2t3 a match tl w ith TmTrue a eva39l t2 TmFa39Ise a eva39l t3 a raise NoRu39IeApp39l39ies TmSuccf39i tl a match eva39l tl w ith nvl a TmSucc dummy39im o nvl a raise NoRu39IeApp39l39ies TmPredf39i tl a match eva39l tl w ith TmZero a TmZerodummy39im o a raise NoRu39IeApp39l39ies TmIsZerof39i tl a match eva39l tl w ith TmZero a TmTruedummy39info TmSucc a TmFa39Isedummy39im o a raise NoRu39IeApp39l39ies a raise NoRu39IeApp39l39ies For reference Untyped boolean and arithmetic expressions syntax t true fa39lse 39iftthen t e39lset 0 succ t pred t 39iszero t true false nv 0 succ nv Boo Evaluation if true then t2 e39l se t3 gt t2 39i F Fa39l se then t2 e39l se t3 a t3 t1gtti 39iftl then t2 e39lse t3 81ft then t2 e39lse t3 t1 8 t 1 succ t1 succ t 1 pred 0 0 pred succ nv1 gt nv1 t1 8 t 1 pred t1 gt pred t 1 39iszero 0 true 39iszero succ nv1 gt Fa39l se t1 8 t 1 39iszero t1 gt 39iszero t39l terms constant true constant false conditional constant zero successor predecessor zero test values true value false value numeric value numeric values zero value successor value 04793 type of booleans type ofnumbers EIFTRUE EIFFALSE ElF ESUCC EPRED ZERO EPREDSUCC EPRED EISZEROZERO EISZEROSUCC EISZERO continued on next page Typing true Boo39l fa39lse Boo39l t1 I BOOI t2 I T if t1 then t2 e39lse t3 0 Nat t1 Nat succ t1 Nat t1 Nat pred t1 Nat t1 I Nat 39iszero t1 Boo39l t3 ET ET TTRUE TFALSE TIF TZERO TSUCC TPRED TISZERO For reference Simply typed lambda calculus with booleans syntax t terms true constant true Fa39l se constant false if t then t e39l se t conditional x variable Ax T t abstraction t t application v values true true value Fa39l se false value AxTt abstraction value T types Boo39l type ofbooleans TaT type offunctions Evaluation if true then t2 e1 se t3 8 t2 EIFTRUE if faT se then t2 e1 se t3 8 t3 EIFFALSE t a t 1 1 EIF 1ft1 then t2 e39lse t3 gt 39I Ftl then t2 e39lse t3 t a t 1 EAPPI t1 t2 8 t1 t2 t a t 2 2 EAPPZ V1 t2 8 V1 t2 AXT11 1112 V2 8 X gt V2t12 EAPPABS Typing true BooT TTRUE Fa39lse BooT TFALSE t 8001 t T t T 139 NF 1ft1 then t2 e39lse t3 T xT E T TVAR F F x T FXT F t T TABS P h AXT1t2 I T1gtT2 F F t T aT F F t T 1 11 12 2 11 TAPP rhtltlelz
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'