Java程序辅导

COMP6463: λ-Calculus
5. Computability
Michael Norrish
Michael.Norrish@nicta.com.au
Canberra Research Lab., NICTA
Semester 2, 2015
Last Time
An involved proof.
Lesson #1: The λ-calculus is a plausible programming language
§ there is an algorithm for turning λ-terms into values
§ (when those terms have values at all)
Lesson #2: Evaluation Orders are a Design Question
§ Do you want to guarantee as much termination as possible?
§ Use normal order
§ Or, do you want more speed, and unnecessary
non-terminations?
§ Use applicative order (like C, Java etc)
Today
What Makes a Computer?
Recursive Functions
Church Numerals
Richer Types
Lists
Conclusion
Introduction
Today’s Objective:
Show that the λ-calculus is capable of all possible
computation.
This requires us to know what “all possible computation” means.
For this we consult the Church-Turing Thesis.
What Makes a Computer? 4/27
The Church-Turing Thesis
In simple terms, the Church-Turing
thesis states that a function is
algorithmically computable if and
only if it is computable by a Turing
machine.
—Wikipedia, 2012
All computational models invented so far have been shown
equivalent to Turing Machines.
Two important examples:
§ The Recursive Functions
§ The λ-Calculus
What Makes a Computer? 5/27
Computational Equivalence
Two models M1 and M2 are computationally equivalent if
§ they each compute the same functions; or
§ each can simulate the other
We will assume that Turing Machines and the Recursive Functions
are equivalent.
We’ll show that the λ-Calculus can simulate the Recursive
Functions.
§ That will mean that the λ-Calculus is at least as powerful as
the Recursive Functions
§ Showing the other direction (that the Recursive Functions can
simulate the λ-Calculus) is very fiddly.
What Makes a Computer? 6/27
The Recursive Functions
Recursive functions are functions that take natural number
arguments and return natural number results.
Different recursive functions can take different numbers of
arguments.
For example, factorial (N→ N) and addition (N2 → N) are both
recursive functions.
Not all functions of this sort are recursive! (Consider cardinality)
What Makes a Computer? Recursive Functions 7/27
Recursive Functions—Base Cases
The following are all recursive functions
Zero n Þ→ 0 (written Z)
Successor: n Þ→ n+ 1 (written Suc)
Projection: xn1, n2, . . . nmy Þ→ ni (written pimi )
What Makes a Computer? Recursive Functions 8/27
Combining Recursive Functions: Composition
If f and g are recursive functions, so too is f ˝ g.
If f expects n arguments, can compose with n different others:
f ˝ xg1, . . . , gny
For example,
+ ˝ xˆ, fy
is a recursive function that behaves:
(+ ˝ xˆ, fy)(x, y) = xy+ f(x, y)
What Makes a Computer? Recursive Functions 9/27
Combining Recursive Functions: Primitive Recursion
If f : Nn → N and g : Nn+2 → N are recursive,
then Prxf, gy is recursive also, taking n+ 1 arguments such that
Prxf, gy(0, x1, . . . , xn) = f(x1, . . . , xn)
Prxf, gy(m+ 1, x1, . . . , xn) =
g(m,Prxf, gy(m,x1, . . . , xn), x1, . . . , xn)
What Makes a Computer? Recursive Functions 10/27
Primitive Recursion: Example
Prxf, gy(0, x1, . . . , xn) = f(x1, . . . , xn)
Prxf, gy(m+ 1, x1, . . . , xn) =
g(m,Prxf, gy(m,x1, . . . , xn), x1, . . . , xn)
Let f : N→ N be pi11, the identity function (a projection).
Let g : N3 → N be Suc ˝ pi32.
Then
Prxpi11,Suc ˝ pi32y(0, y) = pi11(y) = y
Prxpi11,Suc ˝ pi32y(x+ 1, y)
= (Suc ˝ pi32)(x,Prxpi11,Suc ˝ pi32y(x, y), y)
= Suc(pi32(x,Prxpi11,Suc ˝ pi32y(x, y), y))
= Suc(Prxpi11,Suc ˝ pi32y(x, y))
In other words, Prxpi11,Suc ˝ pi32y is addition.
What Makes a Computer? Recursive Functions 11/27
Primitive Recursion Defines a Lot!
Using just these facilities, we can define
§ Addition (as per previous slide)
§ Predecessor
§ predecessor of 0 is 0
§ Subtraction (repeat predecessor)
§ Write m´ n to mean m− n if m ě n, 0 otherwise
§ Multiplication (repeat addition)
§ Exponentiation (repeat multiplication)
§ Equality Tests
§ . . .
What Makes a Computer? Recursive Functions 12/27
Combining Recursive Functions: Minimisation
Let f be a recursive function taking n ą 1 arguments.
Then µf is also a recursive function, taking n− 1 arguments.
If there is an x where f(x, y1, . . . , yn−1) = 0,
(and f(y, y1, . . . , yn−1) is defined for all y ă x) then
µf(y1, . . . , yn−1) returns the least such x.
Otherwise µf(y1, . . . , yn−1) is undefined.
For example, if f(x, y) = (x2 ´ y) + (y´ x2), then
µf(9) = 3
µf(10) = K (undefined)
What Makes a Computer? Recursive Functions 13/27
So, How Do We Do All This With the λ-Calculus?
Important things:
§ Numbers
§ Primitive Recursion
§ Representation of Multiple Arguments (easy!)
§ Minimisation (unbounded search)
Church Numerals 14/27
Church Numerals
Represent number n with the λ-term (λf x. fn x).
Thus
Number Term
0 (λf x. x)
1 (λf x. f x)
2 (λf x. f (f x))
¨ ¨ ¨
7 (λf x. f (f (f (f (f (f (f x)))))))
¨ ¨ ¨
A number is represented by its own “recursion operator”:
Give a number n something to do n times to a base case
Church Numerals 15/27
Operations on Church Numerals: Successor
Suc = (λn. (λf x. f (n f x)))
In action:
Suc(3) ” Suc(λf x. f (f (f x)))
= (λf x. f ((λf x. f (f (f x))) f x))
” (λgy. g ((λf x. f (f (f x))) g y))
= (λgy. g ((λx. g (g (g x))) y))
= (λgy. g (g (g (g y))))
= 4
Church Numerals 16/27
Operations on Church Numerals: Addition
Numbers embody recursive operations.
+ = (λxy. x Suc y)
In action:
+ (λf x. f (f (f x))) y = (λf x. f (f (f x))) Suc y
= (λx.Suc (Suc (Suc x))) y
= Suc (Suc (Suc y))
Church Numerals 17/27
Unbounded Recursion
The famous Y combinator:
Y = (λf. (λx. f (x x)) (λx. f (x x)))
The important property of Y :
Y f = (λx. f (x x)) (λx. f (x x))
= f ((λx. f (x x)) (λx. f (x x)))
= f (Y f)
Church Numerals 18/27
Using the Y Combinator
Imagine wanting to implement the Collatz function:
c(0) = 1
c(1) = 1
c(n) =
{
c(n˜ 2) if n is even
c(3n+ 1) if n is odd
When programming without pattern-matching:
c(n) = if n ă 2 then 1
else if even(n) then c(n˜ 2)
else c(3n+ 1)
Church Numerals 19/27
Using the Y Combinator
Want:
c(n) = if n ă 2 then 1
else if even(n) then c(n˜ 2)
else c(3n+ 1)
Let
c0 = (λfn. if (ă n 2) 1 (if (even n) (f (˜ n 2)) (f (+ (ˆ 3 n) 1))))
Then (assuming we have ă, even, ˜ and if):
c
def
= Y c0
= c0 (Y c0)
= c0 c
= (λn. if (ă n 2) 1 (if (even n) (c (˜ n 2)) (c (+ (ˆ 3 n) 1))))
Church Numerals 20/27
How Do We Implement Booleans?
Let
K = (λxy. y)
J = (λxy. x)
if = (λb t e. b t e)
Then
if J t e = J t e
= (λy. t) e
= t
if K t e = K t e
= (λy. y) e
= e
Richer Types 21/27
Booleans and Numbers
Implement the “is zero” test:
isZero = (λn. n (K K) J)
Behaviour:
isZero 0 = (λn. n (K K) J) (λf x. x)
= (λf x. x) (K K) J
= J
isZero 3 = (λn. n (K K) J) (λf x. f (f (f x)))
= (λf x. f (f (f x))) (K K) J
= K K (K K (K K J))
= K
Richer Types 22/27
How Do We Implement Pairs?
Let
Pair = (λxy f. f x y)
fst = (λp. p (λxy. x))
snd = (λp. p (λxy. y))
Then
fst (Pair M N) = fst (λf. f M N)
= (λf. f M N) (λxy. x)
= (λxy. x) M N
= (λy.M) N
= M
Richer Types 23/27
How Do We Implement Lists?
Let
nil = (λcn. n)
cons = (λh t cn. c h (t c n))
Thus:
[2] = cons 2 nil
= (λcn. c 2 (nil c n))
= (λcn. c 2 n)
[3, 2] = cons 3 [2]
= (λcn. c 3 ([2] c n))
= (λcn. c 3 (c 2 n))
Richer Types Lists 24/27
More Lists
Let
Sum = (λ`. ` + 0)
Then
Sum [3, 1, 2] = Sum (λcn. c 3 (c 1 (c 2 n)))
= (λcn. c 3 (c 1 (c 2 n))) + 0
= (λn.+ 3 (+ 1 (+ 2 n))) 0
= + 3 (+ 1 (+ 2 0))
= 6
Richer Types Lists 25/27
Summary
The λ-Calculus is “Turing-Complete”.
Church Numerals allow for direct encodings of
primitive recursive functions such as addition and multiplication.
The Y combinator can encode unbounded search through
arbitrary recursion.
§ The λ-Calculus thus captures all recursive functions.
The λ-calculus can encode (in a standard way)
algebraic data types such as lists and trees.
Conclusion 26/27
(Half-)Topic Summary
§ Equational Logic
§ connection to −→β˚
§ inconsistent assumptions
§ soundness & completeness
§ Soundness via Church-Rosser
§ Diamond chasing and parallel reduction
§ Standardisation
§ Normal order evaluation finds normal forms
§ Computation
§ Church Numerals
§ Encoding Other Types
§ Encoding the Recursive Functions
Conclusion 27/27