COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
COMP0020 Functional Programming Lecture 7
Recursion and the Lambda Calculus
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 1 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Contents
Introduction
Recursive functions in Miranda
Recursive functions in the lambda calculus
Binding for function name
Fixed point
Fixed point operator self-application
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 2 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Introduction
Recursive function f
↓
Intermediate function h
↓ ←− Fixed points and the fixpoint operator Y Definition of f in terms of Y
↓ ←− How to define Y in the lambda calculus Final Lambda-calculus definition of f
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 3 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
Consider :
fx =3,if(x=0) = 11, otherwise
In the lambda calculus this is :
λ x.(if (x = 0) 3 11)
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
4 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
However, now consider :
fx =3,if(x=0)
= 1 + f(x – 1), otherwise
What’s wrong with this ? :
λ x.(if (x = 0) 3 (1 + (f(x – 1))))
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
5 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
Consider it again in the context of the whole program :
f x = 3, if (x = 0)
= 1 + f(x – 1), otherwise
main =f7
This would translate to the following, which still has a problem : λf.(f 7)(λx.(if(x=0)3(1+(f(x-1)))))
→β λ x.(if (x = 0) 3 (1 + (f(x – 1)))) 7
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 6 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
SO how can we represent a recursive function in the lambda calculus ?
1 First define a new NON-RECURSIVE function (e.g. call it “h”), whose body is identical to that of
“f” but which takes “f” as an argument,1 as follows : hfx =3,if(x=0)
= 1 + f(x – 1), otherwise
1. NB here we are using a curried style of function definition.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 7 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
1 Now the following lambda expression for “h” is fine, because “f” is bound : λ f.(λ x.(if (x=0) 3 (1+(f(x-1))))
BUT “h” is not “f”, so we haven’t solved the problem yet!
2 However, notice that the partial application (h f) gives the same result as f, so (h f) ≡ f (this is an identity, not a definition)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 8 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
A “fixed point” (or “fixpoint”) of any function g is a value x from the input domain of g such that (g x) ≡ x
Example 1 :
id x = x
Every value in the input domain of id is a fixed point of id
Example 2 :
three x = 3, if (x = 3)
= (x + 1), otherwise
The input value 3 is the only fixed point of the function three
Note that (from the previous slide) the function f is a fixpoint of the function h because (h f ) ≡ f
id is called the “identity function”
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 9 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
There is a special operator (called the “fixpoint operator”) that we can incorporate into the λ-calculus, which will return the fixed-point of any function.
The fixpoint operator is often given the name Y
It takes a function as its argument (call it g) and returns a fixed point of the function g
Thus, by definition, g (Y g) = (Y g)
If the identified fixed-point of g is itself a function 2 then Y returns the “least” (i.e. the definition with
the least amount of arbitrary additional information) version of that function. 3
So now (Y h) gives the least fixpoint of h, which we know is f (because (h f) ≡ f)
f=Yh
2. We alredy know that in the λ calculus we can easily pass functions as arguments, and return them as results.
3. We skate over some interesting problems : what if g doesn’t have a fixpoint? can g have more than one “least” fixpoint ? This is outside the scope of this module, but further explantions are found in Stoy’s excellent book Denotational Semantics : The Scott-Strachey Approach to Programming Language Theory by J.E.Stoy, 1979.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 10 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
The reduction rule for operator Y is trivial : Y g → g (Y g)
Now, for example (because f is the least fixpoint of h), a Normal Order reduction 4 of f 1 gives :
f1 = (Y h) 1 =(h (Yh))1
= ((λ f.(λ x.(if
=(λx.(if(x=
=(if(1=0)3
= (if false 3
= 1 + ((Y h) (1 – 1))
=1+((h (Yh))(1-1))
= 1 + (((λ f.(λ x.(if (x=0) 3 (1 + (f (x-1)))))) (Y h)) (1-1)) = 1 + ((λ x.(if (x = 0) 3 (1 + ((Y h)(x – 1))))) (1 – 1)) =1+((if((1-1)=0)3(1+((Yh)((1-1)-1))))) =1+((if(0=0) 3(1+((Yh)((1-1)-1))))) =1+3
4. Other reduction orders may not terminate.
Christopher D. Clack (University College London) COMP0020: Functional Programming
becausef=Yh becauseYg→g(Yg) from the definition of h after one β reduction
after another β reduction after δ reduction of =
after δ reduction of if loop ! becauseYg→g(Yg) from the definition of h after one β reduction
after another β reduction after δ reduction of =
after δ reduction of if
Academic Year 2019-2020 11 / 56
(x=0)3(1+(f(x-1))))))(Yh))1 0) 3 (1 + ((Y h)(x – 1))))) 1
(1 + ((Y h)(1 – 1))))
(1 + ((Y h)(1 – 1))))
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
Now we have a lambda expression that defines “f”
Y (λ f.(λ x.(if (x = 0) 3 (1 + (f (x – 1))))))
But haven’t we really just shifted the problem ? — how do we define Y in the lambda calculus ?
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 12 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
The real magic : self-application
Y ≡ λq.( (λx.(q (x x))) (λx.(q (x x))) )
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 13 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
Example :
Y h = λq.( (λx.(q (x x))) (λx.(q (x x))) ) h
= (λx.(h (x x))) (λx.(h (x x)))
= h ((λx.(h (x x))) (λx.(h (x x)))) =h(Yh)
line1
line2
line3
becauseline3 ≡(hline2)andline2 ≡Y h
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 14 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Recursion and the lambda calculus
Deriving a λ-calculus definition of the recursive function f without using Y :
f =(Yh)
= (Y (λ f.(λ x.(if (x=0) 3 (1+(f(x-1)))))))
= ((λq.((λx.(q (x x))) (λx.(q (x x))))) (λ f.(λ x.(if (x=0) 3 (1+(f(x-1)))))))
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 15 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Summary
Summary
Recursive functions in Miranda
Recursive functions in the lambda calculus
Binding for function name
Fixed point
Fixed point operator Self-application
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 16 / 56
COMP0020: Functional Programming
Section 7 : Recursion and the Lambda Calculus
Summary
END OF LECTURE
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 17 / 56