jagomart
digital resources
picture1_Lambda Calculus Pdf 171753 | 02 Lambda


 141x       Filetype PDF       File size 0.24 MB       Source: is.muni.cz


File: Lambda Calculus Pdf 171753 | 02 Lambda
ia014 advanced functional programming 2 untyped lambda calculus jan obdralek obdrzalek muni cz faculty of informatics masaryk university brno ia014 2 untyped lambda calculus 1 formal development ia014 2 untyped ...

icon picture PDF Filetype PDF | Posted on 26 Jan 2023 | 2 years ago
Partial capture of text on file.
                        IA014: Advanced Functional
                                          Programming
                             2. Untyped Lambda Calculus
                            Jan Obdržálek                  obdrzalek@fi.muni.cz
                             Faculty of Informatics, Masaryk University, Brno
          IA014   2. Untyped Lambda Calculus                                                               1
                             Formal development
          IA014   2. Untyped Lambda Calculus                                                               2
                                                  Syntax
          Theset of λ-terms is defined by the following BNF grammar:
                              M::= x                                   variable
                                      |    MM′                         application
                                      |    λx.M                        abstraction
             • where x,y,z,... are variables from a countable set Var
             • weuseuppercaseletters M,N,... to denote λ-terms
             • (,) are used whenever the meaning is not clear
                                                   examples
                    I ≡ λx.x                     K≡λx.(λy.x)
                   ω≡λx.(xx)                      S≡λx.(λy.(λz.((x z)(y z))))
                                                 Ω≡ωω≡(λx.(xx))(λx.(xx))
          IA014   2. Untyped Lambda Calculus                                                               3
                                Syntactic conventions
             • λx x ...x .M means λx .(λx .(...(λx .M)...))
                     1 2         n                      1       2             n
             • M M M ...M means(...((M M )M )...)
                    1    2    3         n                          1    2     3
                 application associates to the left
             • λx.x y means λx.(x y)
                 function application takes precedence
             • spaces have no meaning
                                                   Examples
                                                               simplified
                      λx.(x y z)                                λx.x y z
                        (λx.x) y                                (λx.x) y
                       λx.(λy.x)                                  λxy.x
           λx.(λy.(λz.((x z) (y z)))                      λxyz.(x z) (y z)
          IA014   2. Untyped Lambda Calculus                                                               4
The words contained in this file might help you see if this file matches what you are looking for:

...Ia advanced functional programming untyped lambda calculus jan obdralek obdrzalek muni cz faculty of informatics masaryk university brno formal development syntax theset terms is dened by the following bnf grammar m x variable mm application abstraction where y z are variables from a countable set var weuseuppercaseletters n to denote used whenever meaning not clear examples i k xx s syntactic conventions means associates left function takes precedence spaces have no simplied xy xyz...

no reviews yet
Please Login to review.