The original URL for this material was http://cs.wwc.edu/~aabyan/221_2/PLBOOK/Functions.html . Thanks to Anthony A. Aaby at Walla Walla College, and thanks to the Wayback Machine for saving a copy when it went offline. I have corrected a few special characters.
Functional programming is characterized by the programming with values, functions and functional forms.
Keywords and phrases: Lambda calculus, free and bound variables, scope, environment, functional programming, combinatorial logic, recursive functions, functional, curried function.
Functional programming languages are the result of both abstracting and generalizing the data type of maps. Recall, the mapping m from each element x of S (called the domain) to the corresponding element m(x) of T (called the range) is written as:
For example, the squaring function is a function of type:
and may be defined as:
A linear function f of type
may be defined as:
The function:
may be written as the composition of the functions f and sqr as:
where
The compositional operator is an example of a functional form. Functional programming is based on the mathematical concept of a function and functional programming languages include the following:
The basic concepts of functional programming originated with LISP. Functional programming languages are important for the following reasons.
Terminology. Functional programming languages are called applicative since the functions are applied to their arguments, declarative and non-procedural since the definitions specify what is computed and not how it is computed.
As an informal example of the lambda-calculus, consider the function defined by the polynomial expression
The variable x is a parameter. In the lambda-calculus, the notation λx.M is used to denote a function with parameter x and body M. That is, x is mapped to M. We rewrite our function in this format
and read it as ``the function of x whose value is defined by x2 + 3x - 5''. The lambda-calculus uses prefix form and so we rewrite the body in prefix form,
The lambda-calculus curries its functions of more than one variable i.e. (+ x y) is written as ((+ x) y), the function (+ x) is the function which adds something to x. Rewriting our example in this form we get:
To denote the application of a function f to an argument a we write
To evaluate the function application, we remove the λx. and replace each remaining occurence of x with 1 to get
then evaluate the two multiplication expressions
then the addition
and finally the subtraction
We say that the variable x is bound in the lambda-expression λx.B. A variable occuring in the lambda-expression which is not bound is said to be free. The variable x is free in the lambda-expression λy.((+ x) y). The scope of the variable introduced (or bound) by lambda is the entire body of the lambda-abstraction.
The lambda-notation extends readily to functions of several arguments. Functions of more than one argument can be curried to produce functions of single arguments. For example, the polynomial expression xy can be written as
When the lambda-abstraction λx. λy. xy is applied to a single argument as in (λx. λy. xy 5) the result is λy. 5y, a function which multiplies its argument by 5. A function of more than one argument is reguarded as a functional of one variable whose value is a function of the remaining variables, in this case, ``multiply by a constant function.''
The special character of the lambda-calculus is illustrated when it is recognized that functions may be applied to other functions and even permit self application. For example let C = λf. λx . (f(fx))
The pure lambda-calculus does not have any built-in functions or constants. Therefore, it is appropriate to speak of the lambda-calculi as a family of languages for computation with functions. Different languages are obtained for different choices of functions and constants.
We will extend the lambda-calculus with common mathematical operations and constants so that λx.((+ 3) x) defines a function that maps x to x+3. We will drop some of the parentheses to improve the readability of the lambda expressions.
A lambda-expression is executed by evaluating it. Evaluation proceeds by repeatedly selecting a reducible expression (or redex) and reducing it. For example, the expression (+ (* 5 6) (* 8 3)) reduces to 54 in the following sequence of reductions.
(+ (* 5 6) (* 8 3)) → (+ 30 (* 8 3))
→ (+ 30 24)
→ 54
When the expression is the application of a lambda-abstraction to a term, the
term is substituted for the bound variable. This substitution is called
β-reduction. In the following sequence of reductions, the first
step an example of β-reduction. The second step is the
reduction required by the addition operator.
The pure lambda-calculus has just three constructs: primitive symbols, function application, and function creation. Figure N.1gives the syntax of the lambda-calculus.(λx.((+ 3) x)) 4
((+ 3) 4)
7
Figure N.1: The Lambda Calculus Syntax:L in Lambda Expressions(L L) is function application, and
x in Symbols
L ::= x | (L L) | (λx.L)
(λx.L) is a lambda-abstraction which defines a function with argument x and body L.
We say that the variable x is bound in the lambda-expression λx.B. A variable which occurs in but is not bound in a lambda-expression is said to be free. The scope of λx. is B. In the lambda-expression λy.x+y, x is free and y is bound.
We adopt the following notational conventions:
(λx.((+ x) 3)) to represent the function x + 3
λx.((+ x) 3) instead of (λx.((+ x) 3)) and
λx.((+ x) 3) 4 instead of (λx.((+ x) 3) 4)
(+ x 3) instead of ((+ x) 3) that is, we may write
λx.+ x 3 instead of λx.((+ x) 3)
(λx.+ x 3) 4 instead of λx.+ x 3 4
(λx.x + 3) 4 instead of (λx.+ x 3) 4
λxy.x + y instead of λx.λy.x + y
The normal form is formally defined in the following definition.
1. λx.(x2 - 5) 3 f(3) where f(x) = x2 - 5 2. 32 - 5 by substitution 3. 9 - 5 power 4. 4 subtraction
Definition: A lambda-expression is said to be in normal form if no β-redex, a subexpression of the form (λx.P Q ), occurs in it.Non-terminating computations are examples of expressions that do not have normal forms. The lambda-expression
does not have a normal form as we shall soon see.
We define substitution, B[x:M], to be the replacement of all free occurences of x in B with M. Figure N.2 contains a formal definition of substitution.
Figure N.2: Substitution where s is a symbol, M, A and B are lambda-expressions.
s[x:M] = if (s=x) then M else s (A B)[x:M] = (A[x:M] B[x:M]) (λx.B)[x:M] = (λx.B) (λy.B)[x:M] = if (z is a symbol not free in B or M) then λz.(B[y:z][x:M])
Lambda expressions are simplified using β-reduction. β-reduction applies a lambda-abstraction to an argument producing an instance of the body of the lambda-abstraction in which (free) occurrences of the formal parameter in the body are replaced with (copies of) the argument. With the definition of substitution in Figure N.2 and the formal definition of β-reduction in Fugure N.3, we have the tools needed to reduce lambda-expressions to normal forms.
Figure N.3: β-reduction (λx.B) e ⇒ B[x:e]
It is easy to see that the lambda-expression
does not have a normal form because when the second expression is substituted into the first, the resulting expression is identical to the given lambda-expression.
Figure 2 defines the operational semantics of the lambda-calculus in terms of β-reduction.
Figure N.4: Operational semantics for the lambda-calculus Interpreter: reduce expression E to normal form.
Reduce in L → L
where
Reduce[s] = s Reduce[λx.B M] = Reduce[ B[x:M] ] Reduce[L1 L2] = (Reduce[ L1 ] Reduce[ L2 ]) s is a symbol and B, L1, L2, and M are lambda-expressions
The operational semantics of Figure N.4 describe a syntactic transformation of the lambda-expressions.
Theorem: If E has a normal form N then there is a leftmost reduction of E to N.The leftmost outermost reduction (normal order reduction) strategy is called lazy reduction because it does not first evaluate the arguments but substitutes the arguments directly into the expression. Eager reduction is when the arguments are reduced before substitution.
A function is strict if it is sure to need its argument. If a function is non-strict, we say that it is lazy.
parameter passing: by value, by name, and lazy evaluation
Infinite Data Structures
call by need
streams and perpetual processes
A function f is strict if and only if (f ⊥) = ⊥
Scheme evaluates its parameters before passing (eliminates need for renaming) a space and time efficiency consideration.
We can express the semantics of the lambda-calculus as a mathematical function, Eval, from expressions to values. For example,
Figure N.5 gives a denotational semantics for the lambda-calculus.
Figure N.5: Denotational semantics for the lambda-calculus Semantic Domains:
s in DSemantic Function:Eval in L → DSemantic Equations:
where s is a symbol, B, L1, L2, and M are expressions, B[x:M] is substitution as in Figure N.2, E is an expression which does not have a normal form, and _|_ is pronounced bottom.
Eval [ s ] = s Eval [ (λx.B M) ] = Eval [ B[x:M] ] Eval [ (L1 L2) ] = (Eval [ L1 ] Eval [ L2 ]) Eval [ E ] = _|_
The denotational semantics of Figure N.5 describe a mapping of lambda expressions to values in some semantic domain.
Lambda ExpressionsWith the introduction of named expressions we have the potential for recursive definitions since the extended syntax permits us to name lambda-abstractions and then refer to them within a lambda-expression. Consider the following recursive definition of the factorial function.L ::= ...| x : L | ...where x is the name of the lambda-expression L.
which with syntactic sugaring is
We can treat the recursive call as a free variable and replace the previous definition with the following.
Let
Note that H is not recursively defined. Now we can redefine FAC as
This definition is like a mathematical equation. It states that when the function H is applied to FAC, the result is FAC. We say that FAC is a fixed point or fixpoint of H. In general functions may have more than one fixed point. In this case the desired fixed point is the mathematical function factorial. In general, the `right' fixed point turns out to be the unique least fixed point.
It is desirable that there be a function which applied to a lambda-abstraction returns the least fixed point of that abstraction. Suppose there is such a function Y where,
Y is called a fixed point combinator. With the function Y, this definition of FAC does not use of recursion. From the previous two definitions, the function Y has the property that
As an example, here is the computation of FAC 1 using the Y combinator.
FAC 1 = (Y H) 1
= H (Y H) 1
= λfac.(λn.(if (= n 0) 1 (* n (fac (- n 1))))) (Y H) 1
= λn.(if (= n 0) 1 (* n((Y H)(- n 1)))) 1
= if (= 1 0) 1 (* 1 ((Y H)(-11)))
= (* 1 ((Y H)(-11)))
= (* 1 ((Y H)0))
= (* 1 (H (Y H) 0))
...
= (* 1 1)
= 1
The function Y can be defined in the lambda-calculus.
It is especially interesting because it is defined as a lambda-abstraction without using recursion. To show that this lambda-expression properly defines the Y combinator, here it is applied to H.
(Y H) = (λh.(λx.(h (x x)) λx.(h (x x))) H)
= (λx.(H (x x)) λx.(H (x x)))
= H ( λx.(H (x x))λx.(H (x x)))
= H (Y H)
Here is an example using the let-extension.
Lets may be used where ever a lambda-expression is permitted. For example,
is equivalent to
Simple recursive definitions are introduced with letrec expressions which are defined in terms of let expressions and the Y combinator:
Let and letrec expressions may be nested. The definitions of the let and letrec expressions are restated in Figure N.6.
Figure M.6: Lexical Scope Rules
let n : E in B = (λn.B) E
letrec n : E in B = let n : Y (λn.E) in B
Mutual recursion may also be defined but is beyond the scope of this text.
Curry, Feys, and Craig define a number of combinators among them the following:
These definitions lead to transformation rules for sequences of combinators. The reduction rules for the SKI calculus are given in Figure N.7.
S = λf .( λg .( λx. f x ( g x ) ) ) K = λx .λy. x I = λx.x Y = λf. λx.( f(x x)) λx.(f (x x))
Figure N.7: Reduction rules for SKI calculus
S f g x → f x (g x) K c x → c I x → x Y e → e (Y e) (A B) → A B (A B C) → A B C
The reduction rules require that reductions be performed left to right. If no S, K, I, or Y reduction applies, then brackets are removed and reductions continue.
The SKI calculus is computationally complete; that is, these three operations are sufficient to implement any operation. This is demonstrated by the rules in Figure N.8.
Figure N.8: Translation Semantics for the Lambda calculus
Compile [ s ] → s Compile [ (E1 E2)] → (Compile [ E1] Compile [ E2 ]) Compile [ λx.E] → Abstract [ (x, Compile [ E] ) ] Abstract [ (x, s) ] → if (s=x) then I else (K s) Abstract [ (x, (E1 E2))] → ((S Abstract [ (x, E1)] ) Abstract [ (x, E2) ] ) where s is a symbol.
which translate lambda-expressions to formulas in the SKI calculus.
Any functional programming language can be implemented by a machine that implements the SKI combinators since, functional languages can be transformed into lambda-expressions and thus to SKI formulas.
Function application is relatively expensive on conventional computers. The principle reason is the complexity of maintaining the data structures that support access to the bound identifiers. The problems are especially severe when higher-order functions are permitted. Because a formula of the SKI calculus contains no bound identifiers, its reduction rules can be implemented as simple data structure manipulations. Further, the reduction rules can be applied in any order, or in parallel. Thus it is possible to design massively parallel computers (graph reduction machines) that execute functional languages efficiently.
Recursive functions may be defined with the Y operator.
with the corresponding reduction rules.
B = λx .( λy .( λz. ((x y) z))) C = λx .(λy.(λz((x z) y)))
| B a b c | →((a b) c) |
| C a b c | →((a c) b) |
Having these combinators we can simplify the expressions obtained by applying the rules in Figure N.9.
Figure N.9: Optimizations for SKI code The optimizations must be applied in the order given.
S (K e) (K f) → K (e f) S (K e) I → e S (K e) f → (B e) f S e (K f) → (C e) f
Just as machine language (assembler) can be used for programming, combinatorial logic can be used as a programming language. The programming language FP is a programming language based on the idea of combinatorial logic.
Scheme SyntaxExpressions are atoms which are variables or constants, lists of arbitrary length (which are also function applications), lambda-abstractions of one or more parameters, and other built-in functions.E in Expressions
A in Atoms ( variables and constants )
...
E ::= A | (E...) | (lambda (A...) E) | ...
Scheme provides a number of built in functions among which are +, -, *, /, <, <=, =, >=,>, and not. Scheme provides for conditional expressions of the form (if E0 E1 E2) and (if E0 E1). Among the constants provided in Scheme are numbers, #f and the empty list () both of which count as false, and #t and any thing other than #f and () which count as true. nil is also used to represent the empty list.
E ::= ...| (define I E) | ...
Figure N.10: Stack operations in Scheme ( define empty_stack ( lambda ( stack ) ( if ( null? stack ) \#t \#f ))) ( define push ( lambda ( element stack ) ( cons element stack ) )) (define pop ( lambda ( element stack ) ( cdr stack ))) (define top ( lambda ( stack ) ( car stack )))
Figure N.10 contains an example of stack operations writtem in Scheme. The figure illustrates definitions, the conditional expression, the list predicate null? for testing whether a list is empty, and the list manipulation functions cons, car, and cdr.
Scheme SyntaxThe let definitions are done independently of each other (collateral bindings), the let* values and bindings are computed sequentially and the letrec bindings are in effect while values are being computed to permit mutually recursive definitions....
B in Bindings
...E ::= ...| (let B0 E0) | (let* B1 E1) | (letrec B2 E2) |...
B ::= ((I E)...)
Figure N.11: A sample program in Haskell module AStack( Stack, push, pop, top, size ) where data Stack a = Empty | MkStack a (Stack a) push :: a -> Stack a -> Stack a push x s = MkStack x s size :: Stack a -> Integer size s = length (stkToLst s) where stkToLst Empty = [] stktoLst (MkStack x s) = x:xs where xs = stkToLst s pop :: Stack a -> (a, Stack a) pop (MkStack x s) = (x, case s of r -> i r where i x = x) top :: Stack a -> a top (MkStack x s) = x
module Qs where qs :: [Int] -> [Int] qs [] = [] qs (a:as) = qs [x | x <- as, x <=a] ++ [a] ++ qs [x | x <- as, x> a]
module Primes where primes :: [Int] primes = map head (iterate sieve [2 ..]) sieve :: [Int] -> [Int] sieve (p:ps) = [x | x <- ps, (x `mod` p)=0]
module Fact where fact :: Integer -> Integer fact 0 = 1 fact (n+1) = (n+1)*fact n -- * "Foo" fact _ = error "Negative argument to factorial"
module Pascal where pascal :: [[Int]] pascal = [1] : [[x+y | (x,y) <- zip ([0]++r) (r++[0])] | r <- pascal] tab :: Int -> ShowS tab 0 = λx -> x tab (n+1) = showChar ' ' . tab n showRow :: [Int] -> ShowS showRow [] = showChar '\n' showRow (n:ns) = shows n . showChar ' ' . showRow ns showTriangle 1 (t:_) = showRow t showTriangle (n+1) (t:ts) = tab n . showRow t . showTriangle n ts
module Merge where
merge :: [Int] -> [Int] -> [Int]
merge [] x = x
merge x [] = x
merge l1@(a:b) l2@(c:d) = if a < c then a:(merge b l2)
else c:(merge l1 d)
half [] = []
half [x] = [x]
half (x:y:z) = x:r where r = half z
sort [] = []
sort [x] = [x]
sort l = merge (sort odds) (sort evens) where
odds = half l
evens = half (tail l)
The lambda-calculus and combinatory logic are abstract models of computation equivalent to the Turing machine, recursive functions, and Markov chains. Unlike the Turning machine which is sequential in nature, they retain the implicit parallelism that is present in mathematical expressions.
The lambda-calculus is a direct influence on the programming language LISP, the call by name parameter passing mechanism of Algol-60, and textual substitution performed by macro generators.
Explicit and systematic use of the lambda-calculus in computer science was initiated in the early 1960s by Peter Landin, Christopher Strachy and others who started a formal theory of semantics for programming languages called denotational semantics. Dana Scott (1969) discovered the first mathematical model for the type-free lambda-calculus.
New hardware designs are appearing to support the direct execution of the lambda-calculus or combinators which support parallel execution of functional programs, removing the burden (side-efficts, synchonization, communication) of controlling parallelism from the programmer.
LISP (LISt Processing) was designed by John McCarthy in 1958. LISP grew out of interest in symbolic computation. In particular, interest in areas such as mechanizing theorem proving, modeling human intelligence, and natural language processing. In each of these areas, list processing was seen as a fundamental requirement. LISP was developed as a system for list processing based on recursive functions. It provided for recursion, first-class functions, and garbage collection. All new concepts at the time. LISP was inadvertantly implemented with dynamic rather than static scope rules. Scheme is a modern incarnation of LISP. It is a relatively small language with static rather than dynamic scope rules. LISP was adopted as the language of choice for artificial intelligence applications and continues to be in wide use in the aritficial intelligence community.
ML
Miranda
Haskell is a modern language named after the logician Haskell B. Curry, and designed by a 15-member international committee. The design goals for Haskell are have a functional language which incorporates all recent ``good ideas'' in functional language research and which is suitable for for teaching, research and application. Haskell contains an overloading facility which is incorporated with the polymorphic type system, purely functional i/o, arrays, data abstraction, and information hiding.
Functional programming languages have been presented in terms of a sequence of virtual machines. Functional programming languages can be translated into the lambda-calculus, the lambda-calculus into combinatorial logic and combinatorial logic into the code for a graph reduction machine. All of these are virtual machines.
Models of the lambda-calculus.
History \cite{McCarthy60} For an easily accessable introduction to functional programming, the lambda-calculus, combinators and a graph machine implementation see Revesz (1988). For Backus' Turing Award paper on functional programming see \cite{Backus78}. The complete reference for the lambda-calculus is \cite{Bare84}. For all you ever wanted to know about combinatory logic see \cite{CF68,CHS72,HS86}. For an introduction to functional programming see Henderson (1980), BirdWad88, MLennan90. For an intoduction to LISP see \cite{McCarthy65} and for common LISP see \cite{Steele84}. For a through introduction to Scheme see \cite{AbSus85}. Haskell On the relationship of the lambda-calculus to programming languages see \cite{Landin66}. For the implementation of functional programming languages see Henderson (1980) and Peyton-Jones (1987).
Redo the previous exercise making use of the η-rule whenever possible. What value is there in the α-rule?α-rule: (λx.E) ⇒ (λy.E[x:y]) η-rule: (\x.E x) ⇒ E where x does not occur free in E