jagomart
digital resources
picture1_Lambda Calculus Pdf 172157 | Lesson2


 190x       Filetype PDF       File size 0.12 MB       Source: www.classes.cs.uchicago.edu


File: Lambda Calculus Pdf 172157 | Lesson2
lesson 2 lambda calculus lesson2 lambda calculus basics 1 10 02 chapter 5 1 5 2 outline syntax of the lambda calculus abstraction over variables operational semantics beta reduction substitution ...

icon picture PDF Filetype PDF | Posted on 27 Jan 2023 | 2 years ago
Partial capture of text on file.
         Lesson 2: Lambda Calculus
                                                    Lesson2
                                          Lambda Calculus Basics
                                                     1/10/02
                                                Chapter 5.1, 5.2
                              Outline
                              • Syntax of the lambda calculus
                                 – abstraction over variables
                              • Operational semantics
                                 – beta reduction
                                 – substitution
                              • Programming in the lambda calculus
                                 – representation tricks
                              1/10/02              Lesson 2: Lambda Calculus         2
                                                                                                          1
         Lesson 2: Lambda Calculus
                              Basic ideas
                              • introduce variables ranging over values
                              • define functions by (lambda-) abstracting
                                 over variables
                              • apply functions to values
                                     x + 1
                                     lx. x + 1
                                     (lx. x + 1) 2
                              1/10/02               Lesson 2: Lambda Calculus          3
                              Abstract syntax
                                 Pure lambda calculus: start with nothing
                                   but variables.
                                 Lambda terms
                                 t ::=
                                       x             variable
                                       lx . t        abstraction
                                      t t            application 
                              1/10/02               Lesson 2: Lambda Calculus          4
                                                                                                            2
         Lesson 2: Lambda Calculus
                              Scope, free and bound occurences
                                lx . t        body
                                  binder
                                 Occurences of x in the body t are bound.
                                 Nonbound variable occurrences are called free.
                                    (lx . ly. zx(yx))x
                              1/10/02              Lesson 2: Lambda Calculus         5
                              Beta reduction
                                Computation in the lambda calculus takes the form of beta-
                                reduction:
                                     (lx. t1) t2 Æ [x ! t2]t1
                                where [x ! t2]t1 denotes the result of substituting t2 for all
                                free occurrences of x in t1.
                                A term of the form (lx. t1) t2 is called a beta-redex (or b-
                                redex).
                                A (beta) normal form is a term containing no beta-redexes.
                              1/10/02              Lesson 2: Lambda Calculus         6
                                                                                                          3
         Lesson 2: Lambda Calculus
                               Beta reduction: Examples
                                (lx.ly.y x)(lz.u) Æ ly.y(lz.u)
                                (lx. x x)(lz.u) Æ (lz.u) (lz.u)
                                (ly.y a)((lx. x)(lz.(lu.u) z)) Æ (ly.y a)(lz.(lu.u) z)
                                (ly.y a)((lx. x)(lz.(lu.u) z)) Æ (ly.y a)((lx. x)(lz. z))
                                (ly.y a)((lx. x)(lz.(lu.u) z)) Æ ((lx. x)(lz.(lu.u) z)) a
                               1/10/02              Lesson 2: Lambda Calculus           7
                               Evaluation strategies
                               • Full beta-reduction
                                  – any beta-redex can be reduced
                               • Normal order
                                  – reduce the leftmost-outermost redex
                               • Call by name
                                  – reduce the leftmost-outermost redex, but not inside
                                    abstractions
                                  – abstractions are normal forms
                               • Call by value
                                  – reduce leftmost-outermost redex where argument is a value
                                  – no reduction inside abstractions (abstractions are values)
                               1/10/02              Lesson 2: Lambda Calculus           8
                                                                                                             4
The words contained in this file might help you see if this file matches what you are looking for:

...Lesson lambda calculus basics chapter outline syntax of the abstraction over variables operational semantics beta reduction substitution programming in representation tricks basic ideas introduce ranging values define functions by abstracting apply to x lx abstract pure start with nothing but terms t variable application scope free and bound occurences body binder are nonbound occurrences called ly zx yx computation takes form where denotes result substituting for all a term is redex or b normal containing no redexes examples y lz u lu z evaluation strategies full any can be reduced order reduce leftmost outermost call name not inside abstractions forms value argument...

no reviews yet
Please Login to review.