and the operation that mapsftoffis writtenas Xf.Xr.f(f(z)). The evaluation of highe -order functions can get somewhat complex;as an exam ple,consider the following expression: ((Xf.xr.f(f(z)))(Ay.y2))(5) Convince yourself that this evaluates to 625.Another example is given in the following exercise: Exercise 1.Evaluate the lambda-expression （(af.z.fff))(Ag.Awg(g())(Az.z+1)）O) We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs.typed lambda-calculi We have already mentioned that when considerir ns as rules”,isno always necessary to know the domain and codomain of a function ahead of time The simplest example is the identity functionf which can have any set ain and c main are that we encountered above.One can check that o maps any function f:X to a function(f):.In this case,we say that the type of g is (X→X)→(X一X). By being fle mains and codoma s,we are able to manipulate func po d e we can take r=f,and we get f(f)=(Ar.)(f)=f. As another example,letw=Ar.r(). and the operation that maps f to f ◦ f is written as λf.λx.f(f(x)). The evaluation of higher-order functions can get somewhat complex; as an exam￾ple, consider the following expression: ￾ (λf.λx.f(f(x)))(λy.y2 )
(5) Convince yourself that this evaluates to 625. Another example is given in the following exercise: Exercise 1. Evaluate the lambda-expression ￾ (λf.λx.f(f(f(x)))) (λg.λy.g(g(y)))
(λz.z + 1) (0). We will soon introduce some conventions for reducing the number of parentheses in such expressions. 1.3 Untyped vs. typed lambda-calculi We have already mentioned that, when considering “functions as rules”, is not always necessary to know the domain and codomain of a function ahead of time. The simplest example is the identity function f = λx.x, which can have any set X as its domain and codomain, as long as domain and codomain are equal. We say that f has the type X → X. Another example is the function g = λf.λx.f(f(x)) that we encountered above. One can check that g maps any function f : X → X to a function g(f) : X → X. In this case, we say that the type of g is (X → X) → (X → X). By being flexible about domains and codomains, we are able to manipulate func￾tions in ways that would not be possible in ordinary mathematics. For instance, if f = λx.x is the identity function, then we have f(x) = x for any x. In particular, we can take x = f, and we get f(f) = (λx.x)(f) = f. Note that the equation f(f) = f never makes sense in ordinary mathematics, since it is not possible (for set-theoretic reasons) for a function to be included in its own domain. As another example, let ω = λx.x(x). 7