Transcription
Introduction to Lambda-CalculusBy John Lång, 20 February 2020
“Yön maku,kun linnut syöksyy mustina siipinä tähtiä päin;vaan mikä on nimesi nimi,tähtesi salainen luku ja numero?”– Arcana by CMX, from their album Discopolis2 / 252
An Appetizer: The MIU-System Douglas Hofstadter presented the following puzzle in his famousbook “Gödel, Escher, Bach: an Eternal Golden Braid”: The MIU-system has the letters M, I, and U in its alphabet It has four production rules:1) αI αIU;3) αIIIβ αUβ; and 2) Mα Mαα;4) αUUβ αβ;The question is: Is MU derivable from MI?3 / 252
Subway MapsophStyri ngsanRdenλamterminRgsedVaucri ainblgesdeλteBrmrui oTyrypeLosgicFurtherToConpiclus csionThis slide was inspired by the West Metro, that connects Espooand Helsinki (most of the time). The stops are the conceptsworth learning. Page number is written beneath the stopsPhilo 5305475951041251491601762172474 / 252
Map of the UniverseMathematicsWe are hereComputerScience5 / 252
What Is a Function?FormulaInterpretation f(x) 2x f(x) yields 2x g(x,y) 5 g is a constant function h : X Y h maps every X to a Y x 3 x is mapped to 3 (a b)(x) a(b(x)) composition of a and b6 / 252
First-Order vs. Higher-OrderFirst-OrderA BfHigher-OrderCA(a1, b1)(a1, b2)(a1, b3) c1c2c3 f {((a1,b1),c1), ((a1,b2),c2), .}A Bf 1BfCBCB BfϵCf ϵ f 1B7 / 252
First-Order vs. Higher-OrderFirst-OrderA BfHigher-OrderCA(a1, b1)(a1, b2)(a1, b3) c1c2c3 f {((a1,b1),c1), ((a1,b2),c2), .}A Bf 1BfCBCB BfϵCf ϵ f 1B8 / 252
Extensional vs. IntensionalExtensionalIntensionalx yyf(x)GCD(x,y)falsex 0truex(x,y) (y%x,x)return y9 / 252
Extensional vs. IntensionalExtensionalIntensionalx yyf(x)GCD(x,y)falsex 0truex(x,y) (y%x,x)return y10 / 252
My Point of View According to Wiktionary (viewed some time in 2017):–The word “function” comes from a Latin word that meansperformance or execution–The Latin word “calculus” means “a pebble or stone used for counting”Does set theoretical mathematics do justice to these concepts?– Do you see pebbles in the real line?I think of functions as a primitive rather than a derived notion11 / 252
Some Terminology Functions are abstract dependencies between objectsAlgorithms are representations of functions in a formal system.Several algorithms per function; one function per algorithm Strings can represent functions as well as their arguments Computation is the art of algorithmic string manipulation A model of computation is a formal system that defineseffectively computable functions in terms of algorithms12 / 252
Some Models of ComputationIndustrial Cellular AutomataCombinatory LogicFlow ChartsFRACTRANLambda-CalculusMu Recursive FunctionsPeano ArithmeticPetri NetsPost Canonical SystemsTuring MachinesType TheoryUnlimited Register FPAPNPCSTMTTURMTTComplexLegend:CAFTAcademic13 / 252
Some Models of ComputationIndustrial Cellular AutomataCombinatory LogicFlow ChartsFRACTRANLambda-CalculusMu Recursive FunctionsPeano ArithmeticPetri NetsPost Canonical SystemsTuring MachinesType TheoryUnlimited Register FPAPNPCSTMTTURMTTComplexLegend:CAFTAcademic14 / 252
The Computational Universe Lambda-Calculus, Combinatory Logic, Mu Recursive Functions,Turing Machines, and others, represent the strongest class ofmodels of computation. (Church-Turing Thesis)They’re powerful enough to feature undecidability, i.e. theincompleteness of computational universe. (Thanks, Gödel!)–There are strange loops between object and meta languages–On the bright side, we can extend every formal system infinitely!–We’ll see later how undecidability emerges in LC15 / 252
Lambda-Calculus? Lambda-Calculus (LC) is the model (or language) of computation(i.e. programming) discussed in this presentation.– It is a system that expresses functions as strings of symbolsA few common misconceptions need to be addressed:–It’s lambda (the Greek letter Λ, λ), not “lambada” (the dance)–“Calculus” referes to proof calculus, not the differential/integral one–“Barendregt convention” was actually initiated by Thomas Ottmann–“Curry transformation” was actually discovered by Gottlob Frege16 / 252
The Rough Idea Lambda-Calculus is about anonymous functions, called lambdaexpressions (λ-exprs)There are conversion and reduction rules that allow us to reasonabout (in)equality of λ-exprs. Reducing λ-exprs is like–running a computer program;–performing a series of algebraic simplifications; or–transforming graphsWe’ll see how this works in due time17 / 252
Teaser: Building Functions f(x) 2x c translates into f λx. ((λt. 2 t)x) c in LC–2x can be seen as a function of t, t 2 t, applied to x–In LC, we write 2 t in prefix notation as 2 t–c is constant (or free variable); it stays fixed as x varies–We bind x as the formal parameter: λx. ((λt. 2 t)x) c (λt. 2 t)x means evaluating t ( 2 t) with the argument x We can simplify: f λx. ((λt. 2 t)x) c λx. ( 2 x) c18 / 252
The Black Box Analogy Revisited Traditionally, functions areseen as black boxesinput1 In LC, functions are the starsof the ut319 / 252
The Black Box Analogy Revisited Traditionally, functions areseen as black boxesinput1 In LC, functions are the starsof the ut320 / 252
Two Programming Paradigms Imperative paradigm operatesalgorithms like cookingrecipes, on step-by-step , KBDR2, 1R1, 6R2, R1R1, 12R2, CRTR0, HALT Declarative paradigm definesalgorithms as compositions ofcomputational primitives:select name, emailfrom students join staffwhere email like ’%.fi’ LC is declarativeLC doesn’t have implicit stateor side effects21 / 252
Two Programming Paradigms Imperative paradigm operatesalgorithms like cookingrecipes, on step-by-step , KBDR2, 1R1, 6R2, R1R1, 12R2, CRTR0, HALT Declarative paradigm definesalgorithms as compositions ofcomputational primitives:select name, emailfrom students join staffwhere email like ’%.fi’ LC is declarativeLC doesn’t have implicit stateor side effects22 / 252
Side-Effects Make Program Analysis Hard A “function” in C:int c 0;int f(int i){return i c ;}f(3); // Returns 3f(3); // Returns 4 Thus,f(3) f(3)!23 / 252
Lambda-Calculus Makes Effects Explicit A “function” in C: int c 0;int f(int i){return i c ;}f(3); // Returns 3f(3); // Returns 4 The state of In pseudo-LC, we’d declareThus,f(3) Consider the following:int g(int c, int i){return i (c 1);}int h(int i) {return g(0);}cis now explicitint g(int c)(int i);int h(int i){return g(0)(i);}f(3)! Now,h(3) h(3)24 / 252
Traditional Notation is Imprecise Take “f(x) y” for instance–What does ‘ ’ mean?–Definition or assertion?–Did we apply f to x?–Perhaps we multiplied f by x?–Do we need the graph of f ?Is ‘ ’ in (f g) a function?25 / 252
Lambda-Calculus is Unambiguous Take “f(x) y” for instance–What does ‘ ’ mean?–Definition or assertion?–Did we apply f to x?–– Perhaps we multiplied f by x?Do we need the graph of f ?Is ‘ ’ in (f g) a function? In LC, f(x) y means“f applied to x equals y”–It is an assertion (“ ”), not adefinition (“ ”)–No other interpretations–‘ ’ always has a direct proof is just another function:– f g (λvwx.v(wx))fg26 / 252
Why Lambda-Calculus? Lambda-Calculus is capable of describing computable functionsusing a referentially transparent (i.e. compositional) language LC has an unambiguous syntax with very few special cases The computer of LC doesn’t need soul, intuition, or magic LC doesn’t burden us with boring and error-prone technicaldetails, such as memory management or instruction sequencingLC gives the best of both mathematics and computer science27 / 252
My Very Small World vinspireitedrAlgebra28 / 252
sophStyri ngsanRdenλamterminRgsedVaucri ainblgesdeλteBrmrui oTyrypeLosgicFurtherToConpiclus csion PhiloSubway MapYou’re probably very eager to get started already, so let’s get tobusiness!53054759510412514916017621724729 / 252
Before We Start Our object language is the language of lambda expressions– Our meta language (e.g. set/category/topos/type theory, etc.)defines rules for working with lambda expressions– Words in the object language consist of variable and other symbolsCapital Latin letters (i.e. meta variables), indices, substitutionnotation, and various relational symbols belong to this languageDon’t get confused with object and meta languages!30 / 252
Strings Strings are (finite) ordered sequences of symbols, i.e. objects–For example, “a string” is a string (of the English alphabet)–Quotation marks separate object and meta languages. They may (andusually will) be omitted, when there’s no risk of ambiguityWe refer to strings by identifying them with meta variables.–‘V “value”’ tells that we denote the string “value” with V;–‘V W’ declares that V is a shorthand for W; and–A meta variable is interchangeable with the string it denotes31 / 252
String Length and Equality The length of a string V, written as V , is the number of(possibly repeated) symbols in it– For example, “” 0, “x” 1, “xx” 2, “string” 6Strings V and W, are equal, written as V W, if and only if V W and they contain the same symbols in the same order–For example, “cat” “cat”, but “cat” “tac” and “cat” “catch”–String equality is reflexive, symmetric, and transitive32 / 252
String Catenation V W or VW is a string, called (con)catenation of V and W. Itcontains every symbol of first V, then W.– E.g. “bat” “man” “batman”, but “bat” “man” “man” “bat”For every string U, V, and W:1) “” U U “” U(“” is the neutral element of )2) (U V) W U (V W)( is associative)Catenation also satisfies the equation U V U V 33 / 252
Substrings V is a substring of W if and only if V W and V containsthe same symbols as W in the same order, until the end of VFor instance,–V and W (and their substrings) are substrings of VW;–“tba” is a substring of “cat” “bat”, but not of “cat” or “bat”–“at” and “cat” are substrings of “cat”; “Cat” is not a substringof “cat” (as “C” “c”)34 / 252
Alphabet of Lambda-Calculus The objects of study in LC are (non-empty) strings known aslambda expressions (λ-exprs, a.k.a. lambda terms). Theiralphabet contains:1) ‘λ’(lambda)2) ‘.’(dot)3) ‘(’(left parenthesis)4) ‘)’(right parenthesis)5) x0, x1, x2, (variable symbols)35 / 252
First Definition: Induction Let x be a variable symbol and M, N (meta!) λ-exprs. Then:1) xis a lambda expression (called variable);2) (λx.M)is a lambda expression (called abstraction);3) (MN)is a lambda expression (called application); and4) nothing elseis a lambda expression.The definitions above may be applied recursively; e.g. since x isa λ-expr, (xx), (λx.(xx)), ((λx.(xx))(xx)), etc. are also λ-exprs36 / 252
Second Definition: BNF Alternatively, we can use Backus-Naur Form (BNF). Let λ-expr λ-var λ-abstr λ-app :: :: :: :: λ-var λ-abstr λ-app “(” λ-symbol “)”“(λ” λ-symbol “.” λ-expr “)”“(” λ-expr λ-expr “)”where λ-symbol can be replaced with an appropriate variablesymbol from the alphabet We can construct every (finitary) λ-expr be applying theseproduction rules finitely many times37 / 252
Third Definition: Deduction Rules Yet another way to definelambda expressions is to useformation rulesx : λ-expr(var)A string of symbols is a λexpr iff it can be derivedusing the rules on the rightx : λ-exprM : λ-exprλx.M : λ-expr(abs)Rules are useful, aren’t they?M : λ-exprN : λ-exprMN : λ-expr(app)38 / 252
Fourth Definition: Parse TreesExpressionVariable yM Abstractionλx.MApplication MNλxM MNSubexpressionsare below thebigger expressionsColours identifyvariablesTrees can benestedMore on parsetrees shortly39 / 252
Syntactic Sugar It shall be declared that:1) Outermost parentheses may be omitted;2) abstraction binds as far to the right as possible;3) MNO (MN)O, so application is left-associative;4) λx.λy.M λx.(λy.M), so abstraction is right-associative; and5) λxy.M λx.λy.M (in general, λx0x1x2.xn.M λx0.λx1.λx2.λxn.M). For example, (λx.x)y is different from λx.xy (i.e. λx.(xy))40 / 252
Subexpressions A subexpression (or subterm) N of a λ-expr M is1) a substring of M; such that2) N is a λ-expr in its own right; and3) M can be formed from N using the syntax rules of LC. For example:–x is a subexpression of itself, (λx.x), and (xy); and–λw or (λx.z) are not subexpressions of x, (xy), or (z(λx.y)wv).41 / 252
A Corner Case Consider λxz.xz. One might think that it has λxz.x or λz.x as asubexpression.But it doesn’t! Let’s unroll the syntactic sugar:λxz.xz λx.λz.xz λx.(λz.(xz)) The subexpressions of λxz.xz are λxz.xz, λz.xz, xz, x, and z The lesson: The definition applies to de-sugared expressions42 / 252
Did You Get The Syntax?Are the following strings are λ-exprs? x)(λx.x)–c–(c)43 / 252
Did You Get The Syntax?Are the following strings are λ-exprs? (Why?)–λxNo. The expression after “λx” is missing–(λx.xNo. The right parenthesis is missing–zx(λx.y)Yes.–λxy.zYes. Stands for (λx.λy.z)–(λx.x)(λx.x)Yes, it’s (λx.x) applied to itself–cOf course! (A variable expression)–(c)Yes, it’s the same as c above44 / 252
Are These Expressions Identical? Are the following pairs of lambda expressions y.x)z andλx.λy.xz–λwx.(λy.z) andλwxy.z–λxy.zandλx.yz45 / 252
Are These Expressions Identical? Are the following pairs of lambda expressions identical?–(x)andxYes. Outer parentheses omitted–z(λx.y)and(λx.y)zNo, there’s no commutativity–x(λx.y)zand(x)((λx.y)z)No. Application is left-associative–wx(yz)and(wx)(yz)Yes. Application is left-associative–λx.(λy.x)z andλx.λy.xzNo. (λy.x)z λy.xz–λwx.(λy.z) andλwxy.zYes–λxy.zλx.yzNo. λxy.z λx.λy.z λx.yzand46 / 252
Tree Analogy Lambda expressions can becombined into largerexpressions, using the syntaxrules given in p. 35λx.λy.λz.(xz)(yz)λxλyThe structure of a lambdaexpression can be visualizedwith a parse tree (or abstractsyntax tree) (see p. 39)λzxzyz47 / 252
Side Note: Proof z)(yz)48 / 252
The Other CalculusD(3x²-x 5) Here’s another tree analogy,representing the process offinding the derivative of apolynomial functionNotice how structural it isNo need to think aboutpoints or limitsD(3x²-x)D(5)D(3x²)D(-x)3D(x²)-D(x)D(x²)3 2x (-1) D(x)1 049 / 252
The Syntax of LC Lacks Symmetry Remember, that –(MN)K M(NK)–MN NM (unless M N)–(λx.x)y λx.(xy)No general associativity,commutativity, ordistributivity in LC!λx.(MN)xCf. function composition:–Usually, (x²) ( x)²–hence, ² ² λxxMNλx.M(Nx) λxMNx50 / 252
String Equality is Very Limiting Consider parse trees forw(λyz.x(yz)) and u(λgx.f(gx))They’re essentially the sametree, with different labelsWe’ll want to focus on theirstructure instead of ) xuλgλxfyzgx51 / 252
From Lambdas to Calculus So far, we are only familiar with strings and lambda expressions.We don’t have the “Calculus” part yetThe idea in LC is to show that the dynamical behaviour offunctions can be expressed in terms of a static languageAt this point, the only notion of equivalence between lambdaexpressions we have, is string equality (up to sugaring)In order to construct a more useful notion of equality, we’regoing to need more definitions.52 / 252
Subway MapsophStyri ngsanRdenλamterminRgsedVaucri ainblgesdeλteBrmrui oTyrypeLosgicFurtherToConpiclus csionNow that we understand the basic structure of λ-exprs, it’s timeto start building the machinery that we’ll need for meta theory.First, we need free/bound variables, renaming, and substitutionPhilo 53054759510412414916017621724753 / 252
Free, Binding, And Bound Variables There are free, binding, and bound variables. Intuitively:–Bound variables occur as free variables in subexpressions of lambdaabstractions. For example, x is bound in λx.xx but not in λy.x–Binding variables are prefixed with lambdas, like x in λx.y–Free variables are variables not bound, such as x in zxy or (λy.y)x–The subexpressions of applications are handled recursivelyA variable can be both free and bound, or neither–For example, x in x(λx.x) is free, binding and bound54 / 252
Free and Bound Variables, Formal Definition The free variables in a λ-expr, using the language of sets:1) free(x) {x}2) free(λx.M) free(M) \ {x}3) free(MN) free(M) free(N)The bound variables, on the other hand, can be defined as:1) bound(x) {} (i.e. Ø)2) bound(λx.M) bound(M) {x}3) bound(MN) bound(M) bound(N)55 / 252
Example on Free Variablesfree(λy.(λx.zy)w) free((λx.zy)w) \ {y} (free(λx.zy) free(w)) \ {y} ((free(zy) \ {x}) {w}) \ {y} (((free(z) free(y)) \ {x}) {w}) \ {y} ((({z} {y}) \ {x}) {w}) \ {y} (({z, y} \ {x}) {w}) \ {y} ({z, y} {w}) \ {y} {z, y, w} \ {y} {z, w}.56 / 252
Real World Examples on Variable Binding Consider the following examples:– x.( x) ( y.(y x {y,{y}} x))–z (Σk ℕ\{0}6k ²) z π²–int f(int i) {return i c ;}Variables x, y, k, andiare bound. They are parametersVariables z, π, and c are not bound. Their meaning depends onthe context in which they are interpreted in57 / 252
Free and Bound Variables QuizWhich variables in the following expressions arefree/bound/both/neither (in outermost x)–λx.λy.xy–λx.x(λy.y)–x(λy.y)yz58 / 252
Free and Bound Variables QuizWhich variables in the following expressions arefree/bound/both/neither (in outermost context)?–λx.xx is bound and not free. Easy, wasn’t it?–λx.xxx is bound, not free. (y is neither free nor bound)–λx.xyx is bound, not free. y is free and not bound–(λx.y)(λy.x)Both x and y have free and bound occurences–λx.λy.xyBoth x and y are bound and not free–λx.x(λy.y)Both x and y are bound and not free–x(λy.y)yzx and z are only free. y is both free and bound59 / 252
Renaming Variables Let M be a λ-expr and y be a variable symbol. Then,1) x{x y} y2) z{x y} z3) (λx.N){x y} λx.N4) (λz.N){x y} λx.(N{x y})5) (NO){x y} (N{x y})(O{x y})(with z x)(with z x)For example, (λz.xy(λx.x)(λy.x)z){x y} λz.yy(λx.x)(λy.y)z60 / 252
Renaming FlowchartM{x y}return (N{x y})(O{x y})M NOfalseM xtruereturn yfalseM ztruereturn zfalseM λx.Ntruereturn λx.NfalseM λz.Ntruereturn λz.(N{x y})61 / 252
Renaming Quiz Are the following assertions correct or not?–(λx.x){x y} λy.y–(λy.x){x y} λy.y–(λy.y){x y} λy.y–(λxy.z){x y} λxy.y–(λxx.x){x y} λxy.y–(λxy.x){x y} λxy.y62 / 252
Renaming Quiz Are the following assertions correct or not?–(λx.x){x y} λy.yNo. x is bound.–(λy.x){x y} λy.yYes. x is free.–(λy.y){x y} λy.yYes. x does not occur in λy.y.–(λxy.z){x y} λxy.yNo. z is not being renamed.–(λxx.x){x y} λxy.yNo. x is bound by the inner λ.–(λxy.x){x y} λxy.yNo. x is bound by the outer λ.63 / 252
Alpha Congruence A λ-expr M λx.N is alpha congruent/convertible withM' λy.N{x y}, if and only if y does not occur (at all) in N–The assertion of alpha congruence is denoted with M α M'–We also consider expressions having congruent subexpressions to becongruent, i.e. if M α M', then αMβ α αM'β (α or β may be “”)Following the custom in LC, we focus on λ-exprs modulo alphacongruence (i.e. as representatives of equivalence classes of α),meaning that if M α N, then we usually write just M N64 / 252
Can You Convert These? Are the following pairs of expressions alpha congruent?–λx.xand λy.y–λx.xand λx.y–λx.xand λy.x–λxy.xand λyx.x–λxy.xand λyx.y–λxy.xy and λzy.zy–λxy.xy and λyx.yx65 / 252
Can You Convert These? Are the following pairs of expressions alpha congruent?–λx.xand λy.yYes. λx.x α λy.x[x y] α λy.y–λx.xand λx.yNo. Different variable bindings–λx.xand λy.xNo. Different variable bindings–λxy.xand λyx.xNo. λxy.x λx.λy.x λy.λx.x λyx.x–λxy.xand λyx.yYes. λxy.x λzy.z λzx.z λy.xy–λxy.xy and λzy.zyYes. λxy.xy λx.λy.xy λz.λy.zy λzy.zy–λxy.xy and λyx.yxYes. λxy.xy λxz.xz λyz.yz λyx.yx66 / 252
Substitution of Expressions M[x N] denotes “M with all free occurrences of x replaced withN, after renaming bound variables of M if necessary”The formal definition of substitution is technical. Intuitively:1) free variables must remain free;2) bound variables must remain bound;3) same variables must remain same; and4) different variables must remain different.67 / 252
Perils of Careless Substitution Substitution is surprisingly non-trivial business because variablecapture needs to be avoidedVariable capture is a violation of the rules on the previous slide– Note that y captured x on p. 60! That’s why we have the extracondition on p. 67 demanding that we always pick fresh variablesFor example, if (λx.y)[x y] yielded λy.y, the free variable ywould become bound. (Thus, it gives λx.y back unchanged)–Other examples include (λx.y)[y x], (λx.yz)[x z], and (λx.yz)[y z]68 / 252
How to Avoid Variable Capture Wrong (λx.xyz)[z x]:–Naïve substitutionλx.xyzλxzx y Correct (λx.xyz)[z x]:–Rename x; Then substituteλx.xyxλx.xyzλxλxxxyzxyλw.wyx λwxwy69 / 252
Formal Definition of Substitution Formally, we define M[x N] by cases on M:1a) x[x N] N1b) y[x N] y(if y x, o/w case 1a applies)2) (λx.O)[x N] λx.O(x isn’t free in λx.O)3a) (λy.O)[x N] λy.O[x N](if x free(O) or x free(N))3b) (λy.O)[x N] λz.(O[y z])[x N] (with z being fresh)4) (OP)[x N] O[x N]P[x N](recursive case)70 / 252
Substitution FlowchartM[x N]return (O[x N])(P[x N])return λx.O[x N]false, M OPfalseM ytruey xtruereturn NM λy.Oreturn yfalsefalsetruetruey xfalsetruereturn λx.Ofree(x,O)free(x,N)falsetruereturn λz.(O[y z])[x N]71 / 252
Substitution QuizWhat is the result of these substitutions? (Why?)–y[x y]–x[x y]–(xy)[x y]–(λy.x)[x y]–(λy.y)[x y]–(λy.x)[x (λz.z)]–(λy.x)[x (λx.x)]72 / 252
Substitution QuizWhat is the result of these substitutions? (Why?)–y[x y]y. There’s no x to be replaced–x[x y]y. This is a basic substitution–(xy)[x y]xy. Otherwise, y would capture x–(λy.x)[x y]λz.y. The bound variable was renamed–(λy.y)[x y]λy.y. No x present–(λy.x)[x (λz.z)]λy.λz.z–(λy.x)[x (λx.x)]λy.λx.x. x is not free in λx.x73 / 252
Subway MapsophStyri ngsanRdenλamterminRgsedVaucri ainblgesdeλteBrmrui oTyrypeLosgicFurtherToConpiclus csionNow that we’ve endured most of the gory technical details, wecan take the next step towards defining equality of λ-exprs.Equality is one of the most interesting questions in LC and TTPhilo 53054759510412414916017621724774 / 252
Beta Reducible Expressions From now on, were going to be naïve. We will only work withexpressions for which substitution works easilyA lambda expression is beta reducible expression (β-redex) if(and only if) it’s of the following form:– (λx.M)N (where x is a variable symbol and M, N are λ-expr)A λ-expr is in β-Normal Form (β-NF) if and only if it doesn’tcontain any β-redexes.75 / 252
Beta Reduction Let M (λx.N)O and M' N[x O] be expressions. The rule of(beta) reduction says that:–redex M reduces to reduct M'. This is denoted with M M'–We also say that αMβ reduces to αM'β. (α or β can be empty.)This means, that the computer has to:–Take (λx.N)O(A β-reducible expression)–Give [x O]N(Drop “λx.”; Substitute free ‘x’s with Os)76 / 252
Reduction Flowchart (Single Step)return reduce Oreduce MfalseM xtruereturn xfalseM (λx.N)Ofalsetruereturn N[x O]M λx.Nfalse, M NOtruereturn reduce Nredexesin N?truereturn reduce N77 / 252
The Fun Is About to Begin Performing a single step of reduction is like performing onearithmetic operation, or one step of logical inference.– Usually, we need many steps to fully reduce long expressionsReducing complex expressions comes down to repeatedlyapplying beta reduction until a β-NF is reachedIf M reduces to N in zero or more steps, we write M N.–( is the transitive-reflexive closure of )78 / 252
Graph(ical) Example(λx.λy.x)(λz.z)MNNleftmost xλz.zredex79 / 252
Graph(ical) Example (λx.λy.x)(λz.z)MN“λx.” was removed andλz.z replaced x.In programming jargon,the formal parameter xwas evaluated with theactual parameter λz.z.NλyMλzzformer variable x80 / 252
Graph(ical) Example Next, “λy.” was removed.Because y wax not freein the subexpressionλz.z, the applicand Mwas thrown away duringthe reduction process.(λx.λy.x)(λz.z)MNλzNzOne more step to go.81 / 252
Graph(ical) Example So, (λx.λy.x)(λz.z)MN N.The result didn’t depend onM or N in any way, becauseLC is f. the C languageexample in p. 22–23.82 / 252
Formal Example Let’s consider M (λvw.v)xy. It holds that M x:M (λvw.v)xy((λv.λw.v)x)y((λw.v)[v x])y(λw.x)yx[w y]xThus, M x (in two steps).83 / 252
Numerical Example Intuitively, we know what‘ ’, ‘ ’, ‘ ’, ‘2’, ‘3’, ‘5’, ‘7’,“10”, “35”, “32”, and “42” are.We’ll learn how to definethese things in a way thatmakes even machines ableoperate on them.–The trick is called recursion.(λx.λy.2 x x y 3) 5 7 (λy.2 5 5 y 3) 7 (λy.10 5 y 3) 7 10 5 7 3 10 35 3 10 32 4284 / 252
More graphs The graph to the right showsall the possible reducts of oneparticular λ-expr.Note that every path ends tothe same normal form (λv.v).–This is not a coincidence!–(It follows from the ChurchRosser �z.v))λv.v85 / 252
Algebraic Analogy(1 2) (3 4)1 (3 4) 2 (3 4)3 4 2 (3 4)1 ( 1) 2 (3 4)3 (3 4)1 (3 4) 2 ( 1)1 (3 4) 6 8(3 4) 6 8 1 ( 1) 6 8(1 2) ( 1)(1 2) 3 (1 2) 43 ( 1)1 (3 4) 2 386 / 252
Reduction Quiz, Part I1) The β-NF of (λx.xx)y is.2) The β-NF of w(λx.xz)y is.a) xxa) the expression itselfb) yyb) wyzc) neitherc) wzy87 / 252
Reduction Quiz, Part I1) The β-NF of (λx.xx)y is.2) The β-NF of w(λx.xz)y is.a) xxa) the expression itselfb) yyb) wyzc) neitherc) wzyBy definition,(λx.xx)y xx[x y] yy,so we throw away “λx.” andsubstitute both xs with y.w(λx.xz)y (w(λx.xz))y, so λx.xzcannot be applied to y. On theother hand, w is just a variable.Thus, the expression is in β-NF.88 / 252
Reduction Quiz, Part II3) What is the β-NF of(λw.w)(λx.z)(((λx.x)y)(λx.xz)yw)?4) The β-NF of v(λx.z) is.a) the expression itselfa) (λw.w)zb) zb) (λx.z)(((λx.x)y)(λx.xz)yw)c) neitherc) neither89 / 252
Reduction Quiz, Part II3) What is the β-NF of(λw.w)(λx.z)(((λx.x)y)(λx.xz)yw)?4) The β-NF of v(λx.z) is.a) the expression itselfa) (λw.w)zb) zb) (λx.z)(((λx.x)y)(λx.xz)yw)c) neitherc) neitherThe first two functions from theleft are identity and a constantfunction, so we get z in 2 steps.v(λx.z) is in normal form, so itcannot be reduced to anythingelse. N.B. (b) is wrong, becausethe operations don’t commute.90 / 252
Reduction Quiz, Part III5) The β-NF of w(x(λy.wz)) is.6) The β-NF of (λx.xx)(λx.xx) is.a) w(x(λx.wz))a) the expression itselfb) w(x(λw.wz))b) (λx.xx)c) w(x(λz.wz))c) neither91 / 252
Reduction Quiz, Part III5) The β-NF of w(x(λy.wz)) is.6) The β-NF of (λx.xx)(λx.xx) is.a) w(x(λx.wz))a) the expression itselfb) w(x(λw.wz))b) (λx.xx)c) w(x(λz.wz))c) neitherw(x(λy.wz)) α w(x(λx.wz)), sowe consider them identical.There’s no variable capture,since x, y are not free in wz.(λx.xx)(λx.xx) (λx.xx)(λx.xx).Uh, oh! This expression reducesitself, so it’s a β-redex thatcannot be reduced!92 / 252
A Quick Recapitulation Let’s have a short recap on the (meta) notation:defines a meta variable V that refers to W;–V W–V “wzq” defines V to be a reference to the string literal “wzq”;–M[x N]the λ-expr obtained from M by substituting x with N;–M Nasserts that M and N refer to (alpha) congruent λ-exprs;–M Nasserts that M reduces to N in single step; and–M Nasserts that M reduces to N in any number of steps.93 / 252
Subway MapsophStyri ngsanRdenλamterminRgsedVaucri ainblgesdeλteBrmrui oTyrypeLosgicFurtherToConpiclus csionWe have seen that β-reduction, though simple on the surface,contains some complexity in the underlying machinery. We’llhave a look at an arguably simpler alternative notation nextPhilo 53054759510412514916017621724794 / 252
Alternative notations We’ve seen that named free and bound variables lead into someuncomfortable technicalitiesThere are two alternatives to the ordinary LC notation thatbypass some of these challenges, namely Combinatory Logic(CL) and de Bruijn Indexing–However, they come with their own limitations–We’ll discuss de Bruijn Indexing next95 / 252
de Bruijn Indexing de Bruijn Indexing (dB-exprs) is an alternative syntax to LC Let n be a natural number and M, N be dB-exprs. Then, 1) (n )is a dB-expr;2) (MN)is a dB-expr;3) (λM)is a dB-expr; and4) nothing elseis a dB-expr;We’ll apply syntactic sugar, e.g. λλ0 2 (λ(λ((0)(2))))96 / 252
Syntactical Correspondence The idea of de Bruijn Indexing is that the natural numbersrepresent bound variables by expressing their distance to thebinding lambda abstraction, with 0 meaning immediate binding– E.g. The λ-exprs λx
16 / 252 Lambda-Calculus? Lambda-Calculus (LC) is the model (or language) of computation (i.e. programming) discussed in this presentation. - It is a system that expresses functions as strings of symbols A few common misconceptions need to be addressed: - It's lambda (the Greek letter Λ, λ), not "lambada" (the dance) - "Calculus" referes to proof calculus, not the .
