Java程序辅导

COMP6463: λ-Calculus
1. Basics
Michael Norrish
Michael.Norrish@nicta.com.au
Canberra Research Lab., NICTA
Semester 2, 2015
Outline
Introduction
Lambda Calculus Terms
Alpha Equivalence
Substitution
Dynamics
Beta Reduction
Eta Reduction
Normal Forms
Evaluation Strategies
Conclusion
The Lambda Calculus
Alonzo Church
(1903–1995)
The λ-calculus is a fundamental
computational model.
It also has a number of connections
to logic.
The next five lectures (including this one) will
concentrate on the untyped calculus.
The typed calculus has the most elegant con-
nections to logic, so we will focus on computa-
tion.
But there is also an interesting equational logic
to consider.
Introduction 3/30
Course Plan
By me:
1. Basics (today)
2. Equational Logic
I connection to −→∗β
I examples
I inconsistent assumptions
I soundness & completeness
3. Soundness via Church-Rosser
4. Standardisation
5. Computation
I Church Numerals
I Encoding Other Types
I Encoding the Recursive Functions
And then, five lectures on the typed calculus by Jeremy Dawson.
Introduction 4/30
Some Sources
H. P. Barendregt, The Lambda Calculus:
Its Syntax and Semantics. Elsevier, 1984.
ISBN 0 444 87508 5.
Chris Hankin, Lambda Calculi: A Guide
for Computer Scientists. Oxford University
Press, 1994. ISBN 0 19 853840 3.
Introduction 5/30
What are Lambda Terms?
Lambda terms make up the world’s simplest programming
language.
A lambda term is either
I a variable v; or
I the application of term M to term N, written M N; or
I the abstraction of variable v in term M, written (λv.M).
Examples:
I f x — f, a “function”, applied to an argument x
I (f x) y — a function applied to two arguments
I f (g x) — two function calls
I (λv. v) — the identity function
I (λu. (λv. u z)) x — abstraction and application
Lambda Calculus Terms 6/30
Term Shorthands
Applications are left-associative.
So, you can write M N P, and don’t have to write (M N) P
(You do have to write M (N P) with the parentheses.)
You can “chain” binders.
Instead of (λu. (λv.M)), just write (λu v.M)
Thus:
S = (λab c. a c (b c))
instead of
S = (λa. (λb. (λc. (a c) (b c))))
Think of abstract syntax trees if necessary.
Lambda Calculus Terms 7/30
Abstractions are (Anonymous) Functions
In secondary school mathematics, you learn to write things like
f(x) = x2 + 2x+ 1
meaning that f is a function that takes a parameter x and returns
a value derived from that x.
When you learnt to program, you might have learnt to write
int f(int x)
{
return x*x + 2*x + 1;
}
instead.
Lambda Calculus Terms 8/30
Abstractions are (Anonymous) Functions
In λ-calculus (with arithmetic added), you might write
f = (λx. x2 + 2x+ 1)
In other words,
(λx. x2 + 2x+ 1)
is a function that takes a value x as a parameter, and calculates a
“return value”.
This λ-term is a function without a name. We can decide to give it
the name f (or g, or nothing) later.
Lambda Calculus Terms 9/30
Free and Bound Names
Consider: (λv. u v)
The variable v is bound. It’s the name of a parameter.
The variable u is free.
It’s not the name of an enclosing parameter.
The same notions are apparent in other languages:
int f(int v)
{
return u + v;
}
Lambda Calculus Terms Alpha Equivalence 10/30
Bound Names Can be Renamed
These two functions are the same:
int f(int v)
{
return u + v;
}
int f(int x)
{
return u + x;
}
But this one is different:
int f(int u)
{
return u + u;
}
Clearly, not all bound variable renaming is OK.
Lambda Calculus Terms Alpha Equivalence 11/30
Alpha Equivalence
Two λ-terms M and N are alpha-equivalent (written M ≡ N) if
they
“are the same up to renaming of bound variables”
Proof rules
v ≡ v
M1 ≡M2 N1 ≡ N2
M1 N1 ≡M2 N2
v not free in M N ≡ (uv) ·M
(λu.M) ≡ (λv.N)
where (uv) ·M = “swap u and v everywhere they appear in M”
Lambda Calculus Terms Alpha Equivalence 12/30
Alpha Equivalence—Examples
Rule for (λv.M) again:
v not free in M N ≡ (uv) ·M
(λu.M) ≡ (λv.N)
where (uv) ·M = “swap u and v everywhere they appear in M”
So,
(λv. v u) x ≡ (λw.w u) x 6≡ (λu. u u) x
(λu. (λv. u v) u) ≡ (λv. (λu. v u) v) 6≡ (λu. (λu. u v) u)
(λx. (λy. f y) x) ≡ (λy. (λy. f y) y) 6≡ (λf. (λy. f y) f)
Lambda Calculus Terms Alpha Equivalence 13/30
Alpha Equivalence—Examples
Rule for (λv.M) again:
v not free in M N ≡ (uv) ·M
(λu.M) ≡ (λv.N)
where (uv) ·M = “swap u and v everywhere they appear in M”
So,
(λv. v u) x ≡ (λw.w u) x 6≡ (λu. u u) x
(λu. (λv. u v) u) ≡ (λv. (λu. v u) v) 6≡ (λu. (λu. u v) u)
(λx. (λy. f y) x) ≡ (λy. (λy. f y) y) 6≡ (λf. (λy. f y) f)
Lambda Calculus Terms Alpha Equivalence 13/30
Alpha Equivalence—Examples
Rule for (λv.M) again:
v not free in M N ≡ (uv) ·M
(λu.M) ≡ (λv.N)
where (uv) ·M = “swap u and v everywhere they appear in M”
So,
(λv. v u) x ≡ (λw.w u) x 6≡ (λu. u u) x
(λu. (λv. u v) u) ≡ (λv. (λu. v u) v) 6≡ (λu. (λu. u v) u)
(λx. (λy. f y) x) ≡ (λy. (λy. f y) y) 6≡ (λf. (λy. f y) f)
Lambda Calculus Terms Alpha Equivalence 13/30
Substitution
Substitution is a ternary operation:
M[v := N]
means “replace free occurrences of v in M with N”
(making sure that free variables in N are not captured by binders in M)
(alpha-convert M as necessary)
Conditions:
I Freeness: (λv.M)[v := N] ≡ (λv.M)
(as v is not free in (λv.M))
I Capture-avoiding:
(λv. u v)[u := v] 6≡ (λv. v v) (!!!)
(λv. u v)[u := v] ≡ (λw.u w)[u := v]
≡ (λw. v w)
Lambda Calculus Terms Substitution 14/30
Substitution
Substitution is a ternary operation:
M[v := N]
means “replace free occurrences of v in M with N”
(making sure that free variables in N are not captured by binders in M)
(alpha-convert M as necessary)
Conditions:
I Freeness: (λv.M)[v := N] ≡ (λv.M)
(as v is not free in (λv.M))
I Capture-avoiding:
(λv. u v)[u := v] 6≡ (λv. v v) (!!!)
(λv. u v)[u := v] ≡ (λw.u w)[u := v]
≡ (λw. v w)
Lambda Calculus Terms Substitution 14/30
Substitution: Please Take Care!
Substitution is tricky!
You have seen it before (in handling f.o.l. quantifiers)
Use the Barendregt Variable Convention:
rename bound variables so they don’t overlap with free variables.
Lambda Calculus Terms Substitution 15/30
Substitution Drives Computation
A General Programming Language Axiom:
When you apply a function to an argument, the result is
as if you substituted the actual argument for the formal
parameter and then performed the specified computation
For example, how do we figure out what f(3,5) will return?
int f(int x, int y)
{
return 2*x + y;
}
Dynamics Beta Reduction 16/30
Beta Reduction: λ-Terms Doing Things
Substitution of “actuals for formals” is the essence of
beta-reduction:
(λv.M) N −→β M[v := N]
Reduction can occur anywhere within a term.
Examples:
(λv. v) (λx. x v) −→β (λx. x v)
(λu. (λv. v z) (u z)) −→β (λu. (u z) z)
(λu. (λv. v u) (u z)) v z −→β (λw.w v) (v z) z
−→β (v z) v z
(λx. x x) (λy. y y) −→β (λy. y y) (λy. y y)
≡ (λx. x x) (λy. y y)
Dynamics Beta Reduction 17/30
Beta Reduction: λ-Terms Doing Things
Substitution of “actuals for formals” is the essence of
beta-reduction:
(λv.M) N −→β M[v := N]
Reduction can occur anywhere within a term.
Examples:
(λv. v) (λx. x v) −→β (λx. x v)
(λu. (λv. v z) (u z)) −→β (λu. (u z) z)
(λu. (λv. v u) (u z)) v z −→β (λw.w v) (v z) z
−→β (v z) v z
(λx. x x) (λy. y y) −→β (λy. y y) (λy. y y)
≡ (λx. x x) (λy. y y)
Dynamics Beta Reduction 17/30
Beta Reduction: λ-Terms Doing Things
Substitution of “actuals for formals” is the essence of
beta-reduction:
(λv.M) N −→β M[v := N]
Reduction can occur anywhere within a term.
Examples:
(λv. v) (λx. x v) −→β (λx. x v)
(λu. (λv. v z) (u z)) −→β (λu. (u z) z)
(λu. (λv. v u) (u z)) v z −→β (λw.w v) (v z) z
−→β (v z) v z
(λx. x x) (λy. y y) −→β (λy. y y) (λy. y y)
≡ (λx. x x) (λy. y y)
Dynamics Beta Reduction 17/30
Beta Reduction: λ-Terms Doing Things
Substitution of “actuals for formals” is the essence of
beta-reduction:
(λv.M) N −→β M[v := N]
Reduction can occur anywhere within a term.
Examples:
(λv. v) (λx. x v) −→β (λx. x v)
(λu. (λv. v z) (u z)) −→β (λu. (u z) z)
(λu. (λv. v u) (u z)) v z −→β (λw.w v) (v z) z
−→β (v z) v z
(λx. x x) (λy. y y) −→β (λy. y y) (λy. y y)
≡ (λx. x x) (λy. y y)
Dynamics Beta Reduction 17/30
Beta Reduction Rules and Notation
(λv.M) N −→β M[v := N]
M −→β M ′
M N −→β M ′ N N −→β N
′
M N −→β M N ′
M −→β M ′
(λv.M) −→β (λv.M ′)
Write M −→∗β N to mean M can take zero or more β-reduction
steps and evolve to N.
Write M −→+β N to mean M can take one or more β-reduction
steps and evolve to N.
Dynamics Beta Reduction 18/30
Beta Reduction Does It All!
Lambda Terms + Beta Reduction = All Computation
Any computation can be encoded in what we have just seen.
We will look at computational aspects of the λ-calculus in detail in
later lectures.
In particular, it is easy to encode
I Numbers
I Recursion
And that’s all you need.
Dynamics Beta Reduction 19/30
Eta Reduction
We can also add another computational rule, η-reduction:
v not free in M
(λv.M v) −→η M
(Can perform η-reduction anywhere within a term, as with β.)
We will later see how η ties into extensionality.
Eta-reduction and eta-expansion (!) also play a role in the
typed λ-calculus.
Dynamics Eta Reduction 20/30
Can Combine Beta and Eta
For example:
(λf. f x) (λy. g y)
−→βη (λf. f x) g
−→βη g x
Or:
(λf. f x) (λy. g y)
−→βη (λy. g y) x
−→βη g x (Eta and Beta coincide here)
Dynamics Eta Reduction 21/30
Can Combine Beta and Eta
For example:
(λf. f x) (λy. g y)
−→βη (λf. f x) g
−→βη g x
Or:
(λf. f x) (λy. g y)
−→βη (λy. g y) x
−→βη g x (Eta and Beta coincide here)
Dynamics Eta Reduction 21/30
Normal Forms
A normal form is a term that cannot be further reduced.
For example, (λx. g x) is a β-normal form,
but not an η-normal form.
It is reasonable to think of normal forms as values towards which
we want evaluation to proceed.
Dynamics Normal Forms 22/30
Normal Form Questions
It is natural to ask:
1. Does term M have a normal form?
2. Does M have more than one normal form?
And, we can ask these questions of all terms too.
Dynamics Normal Forms 23/30
Lambda Term Evaluation is Non-Deterministic
Recall:
M −→β M ′
M N −→β M ′ N N −→β N
′
M N −→β M N ′
Remember also:
(λx. x x) (λy. y y) −→β (λy. y y) (λy. y y)
Call (λx. x x) (λy. y y), the self-looping term, Ω.
Dynamics Evaluation Strategies 24/30
Infinite Loops (Depending on Evaluation Order)
Consider what (λx. y) Ω might do.
I If we keep evaluating the argument (Ω), we never stop:
(λx. y) Ω −→β (λx. y) Ω −→β (λx. y) Ω −→β · · ·
I If we apply the top-level function, substituting Ω for x we get:
(λx. y) Ω −→β y
Done!
This term ((λx. y) Ω) has one normal form (y), but not all
evaluation choices reach it.
Dynamics Evaluation Strategies 25/30
How Do Other Languages Do This?
int g l o b a l = 3;
unsigned f(void)
{
unsigned x = 0;
while (1) { x++; }
return x;
}
int g(unsigned i) { return g l o b a l; }
int main(void) { return g( f()); }
What happens in C?
Dynamics Evaluation Strategies 26/30
Evaluation Strategy #1: Applicative Order
Evaluate everything from the bottom up.
I I.e., in (λv.M) N work will start with M, passing to N and
performing the top-level β-reduction last
A function’s arguments (and the function itself) will be evaluated
before the argument is passed to the function.
Also known as strict evaluation.
(Used in Fortran, C, Pascal, Ada, SML, Java†. . . )
Causes (λx. y) Ω to go into an infinite loop.
Dynamics Evaluation Strategies 27/30
Evaluation Strategy #2: Normal Order
Evaluate top-down, left-to-right.
I With (λv.M) N, start by performing the β-reduction,
producing M[v := N]
I Find the top-most, left-most β-redex and reduce it.
I Keep going
This strategy is behind the lazy evaluation of languages like
Haskell.
Normal order evaluation will always terminate with a normal form
if a term has one. (Proof in Lecture 4)
Dynamics Evaluation Strategies 28/30
Strategy Rules
Write M −→n N for “M normal order reduces to N”.
Then:
(λv.M) N −→n M[v := N] M −→n M ′(λv.M) −→n (λv.M ′)
M −→n M ′ M not an abstraction
M N −→n M ′ N
N −→n N ′ M not an abstraction M in β-nf
M N −→n M N ′
Rules for applicative order evaluation will be an assignment
question.
Dynamics Evaluation Strategies 29/30
Summary
Lambda Terms:
I Variables, applications, abstractions
I Bound names, free names, alpha equivalence
I Substitution
Dynamic Behaviour:
I Beta reduction: computation through substitution
I Eta reduction
I Normal forms, and strategies for achieving them
Conclusion 30/30