### Create a StudySoup account

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

Already have a StudySoup account? Login here

# PROGRAMMING LANGUAGES C S 386L

UT

GPA 3.8

### View Full Document

## 22

## 0

## Popular in Course

## Popular in ComputerScienence

This 3 page Class Notes was uploaded by Ryley Lang on Sunday September 6, 2015. The Class Notes belongs to C S 386L at University of Texas at Austin taught by William Cook in Fall. Since its upload, it has received 22 views. For similar materials see /class/181667/c-s-386l-university-of-texas-at-austin in ComputerScienence at University of Texas at Austin.

## Popular in ComputerScienence

## Reviews for PROGRAMMING LANGUAGES

### 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/06/15

Induction and Inductive Definitions William Cook CS 386L Uses of Induction Induction Proving a pmperbfor all elements of a set rwhere the sets of often de ned by rules rfor example showing that w is total and deterministic Types Mathematical induction Structural induction Induction on derivations Wellfounded induction Structural Induction Induction based on structure of term If for each term 5 assuming Pr for all IMmec ate subfamsr of 5 allows us to show Ps then Pt holds for all terms t Structural Induction Example A property Pa is true of all a in Aexp if For all natural numbers m Pm holds For all locations X it is the case that PX holds For all a0 and a1 if Pao and Pal then Pa0a1 For all a0 and a1 if Pao and Pal then Pao al For all a0 and a1 if Pao and Pal then Paoxal wAexp is Deterministic Structural induction using induction hypothesis Pa Vomm lta o w m lta o w m mm a E n There is only one rule for evaluating numbers n m m a 2 X There is only one rule for evaluating locations 000 m m a 2 a0 a1 similar for a0 a1 and a0 gtlt a1 If lta o w mm then by the rule there must exist mu m1 where ltau o w mD and lta o w m1 where mmnm1 and also exist m n m 1 where ltan o w m39El and lta o w mg where m39m39nm391 By the induction hypothesis applied to aEl and a1 we have rnEl m El and m1m Therefore m rrbm1 m nm 1 m wAexp is Total assuming 0 total Structural induction on a using induction hypothesis a V0 3m lta o w m Existence is demonstrated by letting m n a 2 Since 0 is a total function 000 must exist and so m 000 a 2 a0 a1 By induction hypothesis there exists rnEl such that ltau a w rnEl and mlsuch that lta a w m Le 1 Similar for aO a1 and a0 gtlt a1 Well founded Induction WeIIfounded relations A binary relationship lt on a set A is WElfaundedif it has no in nite descending chains a lt lt a1 lt 80 WeIIfounded induction If Px is true assuming Py for all yltx then Pa is true for all a in A Induction on Derivations Sometimes structural induction is not sufficient Cannot prove that wow is determinist39c Structural induction requires campastona rules Premises only involve subtermsquot While depends on same term ltb 11gt w true ltc 11gt w 0 ltwhile b do c a gt w aquot ltwhile b do c agt w aquot But any terminating computation must have a derivation chm is Deterministic Theorem 311 Pc Voooo ltc 00gt w o amp ltc 50gt w o 2 00 Derivation d of execution d it ltc ogt w o rltc 00gt terminates with state 0 Induction hypothesis P Voooo d it ltc 50gt w o ampltc 00gt w o 2 00 Define d39 lt d if d39 is a piece of the derivation d Vd lt d Pd 2 Pd Vd Pd chm is Deterministic Given Pd Vomop d it ltc 50gt w o ampltc 00gt w o 2 00 Show Vd 4 d Pd 2 Pd Show by cases that 3 d1d1lrltc 00gt w a 00 chm is Deterministic c 2 skip d d1 ltskip 50gt w 00 c 2 X a d lt8 00gt W n d lt6 00gt W quot1 ltgtlt 8 00gt W comX 1 By previous result for Aexp nn1 So 0 oongtlt oon1X Uses of Well Founded Induction Mathematical Induction lt is successor function n lt n1 for all n Structural Induction lt is term containment s lt t iff s is a subterm oft Induction on derivations lt is subderivation relation d lt d iff d is a subderivation ofd Structural induction on derivations ltx a 00gt w comX chm is Deterministic C E C0 C1 do d1 d lt50 00gt W 01 lt51 01gt W U lt50 51 00gt W 0 d lt50 00gt W 01 lt51 01 gt W 0 1 lt50 51 00gt W 0 By induction hypothesis Pd0 and Pd1 Dolol andoo Similar for if and while Inductive Definitions of a Set Existence Set of all terms that can be derived from the rules IR set of terms for which a derivation exists Closure De ne set as least set that is closed under a given set of rules Limits Create a series of sets by applying a set operator Take the limit or xedpa ntj of this series Rule instances Rules A n e Aexp 80 E eXp a1 e Aexp Xe Aexp aoale Aexp Rule instances Xy set of premisesconclusion Ql QZ QB Qx1 le Qx3 111 1 212 1 x11x1 1 x1x11 X1gtlt1gtlt1 X11 X2gtlt1gtlt2 1 221 XV 22gtlt1 Closure RClosed set Q is RCasedif for all rule instances Xy X Q Q Y E Q IR is the least set closed under rules R IR is Rclosed if Q is an R closed set then IR g Q But this does not tell us how to construct IR Or how to construct the rule instances Set Construction Operator 1 Define an operator based on rule instances RB v EXQB WY 6 R rcreate set of conclusions where all the premises are in B 1 Series A0 a R003 empty set A1 RAO R103 axioms A2 RAl R203 derived from axioms in 1 step An Rkl R Example 1 Operator RB NULocUaOa1aoale B 1 Sets AO Q A1 RAO N U Loc enumbers and locations A2RA1 NULocUaOa1aOale A1 enumbers locations and sum of any number or location 17 13 Explicit Construction Summary 1 Inclusion 1 Definitions are equivalent AOQAIQAZQmQAan R Closure Define limit Limit of repeated application of operator R A UHEUAW Fixedpoint of operator R A is R closed RA 1 Lets use them A is the least Rclosed set 1 Fixedpoint of an operator xR A such that RA A NR Um Rquot3 19 2o Inductive Syntax Definition Inductive Definition of Relations 1 Formal explanation of Aexp Bexp and Com We have alread l seen one W 5 6 A943 11 nixlaoallao allaogtltal ltn11gtn Const lta139 gtwn1 b e Bexp true false 60 a1 605 a1 lt32 17gt W 2 Sub bi boA b1 b0 V b1 09 11gt W 1100 Loc lta1 a2 11gt w n c e Com skiplXacoc1 a wn where nisD veresuto if b then cO else c1 while b do c lt 1 17gt 1 Emma I mquot lt82 11gt W n2 1 Interpret grammar as inference rules which lta a 11gt w n 5W lt81 11gt W m 1 2i generate the set I I where n mm m lt82 11gt W n2 Prod Ba5is for sb39ucmrdnductmn 0 n1 and n2 lt31 X 32 17gt W n where n isn veproatlct of n1 and n2 21 22 Inductive Semantics of While fiXRw gt ltb 11gt w true ltc 11gt w 11 ltb 11gt w false ltwhile b do c 11 gt w 11 ltwhile b do c 11gt w 11 ltwhile b do c 11gt w 11 1 Convert rules to operator RN RWS ltwhile b do c 11 11gt ltb 11 falsegt e WSW U ltwhile b do c 11 11 gt ltb 11 truegt e WSW 81 ltc 11 11 gt e S ampltwhile b do c 11 11 gt e S U 07 7139r rules for Cam Inductive Function Definitions Variables in an arithmetic expression Loc n Loc X X Loc a0 a1 Locao U Local Loc aO a1 Locao U Local Loc 60 x a1 Locao U Local 1 We are used to seeing programs of this form But normally a de nition gives a convenient name to something that is previously known But here the thing being de nedquot is used in the de nition In what sense is this a de nition

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

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

#### "I used the money I made selling my notes & study guides to pay for spring break in Olympia, Washington...which was Sweet!"

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

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