Popular in Course
Popular in ComputerScienence
verified elite notetaker
This 42 page Class Notes was uploaded by Vito Kilback on Wednesday September 23, 2015. The Class Notes belongs to CS550 at Drexel University taught by JeremyJohnson in Fall. Since its upload, it has received 28 views. For similar materials see /class/212431/cs550-drexel-university in ComputerScienence at Drexel University.
Reviews for ProgrammingLanguages
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/23/15
Programming Languages CS 550 Lecture 7 Summary Operational Semantics of Scheme using Substitution Jeremy R Johnson Starting Point Informal Scheme Semantics 39139 To evaluate E1 E2 En recursively evaluate E1 E2En E1 should evaluate to a function and then apply the function value of E1 to the arguments given by the values of E2En 39139 In the base case there are self evaluating expressions eg numbers and symbols In addition various special forms such as quote and if must be handled separately Theme 1 This lecture continues our exploration of the semantics of scheme programs Previously we informally discussed the substitution model environments and provided an interpreter for scheme that operationally de ned the semantics of scheme programs 1 In this lecture we will more formally study the substitution model using the lambda calculus We will also look at alternative lazy semantics for scheme and an implementation of streams 3 O 99 Lambda Calculus The semantics of a pure functional programming language can be mathematically described by a substitution process that mimics our understanding of function application ie substitute all occurrences of the formal parameters of a function in the function body by the arguments in the function call In order to formally study function de nition and application and computability logicians Alonzo Church Stephen Cole Kleene and others in the 1930s developed a formal notation called the lambda calculus and rules defining an equivalence relation on lambda expressions that encodes function de nition and application They showed the universality of the lambda calculus the uniqueness of normal forms and the undecidablity of the equivalence of lambda expressions Outline 39139Review substitution model of computation 39139Review shortcomings of substitution model 39139Review streams and delayed evaluation gtAdding support for streams gtInterpreter with lazy semantics 1 Lambda calculus gtFree and bound variables gtalpha and beta reduction gtUniversality of lambda calculus Substitution Model of Computation 1 function application corresponds to substituting the argument expressions into the formal parameters of the function body 1 Order of evaluation gtApplicative vs normal order gtlambda calculus gtChurchRosser Substitution Example 3 de ne square X X X 3 de ne sumof squares X y square X square y 3 de ne f a sumof squares a 1 a 2 applicative order 3 f5 2 sumof squares 5 1 5 2 gt square 6 square 10 gt 6 6 10 10 gt 36 100 gt 136 normal order 3 f5 2 sumof squares 5 1 5 2 gt square 5 1 square 5 2 2e ltlt51gtlt51gt ltlt52gtlt52gt gt 6 6 10 10 gt 36100 Order Matters de ne p 19 de ne test X y if X 0 0 y test 0 13 Environments 1 When assignment is introduced the substitution model falls apart and a different model more complicated model must be used 1 Environments used to store variables and bindings gtValues can change gtassignment supported gtList of frames to support nested scope Cost of Assignment define makesimplifiedWithdraw balance lambda amount set balance balance amount balance define W makesimplifiedWithdraw 25 W 10 15 W 10 5 define makedecrementer balance lambda amount balance amount define D makedecrementer 25 D 10 15 D 10 15 Substitution Model Fails makedecrementer 25 20 gt lambda amount 25 amount 20 gt 25 20 gt 5 makesimp1i edWithdraw 25 20 gt lambda amount set balance 25 amount 25 20 gt set balance 25 20 25 Environment Model Solves Problem de ne W1 makeWithdraw 100 VVlSO de ne W2 makeWithdraw 100 Parameters body Streams 1 Sequenee of elements gtcons stream X y gtstreamcar s gtstreamcdr s gtstreamnull s gttheemptystream Streams are Not Lists 39139 Consider the following example car cdr lter prime enumerateinterval 10000 1000000 39139 This would be extremely inef cient if implemented with lists gt Do not build the entire stream of elements gt Get the next element from the stream when needed gt Necessary for potentially in nite streams Delayed Binding consstream ltagt ltbgt ltgt cons ltagt delay ltbgt de ne streamcar stream car stream de ne streamch stream force cdr stream delay lteXpgt ltgt lambda lteXpgt de ne force delayedobject delayedobject 1 Scheme Interpreter To evaluate a combination a compound expression other than a special form evaluate the subeXpressions and then apply the value of the operator subeXpression to the values of the operand subeXpressions To apply a compound procedure to a set of arguments evaluate the body of the procedure in a new environment To construct this environment extend the environment part of the procedure object by a frame in which the formal parameters of the procedure are bound to the arguments to which the procedure is applied Scheme Interpreter eval define eval exp enV cond self evaluating exp exp vanable exp lookupvariablevalue exp env quoted exp textof quotation exp assignment exp evalassignment exp env de nition exp evalde nition exp env if exp evalif exp env lambda exp makeprocedure lambdaparameters exp lambdabody exp env begin exp evalsequence beginactions exp env cond exp eval condgtif exp env application exp apply eval operator exp enV listof values operands exp env else error quotUnknown expression type EVALquot exp Scheme Interpreter apply define apply procedure arguments cond primitiveprocedure procedure applyprimitiveprocedure procedure arguments compoundprocedure procedure evalsequence procedurebody procedure extendenvironment procedureparameters procedure arguments procedureenvironment procedure else error quotUnknown procedure type APPLYquot procedure Stream Practice Exercises 3 Complete the trace of streamcar stream0dr stream lter prime stream enumerateinterval 10000 1000000 2 Modify the scheme interpreter from SICP to support force delay and streams You should implement everything needed to execute the above computation Scheme Interpreter With Streams added to eval delay eXp evaldelay eXp enV consstream eXp evalconsstream eXp enV new functions define delay eXp taggedlist eXp 39delay define evaldelay eXp enV makeprocedure 39 cdr exp enV define evalconsstream eXp enV eval list 39cons consstreamopl exp list 39delay consstreamopZ eXp em 20 Scheme Interpreter With Streams The following need to be defined in the metacircular evaluator to complete the implementation of streams define force delayedobject delayedobj ect define streamcar stream car stream define streamcdr stream force cdr stream define streamnull stream null stream 21 Lazy Evaluation 0 v Language with normal order semantics Compound procedures are nonstrict while primitive procedures remain strict gt Procedure strict if arg evaluated before entering gt Procedure nonstrict if proc not evaluated before entering v Delaying evaluation until last possible moment is called lazy evaluation 39139 Delay evaluation of arguments by converting them to thunks v A thunk is forced only when its value is needed v Memoize thunks to avoid repeated evaluation 22 Examples of Lazy Evaluation define try a b if a 0 l b try 0010 define unless condition usualvalue exceptionalvalue if condition exceptionalvalue usualvalue unless b 0 a b begin display quotexception returning 0quot 0 23 Lazy Scheme Interpreter eval application eXp apply actualvalue operator eXp env operands eXp env define actualvalue eXp env forceit eval eXp env define evalif eXp env if true actualvalue ifpredicate eXp env eval ifconsequent eXp env eval ifalternative eXp env 24 Lazy Scheme Interpreter apply define apply procedure arguments enV cond primitiveprocedure procedure applyprimitiveprocedure procedure listof argvalues arguments enV changed compoundprocedure procedure evalsequence procedurebody procedure extendenvironment procedureparameters procedure listof delayedargs arguments enV changed procedureenvironment procedure else error quotUnknown procedure type APPLYquot procedure 25 Lazy Scheme Interpreter apply define listof argvalues eXps env if nooperands eXps 39 cons actualvalue firstoperand eXps env listof argvalues restoperands eXps env define listof delayedargs eXps env if nooperands maps 390 cons delayit firstoperand eXps env listof delayedargs restoperands eXps enV 26 Representing Thunks define forceit obj if thunk obj actualvalue thunkexp obj thunkenv obj obj define delayit eXp enV list 39thunk eXp env define thunk obj taggedlist obj 39thunk 27 Lazy Evaluation in Action define inputprompt quot LEval inputz define outputprompt quot LEval valuez define driverloop promptforinput inputprompt let input read let output actualvalue input theglobalenvironment announceoutput outputprompt userprint output driverloop define theglobalenvironment setup environment driverloop LEval input define try a b if a 0 l b LEval value 0k LEval input try 0 lt 1 0 LEval value 1 28 Memoization define fib 11 cond n 0 0 11 1 1 else fib n 1 fib 11 Z fib 5 29 Memoization define memoize f let table makeldtable lambda X let previouslycomputedresult ldtable get table X f or previouslycomputedresult let result f X ldtableput table X result result define memo b memoize lambda 11 cond lt n 0 0 ltlt n 1 1 else memoflb 39 11 1 memofib 11 2 30 Memoized Thunks define evaluatedthunk obj taggedlist obj 39evaluatedthunk define thunkvalue evaluatedthunk cadr evaluatedthunk define forceit obj cond thunk obj let result actualvalue thunkexp obj thunkenv obj setcar obj 39evaluatedthunk setcar cdr obj result replace eXp with its value setcdr cdr obj 390 forget unneeded enV result evaluatedthunk obj thunkvalue obj else obj 31 Streams for Free v Previous implementation of streams required new special forms delay and consstream and the reimplementation of list functions for streams v In the lazy evaluator lists and streams are identical v Just need to make sure that cons is nonstrict gt Reimplement cons primitive gt Or implement cons car and cdr as functions see lambda calculus 32 Lambda Calculus Expressions l lt exp gt gt variable 2 application lt exp gt gt lt exp gt lt exp gt 3 abstraction lt exp gt gt lambda variable lt exp gt v Use currying to allow more than one parameter 33 Free and Bound Variables 1 The parameter of an abstraction is bound in the lambda body gt lambda X E 1 Variables not bound by a lambda are free exp exp is a symbol FVexp FVbodyexp parametersexp exp is an abstraction FVexp1 U FVexp2 exp exp 1 exp2 34 Lambda Calculus Reductions alpha conversion lambda XE is equivalent to lambda yEyX provided y does not appear free in E and y is not bound by a lambda when substituted for X in E beta reduction lambda XE F is equivalent to EFX Where F is substituted for all free occurrences of the variable X in E provided all free variables in F remain free when substituted for X in E 35 Universality of Lambda Calculus 1 Church numerals and arithmetic using lambda calculus 2 boolean logic predicates and conditional statements using lambda calculus 3 Data structures lists cons car cdr using lambda calculus 4 Recursion using lambda calculus 36 Y Combinator de ne fact lambda n if n O l quotlt n fact n DD 1 de ne Y lambda g lambda X g X X lambda X g X X 2 g Y g Y g xed point 3 de ne g lambda n f if n O 1 n f n DD 4 g Y g n 37 Lambda Calculus Practice Exc 1 Implement a scheme function FV exp which returns a list of the free variables in the scheme expression exp The scheme expression will not have let letrec or letquotlt statements the only bindings come from labda expressions 38 Lambda Calculus Practice Exc 2 Show that the and or and not functions using the lambda calculus in lecture 2b are correct by showing that the correct result is obtained for all combinations of the inputs 39 Lambda Calculus Practice Exc 3 Using betareduction show that succ two is three where two and three are the Church encodings the numbers 2 and 3 see the scheme code for Church numbers in lecture 2b Use induction to prove that cn addl O the number n where cn is the Church encoding of 11 You may assume that addl correctly adds 1 to its input 40 Lambda Calculus Practice Exc 4 Trace through the expansion use beta reduction of g Y g 3 using the functions g and Y from the discussion on the Y combinator Try implementing g and Y and computing g Y g 3 in scheme What happens and Why Try this again using the normal order scheme interpreter in Section 422 of SICP 41 Lambda Calculus Practice Exc 5 Implement a scheme function that performs a beta reduction You must also have a predicate which checks to see if the beta reduction is valid ie the substitution does not cause problems with name collisions 42
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'