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