134x Filetype PDF File size 1.05 MB Source: www.cs.utah.edu
Programming Languages and Lambda Calculi (Utah CS7520 Version) Matthias Felleisen Matthew Flatt Draft: March 8, 2006 c Copyright 1989, 2003 Felleisen, Flatt 2 Contents I Models of Languages 7 Chapter 1: Computing with Text 9 1.1 Defining Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3 Relations as Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.4 Directed Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.5 Evaluation in Context . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.6 Evaluation Function . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.7 Notation Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Chapter 2: Structural Induction 15 2.1 Detecting the Need for Structural Induction . . . . . . . . . . . . . . . . . . . . . 15 2.2 Definitions with Ellipses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Induction on Proof Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.4 Multiple Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.5 More Definitions and More Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Chapter 3: Consistency of Evaluation 21 Chapter 4: The λ-Calculus 25 4.1 Functions in the λ-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.2 λ-Calculus Grammar and Reductions . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.3 Encoding Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.4 Encoding Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.5 Encoding Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.6 Recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4.6.1 Recursion via Self-Application . . . . . . . . . . . . . . . . . . . . . . . . 32 4.6.2 Lifting Out Self-Application . . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.6.3 Fixed Points and the Y Combinator . . . . . . . . . . . . . . . . . . . . . 34 4.7 Facts About the λ-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 4.8 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 II Models of Realistic Languages 39 Chapter 5: ISWIM 41 5.1 ISWIM Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.2 ISWIM Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 5.3 The Y Combinator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 v 5.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 5.5 Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3 4 5.6 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 5.7 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Chapter 6: Standard Reduction 53 6.1 Standard Reductions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 6.2 Proving the Standard Reduction Theorem . . . . . . . . . . . . . . . . . . . . . . 56 6.3 Observational Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 6.4 Uniform Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 Chapter 7: Machines 69 7.1 CCMachine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 7.2 SCCMachine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 7.3 CKMachine. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.4 CEKMachine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 7.5 Machine Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 Chapter 8: SECD, Tail Calls, and Safe for Space 83 8.1 SECDmachine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 8.2 Context Space . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 8.3 Environment Space . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 8.4 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 Chapter 9: Continuations 89 9.1 Saving Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 9.2 Revised Texual Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 9.3 Revised CEK Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 Chapter 10: Errors and Exceptions 93 10.1 Errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 10.1.1 Calculating with Error ISWIM . . . . . . . . . . . . . . . . . . . . . . . . 93 10.1.2 Consistency for Error ISWIM . . . . . . . . . . . . . . . . . . . . . . . . . 95 10.1.3 Standard Reduction for Error ISWIM . . . . . . . . . . . . . . . . . . . . 98 10.1.4 Relating ISWIM and Error ISWIM . . . . . . . . . . . . . . . . . . . . . . 99 10.2 Exceptions and Handlers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 10.2.1 Calculating with Handler ISWIM . . . . . . . . . . . . . . . . . . . . . . . 103 10.2.2 Consistency for Handler ISWIM . . . . . . . . . . . . . . . . . . . . . . . 104 10.2.3 Standard Reduction for Handler ISWIM . . . . . . . . . . . . . . . . . . . 105 10.2.4 Observational Equivalence of Handler ISWIM . . . . . . . . . . . . . . . . 106 10.3 Machines for Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 10.3.1 The Handler-Extended CC Machine . . . . . . . . . . . . . . . . . . . . . 107 10.3.2 The CCH Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 Chapter 11: Imperative Assignment 111 11.1 Evaluation with State . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 11.2 Garbage Collection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 11.3 CEKS Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 11.4 Implementing Garbage Collection . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 11.5 History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
no reviews yet
Please Login to review.