### Create a StudySoup account

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

Already have a StudySoup account? Login here

# SOFTWARE FOUNDATIONS CIS 500

Penn

GPA 3.76

### View Full Document

## 8

## 0

## Popular in Course

## Popular in Computer & Information Science

This 45 page Class Notes was uploaded by Jackson Will on Monday September 28, 2015. The Class Notes belongs to CIS 500 at University of Pennsylvania taught by B. Pierce in Fall. Since its upload, it has received 8 views. For similar materials see /class/215415/cis-500-university-of-pennsylvania in Computer & Information Science at University of Pennsylvania.

## Reviews for SOFTWARE FOUNDATIONS

### 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

CIS 500 Software Foundations Fall 2006 October 2 Preliminaries Homework Results of my email survey gt There was one badly misdesigned PhD problem and a couple of others that were less well thought through than they could have been These generated the great majority of specific complaints gt Besides these most people felt the homeworks were somewhat but not outrageously too long gt People seemed more or less happy with the pace of the course but no one wanted it faster gt PhD questions are an issue for mixed groups Homework Conclusion gt Basically hold course gt Make homeworks a little shorter and tighter gt Change grading scheme for PhD problems gt NonPhD students in PhD groups will be graded the same as those in nonPhD groups gt Slow down a little more on harder bits of material during lectures gt I need your help for this Midterm gt Wednesday October 11th gt Topics gt Basic OCamI gt TAPL Chapters 3 9 gt Inductive definitions and proofs gt Operational semantics gt Untyped lambdacalculus gt Simple types More About Bound Variables Substitution Our definition of evaluation is based on the substitution of values for free variables within terms Axt12 V2 x gt gt V2t12 E APPABS But what is substitution exactly How do we define it Substitution For example what does Ax x Ay X y Ax x y x reduce to Note that this example is not a complete program the whole term is not closed We are mostly interested in the reduction behavior of closed terms but reduction of open terms is also important in some contexts gt program optimization gt alternative reduction strategies such as full beta reduction Formal izing Substitution Consider the following definition of substitution x gt gt sx s XHSlYY ifxa y x gt gt syt1 y x gt gt st1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition Formal izing Substitution Consider the following definition of substitution x gt gt sx s XHSlYY ifxa y x gt gt syt1 y x gt gt st1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition t substitutes for free and bound variables xgt gt yx x xy This is not what we want Substitution take two xgt gtsxs xgt gtsyy ifxy y xgt gtsyt1y xgt gtst1 ifxy y xgt gtsxt1x t1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition Substitution take two x gt gt sx s xgt gtsyy ifxy y xgt gtsyt1y xgt gtst1 ifxy y x gt gt sxt1 x t1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition It suffers from variable capture xgt gt yyx x x This is also not what we want Substitution take three xgt gtsxs XHSYY ifxaey xgt gtsyt1y xgt gtst1 ifxy y y FVs xgt gtsxt1x t1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition Substitution take three xgt gtsxs XHSYY ifxaey xgt gtsyt1y xgt gtst1 ifxy y y FVs xgt gtsxt1x t1 x gt gt st1 t2 x gt gt st1x gt gt st2 What is wrong with this definition Now substition is a partial function Eg x gt gt yyx is undefined But we want an result for every substitution Bound variable names shouldn t matter It39s annoying that that the spelling of bound variable names is causing trouble with our definition of substitution Intuition tells us that there shouldn39t be a difference between the functions xx and yy Both of these functions do exactly the same thing Because they differ only in the names of their bound variables we39d like to think that these are the same function We call such terms alpha equivalent Alpha equivalence classes In fact we can create equivalence classes of terms that differ only in the names of bound variables When working with the lambda calculus it is convenient to think about these equivalence classes instead of raw terms For example when we write xx we mean not just this term but the class of terms that includes yy and zz We can now freely choose a different representative from a term39s alpha equivalence class whenever we need to to avoid getting stuck Substitution for alpha equivalence Classes Now consider substitution as an operation over alpha equivalence classes of terms XHsxs XHSlYY ifxa y XHsyt1 y XHst1 ifxy y y FVs XHsxt1 x t1 x H st1 t2 x H st1x H st2 Examples gt x H yyx must give the same result as x H yzx We know the latter is zy so that is what we will use for the former gt x H yxz must give the same result as x H ywz We know the latter is wz so that is what we use for the former Review So what does Ax x y x y Ax x y x reduce to Types Plan gt For today we39ll go back to the simple language of arithmetic and boolean expressions and show how to equip it with a very simple type system gt The key property of this type system will be soundness Well typed programs do not get stuck gt Next time we39ll develop a simple type system for the lambda calculus gt We39ll spend a good part of the rest of the semester adding features to this type system Outline 1 begin with a set of terms a set of values and an evaluation relation N define a set of types classifying values according to their shapes define a typing relation t T that classifies terms according to the shape of the values that result from evaluating them A 4 check that the typing relation is sound in the sense that 41 ift Tandtgtvthenv T 42 ift T then evaluation oft will not get stuck Review Arithmetic Expressions Syntax 1 terms true constant true false constant false if t then t else t conditional O constant zero succ t successor pred t predecessor iszero t zero test values true true value false false value nv numeric value numeric values 0 zero value SUCC 11V SUCCESSOI value Evaluation Rules if true then t2 else t3 Atg E IFTRUE if false then t2 else t3 Atg E IFFALSE t1gtt if t1 then t2 else t3 8 if t3 then t2 else t3 E IF 1318133 succ 131 succ t3 pred O a O pred succ nvl nvl 11 133 pred 131 pred t3 iszero O a true iszero succ nvl false t1 A133 iszero 131 iszero ta E SUCC E PREDZERO E PREDSUCC E PRED E ISZERO ZERO E ISZEROSUCC E ISZERO Types In this language values have two possible shapes they are either booleans or numbers types Bool type of booleans Nat type of numbers Typing Rules true Bool T TRUE false Bool T FALSE t Bool t T t T T1F if t1 then t2 else 03 T 0 Nat T ZERO t Nat 1 T SUCC succ t1 Nat t Nat 1 T PRED pred t1 Nat t Nat 1 T ISZERO iszero t1 Bool Typing Derivations Every pair t7T in the typing relation can bejustified by a derivation tree built from instances of the inference rules T ZERO T ZERO 0 2 Nat 0 2 Nat T ISZERO T ZERO T PRED iszero O ZBoo 0 2 Nat pred 0 2 Nat T IF if iszero 0 then 0 else pred 0 2 Nat Proofs of properties about the typing relation often proceed by induction on typing derivations Imprecision of Typing Like other static program analyses type systems are generally imprecise they do not predict exactly what kind of value will be returned by every program but just a conservative safe approximation t BOO t2 T t3 T 1f t1 then t2 else t3 T Using this rule we cannot assign a type to if true then 0 else false even though this term will certainly evaluate to a number Properties of the Typing Relation Type Safety The safety or soundness of this type system can be expressed by two properties 1 Progress A well typed term is not stuck Ift T then either t is a value or else 2 a t for some t 2 Preservation Types are preserved by onestep evaluation Ift Tandtgt t then 25 T Inversion Lemma 1 If true R then R B001 2 If false R then R Bool 51001 If if t1 then t2 else t3 R then t1 Bool t2 R and t3 R If 0 R then R Nat If succ t1 R then R Nat and t1 Nat prred t1 R then R Nat and t1 Nat If iszero t1 R then R B001 and t1 Nat Inversion Lemma 1 If true R then R B001 2 If false R then R B001 3 If if t1 then t2 else t3 R then t1 Bool t2 R and t3 R 4 If 0 R then R Nat 5 If succ t1 R then R Nat and t1 Nat 6 prred t1 R then R Nat and t1 Nat 7 If iszero t1 R then R B001 and t1 Nat Proof Inversion Lemma 1 If true R then R B001 2 If false R then R B001 3 If if t1 then t2 else t3 R then t1 Bool t2 R and t3 R 4 If 0 R then R Nat 5 If succ t1 R then R Nat and t1 Nat 6 lfpred t1 R then R Nat and t1 Nat 7 If iszero t1 R then R B001 and t1 Nat Proof This leads directly to a recursive algorithm for calculating the type of a term Typechecking Algorithm typeoft if t true then Bool else if t false then Bool else 1f t if t1 then t2 else t3 then let T1 typeoft1 in let T2 typeoft2 in let T3 typeoft3 in 1f T1 B001 and T2T3 then T2 else quotnot typablequot else if t 0 then Nat else if t succ t1 then let T1 typeoft1 in if T1 Nat then Nat else quotnot typablequot else if t pred t1 then let T1 typeoft1 in if T1 Nat then Nat else quotnot typablequot else if t iszero t1 then let T1 typeoft1 in if T1 Nat then Bool else quotnot typablequot Canonical Forms Lemma 1 If v is a value of type Bool then v is either true or false 2 If v is a value of type Nat then v is a numeric value Canonical Forms Lemma 1 If v is a value of type Bool then v is either true or false 2 If v is a value of type Nat then v is a numeric value Proof Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a t Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a 0 Proof Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a 0 Proof By induction on a derivation of t T Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a t Proof By induction on a derivation of t T The T TRUE T FALSE and T ZERO cases are immediate since t in these cases is a value Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a 0 Proof By induction on a derivation of t T The T TRUE T FALSE and T ZERO cases are immediate since t in these cases is a value Case T IF t if t1 then t2 else t3 tlzBool tQZT t32T Progress Theorem Suppose t is a well typed term that is t T for some T Then either t is a value or else there is some t with t a t Proof By induction on a derivation of t T The T TRUE T FALSE and T ZERO cases are immediate since t in these cases is a value Case T IF t if t1 then t2 else t3 tlzBool tQZT t32T By the induction hypothesis either t1 is a value or else there is some t 1 such that t1 t l If t1 is a value then the canonical forms lemma tells us that it must be either true or false in which case either E IFTRUE or E IFFALSE applies to t On the other hand if t1 t l then by E IF tgtif t1 then t2 else t3 Preservation Theorem If t T and t a t then 0 T Preservation Theorem If t T and t a t then 0 T Proof Recap Type Systems gt Very successful example of a lightweight formal method gt big topic in PL research gt enabling technology for all sorts of other things eg language based security gt the skeleton around which modern programming languages are designed

### 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

#### "Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

#### "I bought an awesome study guide, which helped me get an A in my Math 34B class this quarter!"

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

#### "Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

### Refund Policy

#### STUDYSOUP CANCELLATION 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 support@studysoup.com

#### STUDYSOUP REFUND POLICY

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: support@studysoup.com

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 support@studysoup.com

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.