This material is from
There
is not original and is not presented as such; the document is for my use; I
Anil Mitra may want to change that in the future. Note: I recognize that this
material is specialized and tailored to programming languages. CONTENTS Recursive definition of expressions Function application associates from the left LAMBDA CALCULUs ## There are two keywordsTo be defined: the keywords LAMBDA and DOT. λ (lambda) . (dot) ## Name or variableTo be defined: the NAME or VARIABLE (identifier) A ‘name’, also called a ‘variable’ is an identifier which can be any letter a, b, c, … ## Recursive definition of expressionsTo be defined: EXPRESSION, FUNCTION, and APPLICATION. <expression> := <name> | <function> | <application> <function> := λ <name>.<expression> <application> := <expression><expression> ## NoteIn a function, ‘λ <name>’ (before the dot) is called the head and the <expression> after the dot is the body. ## ParenthesesAn expression can be surrounded with parentheses for clarity: if E is an expression (E) is an expression. ## Function application associates from the leftThat is, E ## Functions do not have namesTo simplify notation capital letters, digits, and other symbols may be used as synonyms for some function definitions. ## Function evaluationHow do we evaluate functions? The term ‘evaluation’ comes from the terminology f(x) in which given an x, the function is evaluated according to the rule f. However, in the λ calculus functions do not have names. A function applied to an expression may be simplified by SUBSTITUTION (below). This is the only rule for ‘evaluation’ of functions in the λ calculus. From the recursive definition a single identifier (variable or name, e.g. x) is an expression. Therefore λx.x is an expression. ## SubstitutionIf a function (λ <name>.<expression ## Substitution ruleSUBSTITUTE <expression Or, substitute all instances of the name in the head expression by the expression to which the function is applied. ## Identity functionIf the function λx.x is applied to y, the result is λx.xy or (λx.x)y for clarity. From the substitution rule the function REDUCES to y. Therefore λx.x is (called) the IDENTITY function denoted by I which is a synonym for (λx.x). Applying the identity function two times: II = (λx.x) (λx.x) = (λx.x) (λy.y) = (λy.y) = I Note that the names of the arguments in function definitions are placeholders and do not have meaning by themselves: λx.x º λy.y º λz.z º λt.t … ## Free and bound variablesIn λ calculus all names are local to definitions. In the function λx.x we say that x is ‘bound’ since its occurrence in the body of the definition is preceded by λx. A name not preceded by a λ is called a ‘free variable’. In the expression (λx.xy) the variable x is bound and y is free. In the expression (λx.x)(λy.yx) the x in the body of the first expression from the left is bound to the first λ. The y in the body of the second expression is bound to the second λ and the x is free. It is very important to notice that the x in the second expression is totally independent of the x in the first expression. Formally we say that a variable <name> is free in an expression if one of the following three cases holds: § λ <name> is free in <name>. §
λ <name> is free in λ <name §
λ <name> is free in E A variable <name> is bound if one of two cases holds: §
λ <name> is bound in λ <name §
λ <name> is bound in E It should be emphasized that the same identifier can occur free and bound in the same expression. In the expression (λx.xy)(λy.y) the first y is free in the parenthesized sub expression to the left. It is bound in the sub expression to the right. It occurs therefore free as well as bound in the whole expression. ## More on substitutionIn (λx.(λy.xy))y The y in the inner parentheses is bound while the outer y is free. Therefore replacing x by y in the inner expression results in the incorrect result (λy.yy). To obtain the correct result rename the free y as t to get (λx.(λy.xy))t or (λy.ty) which is correct. However, since in the original expression y was free we might want it to be free in the final expression. So we would then replace the inner y by t to get (λx.(λt.xt))y or (λt.yt) which is also correct but may be more convenient. Therefore, if the function λx. <expression> is applied to E, we substitute all free occurrences of x in <expression> with E. If the substitution would bring a free variable of E in an expression where this variable occurs bound, we rename the bound variable before performing the substitution. For example, in the expression (λx.(λy.(x(λx.xy))))y we associate the argument x with y. In the body (λy.(x(λx.xy))) only the first x is free and can be substituted. Before substituting though, we have to rename the variable y to avoid mixing its bound with is free occurrence: (λt.(x(λx.xt))) to get (λx.(λt.(x(λx.xt))))y = [y ® x](λt.(x(λx.xt))) = (λt.(y(λx.xt))) In normal order reduction we try to reduce always the left most expression of a series of applications. We continue until no further reductions are possible. ## ArithmeticDefine 0 (zero) as λs.(λz.z) which has two arguments s and z and is abbreviated λsz.z with the understanding that s is the first and z the second argument to be substituted in the evaluation (any reduction). Using this notation define: 0 º λsz.z 1 º λsz.s(z) 2 º λsz.s(s(z)) 3 º λsz.s(s(s(z))) Define the successor function S º λwyx.y(wyx) Then S0 º (λwyx.y(wyx))(λsz.z) º (λyx.y((λsz.z)yx)) º λyx.y((λsz.z)yx) º λyx.y((λz.z)x) º λyx.y(x) º 1 and S1 º (λwyx.y(wyx))(λsz.s(z)) º λyx.y((λsz.s(z))yx) º λyx.y((λz.z)yx) º λyx.y((y)x) º 2 and S2 º (λwyx.y(wyx))(λsz.s(s(z))) º λyx.y((λsz.s(s(z)))yx) º λyx.y(y(y)x) º λyx.y(y(y(x))) = 3 ## Some formulasNote that Sn = n + 1 but nS = SS…S (n times) Therefore S and n do not commute ## AdditionTherefore nSm = n + m But nSm ≠ n(m+1) because of l ® r evaluation. ## Multiplication1 x 3 = 3 = SSS0 2 x 3 = 3 + 3 = 3+ SSS0 = SSSSSS0 3 x 3 = 3 + 3 + 3 = SSSSSSSSS0 i.e. n x m = ((n' x m') S) 0 where n' and m' are natural numbers so (n' x m') S means S applied n' x m' times. Suppose we had a multiplication operator M. Then nMm = ((n' x m') S) 0 Suppose μ = (λxyz.x(yz)) then nμm=(n'S0)μ(m'S0) … reductions … = ((n' x m') S) 0 Therefore one candidate for M is μ, i.e. one M is M = (λxyz.x(yz)) Note that for any function f 0fa = a ## ConditionalsConsider T = λxy.x and F= λxy.y, then TAB = A and FAB = B and TA = A and FA = I (identity) ## Logical operationsLet
Then — T = F and — F = T ## ConditionalLet Z = IF—F Then Z0 = IF—F0 = 0F—F = —F = T but, for N not zero ZN = IF—FN = NF—F = (FFF… n times … F)—F and since F applied to anything is the identity this results in ZN = F That is, ZN is T or F as N is zero or another natural number. ## PredecessorThe predecessor P, if there is one, would be the ‘inverse’ of S: PS = I. If π is a pair (a,b) it can be represented by λz.zab or Iab. Then πT = a and πF = b. If a function Φ is such that given a pair of numbers π = (r,r-1) then Φπ = (r+1,r) it can generate the predecessor of n by application to (0,0) or I00 n times and selecting the second number. In the case of 0, however, the predecessor would be 0. That is, this procedure results in 0 ® 0 but otherwise n ® n-1. The following is one such function: Φ º (λpz.z(S(pT))(pT)). Thus, applying Φ n times: P = (λn.nΦ(λz.z00)F and selecting the second member of the result (pair) gives the predecessor. ## EqualityIf (λxy.Z(xPy)) = 0 then x >= y. (λxy.&(Z(xPy))(Z(yPx))) = 0 then x = y. ## RecursionConsider the ‘recursion’ operator Y º (λy.(λx.y(xx))(λx.y(xx))) It has the property that for a function R YR = R(YR). Consider R º (λrn.Zn0(nS(r(Pn)))). It then follows that YRn = nS(YR(n-1)). Thus, noting that YR0 = 0, YR3 = 3S(YR2) = 3S(2S(YR1)) = 3S(2S(1SYR0)) = 6. |