Download Here - CWI

2.4.
LAMBDA ABSTRACTION
57
5. ∀ε ∈ R+ ∃n ∈ N∀m ∈ N(m > n ⇒ (|a − am | 6 ε)). (R+ is the set of
positive reals; a, a0 , a1 , . . . refer to real numbers .)
Remark. Note that translating back and forth between formulas and plain
English involves making decisions about a domain of quantification and
about the predicates to use. This is often a matter of taste. For instance,
how does one choose between P (n) for ‘n is prime’ and the spelled out
n > 1 ∧ ¬∃d ∈ N(1 < d < n ∧ d|n),
which expands the definition of being prime? Expanding the definitions of
mathematical concepts is not always a good idea. The purpose of introducing
the word prime was precisely to hide the details of the definition, so that
they do not burden the mind. The art of finding the right mathematical
phrasing is to introduce precisely the amount and the kind of complexity
that are needed to handle a given problem.
Before we will start looking at the language of mathematics and its
conventions in a more systematic way, we will make the link between
mathematical definitions and implementations of those definitions.
2.4
Lambda Abstraction
The following description defines a specific function that does not depend
at all on x:
The function that sends x to x2 .
Often used notations are x 7→ x2 and λx.x2 . The expression λx.x2 is called
a lambda term.
If t is an expression of type b and x is a variable of type a then λx.t
is an expression of type a → b, i.e., λx.t denotes a function. This way of
defining functions is called lambda abstraction.
Note that the function that sends y to y 2 (notation y 7→ y 2 , or λy.y 2 )
describes the same function as λx.x2 .
In Haskell, function definition by lambda abstraction is available. Compare
the following two definitions:
square1 :: Integer -> Integer
square1 x = x^2
square2 :: Integer -> Integer
square2 = \ x -> x^2