

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 metalanguage of denotational semantics (the “bestbet” 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, higherorder 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 firstorder and usually typed; in (pure) lambda calculus, functions are higherorder 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 ("pointsfree")




deBruijn numbers: another way of eliminating variables




typed calculi: a rich family of calculi which model typed programming languages, higherorder 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




Contextfree 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 multisymbol, 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 ‘constantfunction 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 “alphaequivalence 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 subterm reduces, so does the term that contains it)




Different reduction orders




since reductions might apply to various subterms, 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




ChurchRosser theorem




if two terms are equal, then they reduce to a common term




Normalorder reduction




if a term reduces in finitelymany steps to a normal form, then reducing by the strategy “leftmost/outermost 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 ifthenelse as follows:




True ≣ λxy. x




False ≣ λxy. y




if M then N else P ≣ M N P




i.e., ifthenelse = λxyz. x y z




Natural numbers




we can encode a natural number n as the nfold selfcomposition 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 (n1))




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


