New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here


by: Kathleen Cartwright


Kathleen Cartwright
GPA 3.73


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in Computer Information Technology

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.

Similar to CIS500 at Penn

Popular in Computer Information Technology




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


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


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'

Why people love StudySoup

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Jennifer McGill UCSF Med School

"Selling my MCAT study guides and notes has been a great source of side revenue while I'm in school. Some months I'm making over $500! Plus, it makes me happy knowing that I'm helping future med students with their MCAT."

Bentley McCaw University of Florida

"I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

Parker Thompson 500 Startups

"It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.