Topic
 Introduction to Lambda Calculus
 Introduction and motivations
 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)
 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
 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
 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
 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
 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.
 Syntax of the lambda calculus
 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
 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
 Abbreviations, precedence and other syntactic conveniences
 function application associates to the left
 M N P ≣ (M N) P ≢ M (N P)
 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
 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))
 Some sample terms
 the identity function
 (λx. x)
 a polynomial in x
 (λx. x^2 + 2x +3)
 the ‘constant-function producing function’ (Haskell's const)
 (λxy. x)
 function composition
 (λfgx. f (g x))
 the ‘twice’ function
 (λfx. f (f x))
 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
 normally, we define functions only indirectly, by way of application to a parameter
 f x = x+3
 we wouldn’t accept such an indirect definition if we were defining, say, negative numbers in terms of positive ones
 x+4 = 1
 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
 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
 Syntactic operations
 Some intuitions
 intuitively, bound variables can be changed without changing meaning
 (λx.x) = (λy.y) = the identity function
 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
 Notions of free and bound variables
 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)
 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)
 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)
 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])
 Theory and operational semantics of the lambda calculus
 Basic notions of reduction
 Beta reduction
 (λx.M) N →β M [N/x]
 Eta reduction (or expansion)
 (λx.M x) →η M (when x∉FV(M))
 Alpha reduction (or equivalence)
 (λx. M) →α (λy. M[y/x])
 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
 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)
 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
 Normal form
 when a term can be reduced no more, we say it is in normal form
 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 π)
 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
 Church-Rosser theorem
 if two terms are equal, then they reduce to a common term
 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
 Expressive power of the lambda calculus
 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
 Booleans
 we can encode True, False and if-then-else as follows:
 True ≣ λxy. x
 False ≣ λxy. y
 if M then N else P ≣ M N P
 i.e., if-then-else = λxyz. x y z
 Natural numbers
 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)
 we can then encode addition, multiplication and exponentiation
 + ≣ λmnfx. m f (n f x)
 * ≣ λmnf. m (n f)
 ^ ≣ λmn. n m
 Pairing
 we can encode pairs and projection function as follows
 (M,N) ≣ λz. z M N
 fst ≣ λp. p True
 snd ≣ λp. p False
 Defining recursion
 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)
 we can define factorial this way
 fact = Y (λfn. if n=0 then 1 else n * f (n-1))
 Combinators
 Definition of a combinator
 a combinator is any closed lambda term ; i.e., a term without free variables
 Combinatory logic as a separate theory
 rather than defining combinators as certain lambda terms, we can devise a calculus with combinators alone
 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
 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