jagomart
digital resources
picture1_Programming Pdf 184296 | Notes Item Download 2023-02-01 04-03-02


 134x       Filetype PDF       File size 1.05 MB       Source: www.cs.utah.edu


File: Programming Pdf 184296 | Notes Item Download 2023-02-01 04-03-02
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 ...

icon picture PDF Filetype PDF | Posted on 01 Feb 2023 | 2 years ago
Partial capture of text on file.
                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
The words contained in this file might help you see if this file matches what you are looking for:

...Programming languages and lambda calculi utah cs version matthias felleisen matthew flatt draft march c copyright contents i models of chapter computing with text dening sets relations as evaluation directed in context function notation summary structural induction detecting the need for denitions ellipses on proof trees multiple structures more proofs consistency calculus functions grammar reductions encoding booleans pairs numbers recursion via self application lifting out fixed points y combinator facts about history ii realistic iswim expressions v observational equivalence standard reduction proving theorem uniform machines ccmachine sccmachine ckmachine cekmachine machine secd tail calls safe space secdmachine environment continuations saving contexts revised texual cek errors exceptions calculating error relating handlers handler extended cc cch imperative assignment...

no reviews yet
Please Login to review.