Test an expression to see if it is c0 or not: find arguments (for numerals) which yield tru if no successors have been applied, and fls otherwise. i.e. iszero = λm.?.
c0 returns its second argument, make it tru will yield iszro c0 = tru All other numerals (where we want to return fls) applies s at least
Make s = λx.fls, ignoring its argument. Putting that together:
iszero = λm.m (λx.fls) tru
J. Carette (McMaster University) The Lambda Calculus Fall 2023
Testing it
(λm.m (λx.fls) tru) c0
→ c0 (λx .fls) tru
→ (λs .λz . z ) (λx .fls) tru
→ (λz. z) tru
J. Carette
(McMaster University)
The Lambda Calculus
The Mask of Zero
iszero c2 (λm.m (λx.fls) tru) c2
→ c2 (λx .fls) tru
→ (λs.λz. s (s z)) (λx.fls) tru
→ (λz . (λx .fls) ((λx .fls) z )) tru
→ (λx .fls) ((λx .fls) tru)
J. Carette (McMaster University)
The Lambda Calculus
Predecessor(!)
Testing to see if something is zero is relatively straightforward, but predecessor requires some cleverness.
In UAE, we defined pred as an annihilation operation over successors. In λ-Calculus, we essentially need to reconstruct our numeral, while
keeping a history of the previous value.
prd = λm.fst (m ss zz)
ss = λp.pair (snd p) (plus c1 (snd p)) zz = pair c0 c0
J. Carette (McMaster University) The Lambda Calculus
程序代写 CS代考 加微信: cstutorcs
Converting back and forth:
realbool = λb.b true false (5)
churchbool = λb.if b then tru else fls (6)
realnat = λcn.cn (λx.succ x) 0 churchnat = λn.λs.λz.applyN n s z
J. Carette (McMaster University) The Lambda Calculus
Fall 2023 5/18
Curious Constructions
Consider the Ω-Function:
Ω = (λx.x x)(λx.x x) (9) When you β-reduce Ω, you get Ω right back again!
(λx.x x)(λx.x x) → (λx.x x)(λx.x x) (10) Because these functions do not converge to a normal form in a finite number
of steps, they are known as divergent.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 6 / 18
Y-Combinator
The Y-Combinator encodes general recursion in the λ-Calculus.
Y = λf .(λx.f (x x)) (λx.f (x x)) (11)
Unfortunately, it only works under call by name. The following fixed-point combinator solves the problem of general recursion for the call by value evaluation strategy.
fix = λf .(λx.f (λy.x x y)) (λx.f (λy.x x y)) (12)
J. Carette (McMaster University) The Lambda Calculus Fall 2023 7 / 18
程序代写 CS代考 加QQ: 749389476
The factorial function:
n×(n−1)! n>0
We can encode it as follows:
g =λfct.λn.if n==0 then 1 else n×(fct(n−1)) (14)
factorial = fix g (15) To save time and energy, we are encoding this using the enriched calculus.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 8 / 18
Inductive Syntax of λ-Calculus
Let V be a countable set of variable names. The set of terms is the smallest set T such that:
2 t1∈T∧x∈V=⇒λx.t1∈T
3 t1,t2∈T=⇒t1t2∈T
Via this definition, we can define size and depth the same way as we did under UAE.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 9 / 18
Free Variables
The set of free variables of a term t, written FV(t) is defined as follows:
FV (λx.t1) FV (t1t2)
= FV (t1) \ {x}
= FV (t1) ∪ FV (t2)
J. Carette (McMaster University) The Lambda Calculus Fall 2023 10 / 18
Substitution
The intuitive (but wrong) definition:
[x7→s]x [x7→s]y
[x 7→ s]λy.t1 [x 7→ s](t1 t2)
λy.[x 7→ s]t1
([x 7→ s]t1) ([x 7→ s]t2)
J. Carette (McMaster University)
The Lambda Calculus
Why wrong?
This works reasonably well in most situations, such as the following:
[x 7→ (λz.z w)](λy.x) → λy.λz.z w (16)
Consider the following:
[x 7→ y](λx.x) → λx.y (17) This happens because we pass the substitution through lambdas
without checking first to see if the variable we’re replacing is bound!
J. Carette (McMaster University) The Lambda Calculus Fall 2023 12 / 18
浙大学霸代写 加微信 cstutorcs
Another try
If we fix the bit where we ignore bound vs. free variables…
This expression now evaluates the way we expect it to… [x 7→ y](λx.x) → λx.x
But the following expression doesn’t.
[x 7→ z](λz.x) → λz.z
When we sub in z, it becomes bound to λz. This is known as variable capture.
J. Carette (McMaster University) The Lambda Calculus
Accept No Substitutes!
In order to avoid having our variables captured, we might add the condition that, in order for a substitution to pass through a λ abstraction, the abstracted variable must not be in the set of free variables contained within the expression we are subbing in.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 14 / 18
Still wrong
Consider the following example:
[x 7→ y z](λy.x y) (20)
No substitution can be performed, even though it would be reasonable to expect one.
By relabelling y to some other arbitrary label, we can avoid the capture as well. For example:
[x 7→ y z](λy.x y) → [x 7→ y z](λw.x w) → (λw.y z w) (21)
J. Carette (McMaster University) The Lambda Calculus Fall 2023 15 / 18
Relabelling
By convention in λ-Calculus, terms that differ only in the names of bound variables are interchangeable in all contexts.
This is known as α-equivalence.
By working up to α, we can simplify our rules for substitution:
J. Carette (McMaster University) The Lambda Calculus Fall 2023 16 / 18
Operational Semantics of λ-Calculus
Here is the operational semantics of the CbV (call by value) λ-Calculus
Note that these are the semantics for the pure λ-Calculus.
J. Carette (McMaster University) The Lambda Calculus Fall 2023 17 / 18
Things of note
All lambda terms are values (and vice-versa)
One application rule (E-AppAbs), and two congruence rules, (E-App1)
and (E-App2).
Note how the placement of values controls the flow of execution.
We may only proceed with (E-App2) if t1 is a value, implying that (E-App1) is inapplicable.
The reason this strategy is called “call by value” is because the term being substituted in (E-AppAbs) must be a value.
J. Carette
(McMaster University) The Lambda Calculus Fall 2023 18 / 18