V Introduction to Lambda Calculus
V Introduction and motivations
V The lambda calculus is a useful tool in Computer Science
* it constitutes the foundation for functional programming
* it is the meta-language of denotational semantics (the “best-bet” standard for specifying programming language semantics)
* it provides (one version of) a theory of computation (the more traditional version is via Turing Machines)
V Lambda calculus comes from logic and mathematics
* it provides a generalized notion of function (untyped, higher-order functions)
* it provides a generalization of algebraic and logical notations
* it can be used as a foundation for constructive mathematics
V What is lambda calculus?
* it is “the” formal theory of functions (i.e., it formalizes functions first, rather than encoding them in other terms, as in set theory)
* it is “just” a better (more direct) notation for functions
V How does lambda calculus differ from traditional mathematical treatments of functions?
* in traditional math, functions are always first-order and usually typed; in (pure) lambda calculus, functions are higher-order and untyped
V in set theory, functions are coded as their graphs (i.e., sets of pairs); in lambda calculus, functions are viewed operationally, in terms of rules or algorithms
* allows us to distinguish different algorithms and thus different running times, styles of expression, etc.
* allows us to connect to the functions via concrete language: this is how we define and use them, not just what they are
V Variations on lambda calculus
* the pure, untyped calculus (what we will study here)
* applied calculi with extra constants (e.g., for logic or arithmetic)
* combinatory logic: no bound variables ("points-free")
* deBruijn numbers: another way of eliminating variables
* typed calculi: a rich family of calculi which model typed programming languages, higher-order logics, etc.
V Syntax of the lambda calculus
V Notational conventions
* M, N, P, … range over lambda terms (the main syntactic category)
* x,y,z, … range over variable names; actual variables may be drawn from any (countably infinite) set of symbols
V Context-free grammar of expressions
* M ::= x | λx.M | M N
* the first form of term is just an occurrence of a variable
* the second form of term is called a lambda abstraction: its meaning is a function
* the variable in an abstraction is bound by the construct; the body term is the scope of the binding
* the third form is (function) application; the left part is called the operator, the right part the argument
V Abbreviations, precedence and other syntactic conveniences
V function application associates to the left
* M N P ≣ (M N) P ≢ M (N P)
V the scope of lambda extends as far as possible to the right (up to the end, or a closing parenthesis)
* λx.M N ≣ (λx.(M N)) ≢ (λx.M) N
V multiple successive abstractions are often abbreviated with a single lambda (if variables are multi-symbol, then use commas or spaces to separate)
* λxyz. M ≣ λx. (λy. (λz.M))
V Some sample terms
V the identity function
* (λx. x)
V a polynomial in x
* (λx. x^2 + 2x +3)
V the ‘constant-function producing function’ (Haskell's const)
* (λxy. x)
V function composition
* (λfgx. f (g x))
V the ‘twice’ function
* (λfx. f (f x))
V Lambda calculus as a direct means of defining functions
* lambda abstractions stand for (denote) functions directly, so that no separate mechanism for parametric definitions is needed
V normally, we define functions only indirectly, by way of application to a parameter
* f x = x+3
V we wouldn’t accept such an indirect definition if we were defining, say, negative numbers in terms of positive ones
* x+4 = 1
V we would prefer to define negative numbers directly, using a separate notation unique to them; this notation liberates our thinking and allows us to focus on the new concept
* x = -3
V similarly, lambda calculus allows us to define functions directly, and therefore to focus on them as separate entities
* f = (λx.x+3)
* here the lambda abstraction appearing on the right is a kind of inverse of function application, just as subtraction is a kind of inverse of addition
V Syntactic operations
V Some intuitions
V intuitively, bound variables can be changed without changing meaning
* (λx.x) = (λy.y) = the identity function
V intuitively, application substitutes the argument for the bound variable in the function's body
* (λx.x+3*x) 17 = 17+3*17
* although pure lambda calculus contains no constants (such as + or 3), these can be added to the language for more practical applications
V Notions of free and bound variables
V the bound variables of a term are those bound by some abstraction
* BV(x) = {}
* BV(λx.M) = {x}
* BV(M N) = BV(M) ∪ BV(N)
V the free variables of a term are those not bound by some abstraction
* FV(x) = {x}
* FV(λx.M) = FV(M) \ {x}
* FV(M N) = FV(M) ∪ FV(N)
V when substituting terms or variables for bound variables, we need to take some care to avoid confusing one bound variable for another
* (λxy.x) y = (λx.(λy.x)) y = (λy.x) [y/x] =? (λy.y)
V Substitution formally defined
* we define a formal notion of substitution which respects bound variables
* M [N/x]: the term M with the term N substituted for all free occurrences of x
* x [N/x] = N
* y [N/x] = y (for y≢x)
* (λx.M) [N/x] = λx.M
* (λy.M) [N/x] = λy. (M [N/x]) (for y≢x and if y∉FV(N))
* (λy.M) [N/x] = λz. ((M [z/y]) [N/x]) (for y≢x, y∈FV(N), z fresh)
* M P [N/x] = (M [N/x]) (P [N/x])
V Theory and operational semantics of the lambda calculus
V Basic notions of reduction
V Beta reduction
* (λx.M) N →β M [N/x]
V Eta reduction (or expansion)
* (λx.M x) →η M (when x∉FV(M))
V Alpha reduction (or equivalence)
* (λx. M) →α (λy. M[y/x])
V Delta reductions (for applied calculi)
* 2+3 →δ 5
* Of these various rules, alpha reduction is the most innocuous; we normally ignore it by considering terms modulo their “alpha-equivalence classes” and by adopting some convention to avoid any clash of variables
V Extended notion of reduction
* the basic notions of reduction determine relations on terms; we take the reflexive, transitive and compatible closure of these basic notions to get a (full) notion of reduction on terms (compatible closure just says that if a sub-term reduces, so does the term that contains it)
V Different reduction orders
* since reductions might apply to various sub-terms, there may be several ways in which we can reduce a given term; in fact, some might terminate whereas others might not
* (λxy.x) I Ω where Ω = (λx.xx) (λx.xx) and I = λx.x
V Normal form
* when a term can be reduced no more, we say it is in normal form
V some terms may have no normal form
* Ω = (λx.xx) (λx.xx)
* some terms without normal form may still yield information (e.g., a term representing the list of all digits of π)
V Equality on terms
* symmetric and transitive closure of reduction; gives us the primitive notion of equality on terms
* equality on terms is in general undecidable
V Church-Rosser theorem
* if two terms are equal, then they reduce to a common term
V Normal-order reduction
* if a term reduces in finitely-many steps to a normal form, then reducing by the strategy “left-most/outer-most first” will yield that normal form
V Expressive power of the lambda calculus
V We can encode all the usual mathematical and logical notions in terms of lambda calculus
* this is similar to the way in which these notions are encoded in pure set theory
* “pure” theories are good for theoretical studies; applied theories usually categorize entities by some kind of types
V Booleans
V we can encode True, False and if-then-else as follows:
* True ≣ λxy. x
* False ≣ λxy. y
V if M then N else P ≣ M N P
* i.e., if-then-else = λxyz. x y z
V Natural numbers
V we can encode a natural number n as the n-fold self-composition operator
* Zero ≣ λfx. x
* One ≣ λfx. f x
* n ≣ λfx. f (f … (f x) … ) (n occurrences of f)
V we can then encode addition, multiplication and exponentiation
* + ≣ λmnfx. m f (n f x)
* * ≣ λmnf. m (n f)
* ^ ≣ λmn. n m
V Pairing
V we can encode pairs and projection function as follows
* (M,N) ≣ λz. z M N
* fst ≣ λp. p True
* snd ≣ λp. p False
V Defining recursion
V we can define λ-terms which implement general recursion
* Y ≣ λf. (λx. f(x x)) (λx. f(x x))
* Y F = F(Y F)
* Θ ≣ (λxy. y(xxy)) (λxy. y(xxy))
* Θ F ↠ F(Θ F)
V we can define factorial this way
* fact = Y (λfn. if n=0 then 1 else n * f (n-1))
V Combinators
V Definition of a combinator
* a combinator is any closed lambda term ; i.e., a term without free variables
V Combinatory logic as a separate theory
* rather than defining combinators as certain lambda terms, we can devise a calculus with combinators alone
V in Combinatory Logic, each combinator has a rule which shows its behavior under reduction
* S f g x → f x (g x)
* K x y → x
* I x → x
V All terms with variables can be translated into combinatory terms which behave like lambda abstractions
* abs x (x) = I
* abs x (y) = K x (for y≢x)
* abs x (M N) = S (abs x M) (abs x N)
* the translation for lambda abstractions just substitutes abs x M for λx.M