pdf.io >> Free >> Dan Deavours.pdf

Dan Deavours

 FileName: lambda.pdf
[previewonline]


 FileSize: 152 KB download
 Shared by: ittc_ku_edu 43 month ago
 Category: Free
 Report us: delete it


Abstract: Dan DeavoursLambda CalculusPage 1Dan DeavoursLambda Calculus• λ calculus is regarded as the theoretical foundation of functional programminglanguages

Dan Deavours
Lambda Calculus
Page 1
Dan Deavours
Lambda Calculus
• λ calculus is regarded as the theoretical foundation of functional programming
languages
• Like DFA or Turing machines is a model of computation, so is λ calculus.
• Developed in the 1930s
• Everything is a function. Arguments, return “values,” numbers, everything!
• If you’ve never seen it before, be prepared to be dazzled (or perplexed).
Page 2
Dan Deavours
Procedural Aabstraction
If you haven’t noticed before, functions are really a convenient form of abstraction.
x+∆
d −ex
E.g., dx f (x), where f (x) = ex is a nice way of writing lim∆→0 e ∆ .
E.g., Fact(7) = 7 · 6 · 5 · 4 · 3 · 2 · 1.
How do you describe Fact(n)?
Page 3
Dan Deavours
Functional Description
1 n=0
Fact(n) =
n · Fact(n − 1) otherwise
In English, “Fact(n) := if n = 0 then 1 else n · Fact(n − 1).”
In pseudoλ calculus:
Fact = λn. if n = 0 then 1 else n · Fact(n − 1)
Read: λn. · · · “the function that, for each n, yields · · ·.”
Page 4
Dan Deavours
Application
What then does Fact(0) mean?
The function λn. if n = 0 then 1 else n · Fact(n − 1) applied to the argument 0
I.e., the value that results when the bound variable n in the function body “if n = 0
then 1 else . . .” is replaced by 0.
I.e., “if 0 = 0 then 1 else . . .”
I.e., 1.
Page 5
Dan Deavours
Syntax
L, M, N ::= X V ariable
MN Application
λx.M Abstraction
Notation: application is left associative.
I.e., L M N = (L M )N .
Abstraction bodies extend as far right as possible.
I.e., λx.λy.x y x = λx.(λy.((x y)x)).
Don’t worry; when it’s not clear, we use lots of parentheses.
Page 6
Dan Deavours
Terms
For some λ expression λx.M , we say that x is bound in the body M .
How do you compute with λ calculus? Beta reductions!
(λx.M )N −→[N/x]M
Note: This is exactly what you “normally” do with functions anyway!
An expression can be reduced by replacing some subexpression of th eform
(λx.M )N , called a redex, by the result of substituting the argument N for the
bound variable x in the body M .
E.g., (λx. x y)(u v)−→u v y.
E.g., (λx.λy.x)z w−→(λy. z)w−→z.
We can write (λx.λy.x)z w−→∗ z.
Page 7
Dan Deavours
Similarity
This gives us an interesting way to compare two programs.
We say that M and N are betaconvertible, written M =β N , if they are identical, if
one reduces to the other, or both reduce to some third expression L.
(Formally the betaconversion relation =β is the reﬂexive, symmetric, transitive
closeure of betareduction.)
E.g., (λx.x)z =β (λx.λy.x)zw because
(λx.x)z−→z
(λx.λy.x)zw−→(λy.z)w−→z.
Page 8
Dan Deavours
Housecleaning
We need to be very careful with the substitution [N/x]M .
We say that a variable x is free in an expression M if x appears at some position in
M where it is not bound by an enclosing lambdaabstraction on x.
E.g., x is free in xy and λy.xy, but not free in λx.x or λz.λx.λy.xyz.
Rule:
FV(x) = {x}
FV(M N ) = FV(M ) ∪ FV(N )
FV(λx.M ) = FV(M ) \ {x}
Consider λx.x and λy.y . Intuitively, they are the same function, i.e., the function
that, when applied to N , returns N .
λx.M = λy.([y/x]M ) if y ∈ FV(M )
This rule is called the renaming of bound variables, or alpha conversion.
Page 9
Dan Deavours
Substitution Rules
Now, we can deﬁne substitution.
[N/x]x = N
I.e., substituting N for x in the expression consisting only of x itself yields N .
[N/x]z = z
I.e., to substitute N for x in the expression consisting only of some diﬀerent variable
z yields z.
[N/x](L M ) = ([N/x]L)([N/x]M )
I.e., to substitute N for x in an application L M , we substitute in M and L
separately.
[N/x](λz.M ) = λz.([N/x]M ) if z = x and z ∈ FV(N )
To substitute N for x in a lambda abstraction M , we substitute in the body of M
only when:
1. z is not the same as x, or
2. z is not one of the free variables of N .
Page 10
Dan Deavours
Substitution exception 1
For exception 1, consider (λx.λx.x)y−→λx.y?
(λx.λx.x)y −→ [y/x]λx.x “beta − reduction
= λx.[y/x]x illegal
= λx.y
Page 11
Dan Deavours
Substitution exception 2
For exception 2, consider:
(λx.λy.x)y −→ [y/x]λx.λy.x “beta − reduction
= λy.y illegal
Thus, technically speaking, the substition [N/x]M may be undeﬁned for some N , x,
and M , but it is always possible to change the names of the bound variables in N
and/or M so that the substion makes sense. E.g.,
(λx.λx.x)y −→ [y/x](λx.x)
= [y/x](λz.z)
= λz.z
= λx.x
Page 12
Dan Deavours
Everything (Part 1)
Syntax:
L, M, N ::= x variable
MN application
λx.M abstraction
Free variables:
FV(x) = {x}
FV(M N ) = FV(M ) ∪ FV(N )
FV(λx.M ) = FV(M ) \ {x}
Substitution:
[N/x] x = N
[N/x] z = z if z = x
[N/x] (L M ) = ([N/x]L)([N/x]M )
[N/x] (λz.M ) = λz.([N/x]M ) if z = x and z ∈ FV(N )
Page 13
Dan Deavours
Everything (Part 2)
Renaming of bound variables
λx.M = λy.([y/x]M ) if y ∈ FV(M )
Operational Semantics:
(λx.M )N −→[N/x]M functional application (“beta − reduction )
Page 14
Dan Deavours
Title
Don’t be fooled. The simple syntax of lambda calculus is remarkably powerful.
It may seem at ﬁrst that there are a number of deﬁciencies:
• No numbers
• Only single arguments
• Conditionals
• Booleans
• Iteration
Take heart! They’re there.
Page 15
Dan Deavours
Multiple arguments
Multiple arguments can be performed using a “trick” known as higherorder
functions, i.e., functions that return functions. (Not surprising in lambda calculus,
given that everything is a function.)
E.g., suppose we want a function F to take two parameters.
F = λ(x, y).M illegal, but intuitively desirable
Instead, we write
F = λx.λy.M
You would use F L M .
Read: F is a function that, given a value N for x, yields a function that, given a
valueL for y, yields the result.
To “execute” F:
FNL = (λx.λy.M )N L
−→ (λy.[N/x]M )L
−→ [L/y][N/x]M
Page 16
Dan Deavours
Currying
Transformation of multiple parameter functions into higher order functions is called
Currying, after Curry. It was actually invented by Sch¨nﬁnkel, but somehow the term
o
Sch¨nﬁnkeling hasn’t caught on.
o
Page 17
Dan Deavours
Booleans
Boolean values are, naturally, functions. The defnitions aren’t particularly useful
(and somewhat trivial); it’s how they’re used that lets them be booleans.
True = λt.λf.t
False = λt.λf.f
Neither of these functions have free variables, and thus are called combinators.
Combinators are inert with respect to substitution, i.e., [N/x]True = True.
The (important) implication of this is that the only way to interact with combinators
(booleans in particular) is through applying them to expressions.
Thus, we can write an iftheelse statement as follows:
If = λl.λm.λn.l m n
Think:
If
Page 18
Dan Deavours
A bit more iﬀy
Note: If L M N simply means L M N . In that sense, it is a trivial deﬁnition.
E.g.,
If True M N = (λl.λm.λn.l m n)True M N
−→ (λm.λn.True m n)M N
−→ (λn.True M n)N
−→ True M N
= (λt.λf.t)M N
−→ (λf.M )N
−→ M
Page 19
Dan Deavours
Boolean Operators
Boolean operators, such as AND, OR, XOR, NOT, etc. can be formed similarly.
And = λb. λc. b c False
E.g.,
And True X = X
And False X = False
Similarly,
Not = λb. b False True
Page 20
Dan Deavours
Pairs
Two “objects” can be encoded into a pair.
Pair = λf. λs. λb. b f s
To get each object back out,
Fst = λp. p T rue
Snd = λp. p F alse
Note notation: p is for pair, b is for boolean, f ﬁrst, s second.
Pair M N is a function that, when applied to a boolean b, applies b to M and N .
Page 21
Dan Deavours
Fst(P air M N ) = Fst((λf. λs. λb. b f s)M N )
−→ Fst((λs. λb. b M s)N )
−→ Fst(λb. b M N )
= (λb. b M N )True
−→ (λb. b M N )True
−→ True M N
−→∗ M
Page 22
Dan Deavours
Numbers
Natural numbers can be encoded using Church Numerals, written C0 , C1 , C2 , . . ..
Naturally, numbers are functions.
C0 = λz. λs. z
C1 = λz. λs. s z
C2 = λz. λs. s (s z)
C3 = λz. λs. s (s (s z))
Cn = λz. λs. s(. . . (s z) . . .)
n times
Each number n is represented by a combinator Cn , a function that takes two
arguments: z (zero) and s (successor), and applies s ntimes to z. Note that since
numbers are really functions, numbers can “do stuﬀ.”
Page 23
Dan Deavours
Addition
Plus = λm. λn. λz. λs. m (n z s) s
Plus is a function that takes two arguments (numbers) m and n, and yields a
function that takes two arguments: z and s, i.e., a number.
Notice that m is a number, i.e., a function that takes z and s. The z is (n z s), i.e.,
the number n. Then apply s mtimes more.
Page 24
Dan Deavours
Multiplication
Times = λm. λn. m C0 (Plus n)
Here, the “successor” function is (Plus n), and the “zero” function is really zero,
i.e., C0 . Apply (Plus n) mtimes to C0 .
Page 25
Dan Deavours
Test for zero
Testing for zero is an important (critical) function for computational completeness.
Strategy: give a number a z that is True and a s that, when applied to z one or
more times, yields False.
IsZero = λm .m True(λx. False)
Here, z = True, s = λx. False.
E.g.,
IsZeroC0 = (λm. mTrue (λx. False)) C0
−→ C0 True (λx. False)
= (λz. λs. z)True (λx. False)
−→ λs. True(λx. False)
−→ True
Page 26
Dan Deavours
Test for zero
Another example:
IsZero C1 = (λm. m True) (λx. F alse)) C1
−→ C1 True(λx. False)
= (λz. λs. s z)True (λx. False)
−→ (λs. s True)(λx. False)
−→ (λx. False) True
−→ False
Page 27
Dan Deavours
Subtraction (is hard)
First, we will deﬁne
Pred C0 = C0 ,
Pred Ci+1 = Ci
Let Z = Pair C0 C0
Let S = λp. P air(Snd p) (Plus (Snd p) C1 )
Then
Pred = λm. Fst (m Z S)
• Pred takes a number m and applies S mtimes to Z.
• S takes a pair (Ci , Cj ) and returns the pair (Cj , Cj+1 ).
• Applying S mtimes to Z yields (C0 , C0 ) if m = 0, or (Cm−1 , Cm ) if m > 0.
• Fst of (Cm−1 , Cm )−→∗ Cm−1 .
Page 28
Dan Deavours
Recursion
To perform recursive deﬁnitions (calculations), it is useful to deﬁne the socalled Y
combinator.
Y = λf. (λx. f (x x))(λx. f (xx))
This may look odd, but it has the very interesting (and important) property that
Y F =β F (Y F ), for any F !
YF = (λf. (λx. f (x x))(λx. f (x x)))F
−→ (λx. F (x x))(λx. F (x x))
−→ F ((λx. F (x x))(λx. F (x x)))
←− F ((λf. (λx. f (x x))(λx. f (x x)))F )
= F (Y F )
Page 29
Dan Deavours
Factorial
You can deﬁne the factorial function recursively:
if n = 0 then 1
else n · ( if n − 1 = 0 then 1
else (n − 1) · ( if n − 2 = 0 then 1
else (n − 2) · . . .))
F = YG
=β G(Y G)
=β G(G(Y G))
=β ...
Page 30
Dan Deavours
More on Factorial
Fact = λf. λn. If (IsZero n) C1 (Times n(f (Pred n)))
Factorial = Y Fact
Ok, but how do you know it works? What is 2!?
Page 31
Dan Deavours
Factorial Example
Factorial C2 = Y Fact C2
=β Fact(Y Fact) C2
=β (λFact. λn. If (IsZero n) C1 (Times n (Fact (Pred n))))(Y Fact)C2
=β (λn. If (IsZero n) C1 (Times n (Y Fact (Pred n)))) C2
=β If (IsZero C2 ) C1 (Times C2 (Y Fact (Pred C2 )))
=β If False C1 (Times C2 (Y Fact C1 ))
=β Times C2 (Y Fact C1 )
=β Times C2 (Factorial C1 )
Page 32
Dan Deavours
Other Useful Combinators
I = λx. x
K = λx. λy. x
S = λx. λy. λz. (x z) (y z)
I is the identity combinator.
K takes two arguments and throws away the second.
S “distributes” its third argument to both its ﬁrst and second.
Astonishing Fact: For any combinator N , there exists a combinator M such that
N =β M , and M can be writtten using only I, K, and S.
I.e., I, K, and S contain the full power of lambdaabstraction
E.g., False = K I.
Page 33
Dan Deavours
Notes
Not all expressions are reducable, and some depend on the strategy for reduction.
E.g.,
Ω = (λx. x x) (λx. x x)
Is similar to
10 GOTO 10
Page 34
 Related pdf books
 Oscillator Stability
 Efficient Searching with Linear Constraints
 Signal Flow Graphs
 Reading Assignment: pp. 6473
 85 Permanent Magnets and Magnetic Recording
 Unit 4 Requirements Analysis
 Voltage Regulators  KU ITTC
 11/4/2004 Electric Flux Density.doc 1/5
 No Slide Title
 SensorNet III Requirements lss B10124VSFV2
 EGEMEN K C˘ET INKAYA
 A Multipath Channel Estimation Algorithm using a Kalman filter.
 5.4 – The QuarterWave Transformer  KU ITTC
 Understanding Requirements for Developing Open Source ...
 The Rosetta MetaModel Framework
 The NonInverting Configuration lecture
 Design and Development of a One Gigasample per Second Radar Data
Download the ebook