Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 4

20 marca 2020

(2)

Tydzień temu: Liczebniki Churcha

c

_n

= n = λfx .f

ⁿ

(x ),

0 = λfx .x ; 1 = λfx .fx ; 2 = λfx .f (fx );

3 = λfx .f (f (fx )), etc.

(3)

Definable functions

A partial functionf : N^k −◦ N is λ-definable if there is a term F such that for all n₁, . . . , n_k ∈ N:

I If f (n1, . . . , nk) = m, then F n1. . . nk =β m;

I If f (n1, . . . , n_k) is undefined

then F n₁. . . n_k does not normalize.

Theorem

Every partial computable function is definable.

(4)

Definable functions

A partial functionf : N^k −◦ N is λ-definable if there is a term F such that for all n₁, . . . , n_k ∈ N:

I If f (n1, . . . , nk) = m, then F n1. . . nk =β m;

I If f (n1, . . . , n_k) is undefined

then F n₁. . . n_k does not normalize.

Theorem

Every partial computable function is definable.

(5)

Encoding a Turing Machine

We have a termNext s.t.

Next(code of C1) β (code of C₂), whenever the machine can move from C₁ to C₂.

The function computed by the machine is λ-definable as: λx .W (Init x )W,

where

W = λc.if Halt c then λw .Out c else λw .w (Next c)w .

(6)

Encoding a Turing Machine

The function computed by the machine is λ-definable as: λx .W (Init x )W,

where

W = λc.if Halt c then λw .Out c else λw .w (Next c)w .

(7)

Encoding a Turing Machine

The function computed by the machine is λ-definable as:

λx .W (Init x )W, where

(8)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

F = λx .W (Init x )W,

W = λc. if Halt c then λw .Out c else λw .w (Next c)w .

F n → W (Init n)W W C0W →

[if Halt C0 then λw .Out C0 elseλw .w (Next C0)w ]W [λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W → [if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W [λw .w (Next C1)w ]W [λw .w C²w ]W → W C2W →

· · · W C^mW → [if Halt Cm then λw .Out C_m else λw .w (Next C_m)w ]W [λw .Out C_m]W → Out C_m f(n).

(9)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

W = λc. if Halt c then λw .Out c else λw .w (Next c)w . F n → W (Init n)W W C0W →

[if Halt C0 then λw .Out C0 elseλw .w (Next C0)w ]W [λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W → [if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W [λw .w (Next C1)w ]W [λw .w C²w ]W → W C2W →

(10)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

[if Halt C₀ then λw .Out C₀ elseλw .w (Next C₀)w ]W

[λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W → [if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W [λw .w (Next C1)w ]W [λw .w C²w ]W → W C2W →

(11)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

[if Halt C₀ then λw .Out C₀ elseλw .w (Next C₀)w ]W [λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W →

[if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W [λw .w (Next C1)w ]W [λw .w C²w ]W → W C2W →

(12)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

[if Halt C₀ then λw .Out C₀ elseλw .w (Next C₀)w ]W [λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W → [if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W

[λw .w (Next C1)w ]W [λw .w C²w ]W → W C2W →

(13)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · ·

⇒ C

_m

[if Halt C₀ then λw .Out C₀ elseλw .w (Next C₀)w ]W [λw .w (Next C0)w ]W [λw .w C¹w ]W → W C1W → [if Halt C1 then λw .Out C₁ elseλw .w (Next C₁)w ]W [λw .w (Next C₁)w ]W [λw .w C2w ]W → W C₂W →

(14)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · · ⇒ C

_m

· · · W C^mW →

[if Halt Cm then λw .Out C_m else λw .w (Next C_m)w ]W [λw .Out C_m]W → Out C_m f(n).

(15)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · · ⇒ C

_m

· · · W C^mW → [if Halt Cm then λw .Out C_m else λw .w (Next C_m)w ]W

[λw .Out C_m]W → Out C_m f(n).

(16)

Computing: C

₀

⇒ C

₁

⇒ C

₂

⇒ · · · ⇒ C

_m

· · · W C^mW → [if Halt Cm then λw .Out C_m else λw .w (Next C_m)w ]W

(17)

Question

We have definedF = λx .W (Init x )W, and

W = λc. if Halt c then λw .Out c else λw .w (Next c)w . Suppose we replace this definition by:

W = λcw .if Halt c then Out c elsew (Next c)w . Will anything change?

Answer: yes, the term W C0W would never be SN.

(18)

Question

We have definedF = λx .W (Init x )W, and

W = λc. if Halt c then λw .Out c else λw .w (Next c)w . Suppose we replace this definition by:

W = λcw .if Halt c then Out c elsew (Next c)w . Will anything change?

(19)

Computability ⇔ Definability

Twierdzenie

A partial functionf : N −◦ Nis λ-definable if and only if it is partial computable.

Dowód (⇒):

Letf be λ-definable byF.

To computef (n) reduce F nto normal form.

(20)

Computability ⇔ Definability

Twierdzenie

Dowód (⇒):

Letf be λ-definable by F.

To computef (n) reduce F n to normal form.

(21)

Computability ⇔ Definability

Twierdzenie

Dowód (⇐):

Zał.f : N −◦ Njest częściowo obliczalna. We encode the appropriate Turing Machine, and then:

I If f (n) is defined thenF n reduces to f(n).

I Otherwise we have an infinite quasi-leftmost reduction: F n W C0W [λw .w C1w ]W → W C₁W

[λw .w C2w ]W → W C2W · · · ThereforeF n does not normalize.

(22)

Computability ⇔ Definability

Twierdzenie

Dowód (⇐): Zał. f : N −◦ Njest częściowo obliczalna.

We encode the appropriate Turing Machine, and then:

I Otherwise we have an infinite quasi-leftmost reduction: F n W C0W [λw .w C1w ]W → W C₁W

[λw .w C2w ]W → W C2W · · · ThereforeF n does not normalize.

(23)

Computability ⇔ Definability

Twierdzenie

Dowód (⇐): Zał. f : N −◦ Njest częściowo obliczalna.

We encode the appropriate Turing Machine, and then:

I Otherwise we have an infinite quasi-leftmost reduction:

F n W C0W [λw .w C1w ]W → W C₁W

(24)

The following are undecidable problems:

I GivenM and N, doesM β N hold?

I GivenM and N, doesM =_β N hold?

I GivenM, doesM normalize?

Proof: LetA ⊆ N be recursively enumerable, not recursive. Letχ_A be the partial characteristic function of A, i.e.,

χ_A(x ) =ifx ∈ A then0else undefined LetH lambda-define the function χ_A.

To decide ifn ∈ A, ask any of the questions:

I doesH n β 0 hold?

I doesH n =_β 0 hold?

I doesH n have a normal form?

(25)

The following are undecidable problems:

I GivenM and N, doesM β N hold?

I GivenM and N, doesM =_β N hold?

I GivenM, doesM normalize?

Proof: LetA ⊆ N be recursively enumerable, not recursive.

Letχ_A be the partial characteristic function of A, i.e., χ_A(x ) =ifx ∈ A then0else undefined LetH lambda-define the function χ_A.

To decide ifn ∈ A, ask any of the questions:

doesH n 0 hold?

(26)

Undecidability

The following problem is undecidable:

I GivenM, doesM ∈ SN hold?

Proof as before. To decide ifχ_A(n) is defined, ask ifH n is strongly normalizable.

But that requires a stronger result:

Every partial computable function is well-definable. Our coding has this property (proof omitted).

(27)

Undecidability

Every partial computable function is well-definable. Our coding has this property (proof omitted).

(28)

Undecidability

Every partial computable function is well-definable.

Our coding has this property (proof omitted).

(29)

Twierdzenie Rice’a

(30)

Some numbering tricks

Letn be the number of a term M. Write M forn.

This is the Church numeral for the number ofM.

There are computable functions app and num such that app(number of M)(number of N) = number of MN

num(n) = number of n. There are termsApp and Num such that

App M N =β MN and Num n =β n. Example: If the numeral2 = λfx. f (fx) has number 9, then num(2) = 9, 2 = 9, and Num 2 =_β 9.

Now if 2 is the number of some M then Num M =β M = 9. SoM is the Church numeral for. . .

the number of the numeral forthe number of M.

(31)

Some numbering tricks

This is the Church numeral for the number ofM. There are computable functionsapp and num such that

app(number of M)(number of N) = number of MN num(n) = number of n.

There are termsApp and Num such that

App M N =β MN and Num n =β n. Example: If the numeral2 = λfx. f (fx) has number 9, then num(2) = 9, 2 = 9, and Num 2 =_β 9.

(32)

Some numbering tricks

App M N =β MN and Num n =β n.

Example: If the numeral2 = λfx. f (fx) has number 9, then num(2) = 9, 2 = 9, and Num 2 =_β 9.

(33)

Some numbering tricks

Example: If the numeral2 = λfx. f (fx) has number 9, then num(2) = 9,

2 = 9, and Num 2 =_β 9.

(34)

Some numbering tricks

Example: If the numeral2 = λfx. f (fx) has number 9, then num(2) = 9, 2 = 9,

and Num 2 =_β 9.

(35)

Some numbering tricks

(36)

Some numbering tricks

SoM is the Church numeral for. . .

(37)

Some numbering tricks

(38)

Some numbering tricks

(39)

A fixed-point theorem

Theorem

For every termF, there is a term X such that F (X ) =_β X.

Proof

TakeX = Z Z, where Z = λx . F (App x (Num x )). Then: X = Z Z =_β F (App Z (Num Z )) =_β

F (App Z Z ) =_β F (Z Z ) = F (X ).

(Compare X = Z Z to Yf = (λx. f (xx))(λx. f (xx)).)

(40)

A fixed-point theorem

Theorem

Proof

TakeX = Z Z, where Z = λx . F (App x (Num x )).

Then: X = Z Z =_β F (App Z (Num Z )) =_β

F (App Z Z ) =_β F (Z Z ) = F (X ).

(41)

A fixed-point theorem

Theorem

Proof

TakeX = Z Z, where Z = λx . F (App x (Num x )). Then:

X = Z Z =_β F (App Z (Num Z )) =_β

F (App Z Z ) =_β F (Z Z ) = F (X ).

(42)

A fixed-point theorem

Theorem

Proof

TakeX = Z Z, where Z = λx . F (App x (Num x )). Then:

X = Z Z =_β F (App Z (Num Z )) =_β

F (App Z Z ) =_β F (Z Z ) = F (X ).

(43)

Rice’s theorem (Scott)

Theorem

LetAbe a set of λ-terms, which is:

I Nontrivial, i.e., not empty and not full;

I Closed under =_β.

ThenA is undecidable (as a set of numbers).

Warning: Not every interesting set is closed under =_β. For instance, the set SN and sets of typable terms.

(44)

Rice’s theorem (Scott)

Theorem

(45)

Rice’s theorem (Scott)

Theorem

(46)

Proof idea

SupposeAis decidable, nontrivial, and closed under =_β.

We prove that there is no lambda-term F such that: FM =_β 0, for M ∈ A and FM =_β 1, for M 6∈ A. (If such anF existed, the set Awould be decidable.)

(But otherwise it is not enough.) TakeM₁ ∈ A, M₂ 6∈ Aand define

G = λx . if zero(Fx ) then M₂ else M₁. LetN = YG. Then G (N) =_β N.

If N ∈ A then N =_β G (N) =_β M₂ 6∈ A.

If N 6∈ A then N =_β G (N) =_β M₁ ∈ A, contradiction.

(47)

Proof idea

SupposeAis decidable, nontrivial, and closed under =_β. We prove that there is no lambda-term F such that:

FM =_β 0, for M ∈ A and FM =_β 1, for M 6∈ A.

(If such anF existed, the set Awould be decidable.) (But otherwise it is not enough.)

TakeM₁ ∈ A, M₂ 6∈ Aand define

(48)

Proof idea

(49)

Proof idea

G = λx . if zero(Fx ) then M₂ else M₁.

LetN = YG. Then G (N) =_β N. If N ∈ A then N =_β G (N) =_β M₂ 6∈ A.

(50)

Proof idea

(51)

Proof idea

If N ∈ A then N = G (N) = M 6∈ A.

(52)

Proof idea

If N ∈ A then N = G (N) = M 6∈ A.

(53)

Proof of Rice’s theorem

SupposeAis decidable, nontrivial, and closed under =_β.

LetF define the total characterictic function of A:

F M =_β 0, for M ∈ A and F M =_β 1, for M 6∈ A. TakeM₁ ∈ A, M₂ 6∈ Aand define

G = λx . if zero(Fx ) then M2 else M1. LetN be such thatG (N) =_β N.

If N 6∈ A then N =β G (N) =β M1 ∈ A, contradiction.

(54)

Proof of Rice’s theorem

SupposeAis decidable, nontrivial, and closed under =_β. LetF define the total characterictic function of A:

F M =_β 0, for M ∈ A and F M =_β 1, for M 6∈ A.

(55)

Proof of Rice’s theorem

G = λx . if zero(Fx ) then M2 else M1.

LetN be such thatG (N) =_β N. If N ∈ A then N =_β G (N) =_β M₂ 6∈ A.

(56)

Proof of Rice’s theorem

(57)

Proof of Rice’s theorem

(58)

Proof of Rice’s theorem

(59)

Równość w rachunku lambda

(60)

Adding equational axioms

Example 1:

Recall that 1 = λfx.fx. Add the axiomI = 1 to the equational theory of λ-calculus.

Then, for everyM, one proves:

M = IM = 1M = λx . Mx.

Example 2:

Now add the axiomK = S. Then, for everyM, one proves:

M = SI(KM)I = KI(KM)I = I. This extension is inconsistent.

(61)

Adding equational axioms

Example 1:

M = IM = 1M = λx . Mx.

Example 2:

Now add the axiomK = S. Then, for everyM, one proves:

(62)

Adding equational axioms

Example 1:

M = IM = 1M = λx . Mx.

Example 2:

Now add the axiom K = S.

(63)

Adding equational axioms

Example 1:

M = IM = 1M = λx . Mx.

Example 2:

Now add the axiom K = S.

(64)

Böhm’s Theorem

LetM, N be β-normal combinators with M 6=_βη N. ThenM ~P =_β trueand N ~P =_β false, for some P.~

Moral: Any consistent lambda-theory must discriminate between beta-eta normal forms.

(65)

Böhm’s Theorem

LetM, N be β-normal combinators with M 6=_βη N. ThenM ~P =_β trueand N ~P =_β false, for some P.~

Moral: Any consistent lambda-theory must discriminate between beta-eta normal forms.

(66)

Böhm Trees (finite case)

λxy . x λxy . x

λz. x y λzv . x y

z y z x v

M = λxy .x (λz.xzy )y N = λxy .x (λzv .xzxv )y

(67)

Böhm Trees: the difference

λxy . x λxy . x

λz. x y λzv . x y

z y z x v

M = λxy .x (λz.xzy)y N = λxy .x (λzv .xzxv )y

Trick: Applying M to λuv . hu, v igives λy . hλz.hz, y i, y i. And components can be extracted from a pair.

(68)

Böhm Trees: the difference

λxy . x λxy . x

λz. x y λzv . x y

z y z x v

(69)

Discriminating terms

Applying M and N to P = λuv . hu, v i, then to any Q yields: hλz.hz, Qi, Qi hλzv .hz, Piv , Qi

Next appply both to true, I, false to obtain:

λz.hz, Qi λzv .hz, Piv

hI, Qi λv . hI, Piv

Q P = λuv .hu, v i

ChooseQ = λuvw . true and apply both sides tofalse, I, true:

true false.

(70)

Discriminating terms

M = λxy .x (λz.xzy)y N = λxy .x (λzv .xzxv )y Applying M and N to P = λuv . hu, v i, then to any Q yields:

hλz.hz, Qi, Qi hλzv .hz, Piv , Qi

Next appply both to true, I, false to obtain:

Q P = λuv .hu, v i

true false.

(71)

Discriminating terms

hλz.hz, Qi, Qi hλzv .hz, Piv , Qi Next appply both to true, I, false to obtain:

Q P = λuv .hu, v i

true false.

(72)

Discriminating terms

Q P = λuv .hu, v i

true false.

(73)

Discriminating terms

Q P = λuv .hu, v i

true false.

(74)

Discriminating terms

Q P = λuv .hu, v i

true false.

(75)

Discriminating terms

Q P = λuv .hu, v i

(76)

Twierdzenie Böhma: szkic dowodu

I Tuple creation operator

T_p = λx1. . . x_p. hx1, . . . , x_pi = λx1. . . x_pλf . fx1. . . x_p.

I SubstitutionS = [x_i := T_p_i]_{i =1,...,n} is an m-substitution, whenp₁, . . . , p_n> m, and all p_is are different.

I TermsM i N arem-discriminable, when for every m-substitution S there are combinators ~L with:

M[S ]~L β true and N[S ]~L β false.

(77)

Twierdzenie Böhma: szkic dowodu

M[S ]~L β true and N[S ]~L β false.

(78)

Twierdzenie Böhma: szkic dowodu

M[S ]~L true and N[S ]~L false.

(79)

Twierdzenie Böhma: main lemma

If M i N are normal and M 6=βη N,

then M i N arem-discriminable for almost everym.

Czyli:

for every m-substitution S, there are ~L, s.t.

M[S ]~L β true oraz N[S ]~L β false.

(80)

Twierdzenie Böhma: main lemma

If M i N are normal and M 6=βη N,

Czyli:

for everym-substitution S, there are ~L, s.t.

M[S ]~L β true oraz N[S ]~L β false.

(81)

Twierdzenie Böhma: main lemma

If M i N are normal and M 6=_βη N,

Proof: Induction with respect to sum of lengths ofM, N. W.o.l.o.g., M = xP1. . . Pk and N = yQ1. . . Q`. Indeed:

I to discriminateλx M iλx N means to discriminate M iN;

I a missing lambda can be added: take λx Mx forM.

(82)

Twierdzenie Böhma: main lemma

Proof: Induction with respect to sum of lengths ofM, N. W.o.l.o.g., M = xP1. . . P_k and N = yQ1. . . Q_`. Indeed:

I to discriminateλx M iλx N means to discriminateM iN;

I a missing lambda can be added: take λx Mx forM.

(83)

Twierdzenie Böhma: main lemma

Dowód: Induction with respect to sum of lengths of M, N. W.o.l.o.g., M = xP1. . . P_k and N = yQ1. . . Q_`. Then:

M[S ] = T_pP₁[S ]...P_k[S ] β λ~uhP₁[S ], ..., P_k[S ], u₁, ..., u_p−ki N[S ] = T_qQ₁[S ]...Q_`[S ] β λ~v hQ₁[S ], ..., Q_`[S ], v₁, ..., v_q−`i Base cases: x 6= y or x = y but k 6= `: exercise.

If x = y and k = ` then P_i 6=_βη Q_i, for some i. Project on the i-th coordinate and apply induction.

(84)

Twierdzenie Böhma: main lemma

Dowód: Induction with respect to sum of lengths of M, N.

W.o.l.o.g., M = xP1. . . P_k and N = yQ1. . . Q_`. Then:

M[S ] = T_pP₁[S ]...P_k[S ] β λ~uhP₁[S ], ..., P_k[S ], u₁, ..., u_p−ki N[S ] = T_qQ₁[S ]...Q_`[S ] β λ~v hQ₁[S ], ..., Q_`[S ], v₁, ..., v_q−`i

Base cases: x 6= y or x = y but k 6= `: exercise. If x = y and k = ` then P_i 6=_βη Q_i, for some i. Project on the i-th coordinate and apply induction.

(85)

Twierdzenie Böhma: main lemma

If x = y and k = ` then P_i 6=_βη Q_i, for some i. Project on the i-th coordinate and apply induction.

(86)

Twierdzenie Böhma: main lemma

If x = y and k = ` then P_i 6=_βη Q_i, for some i. Project on the -th coordinate and apply induction.

(87)

The standard theory

(88)

The Meaning of “Value” and “Undefined”

First idea: Value = Normal form.

Undefined = without normal form.

Can we identify all such terms?

No: for instance λx .x KΩ = λx .x SΩ implies K = S (apply both toK).

Moral: A term without normal form can still behave in a well-defined way. In a sense it has a “value”. Better idea: Value = Head normal form. Undefined = without head normal form.

(89)

The Meaning of “Value” and “Undefined”

No: for instance λx .x KΩ = λx .x SΩ implies K = S (apply both toK).

(90)

The Meaning of “Value” and “Undefined”

No: for instance λx .x KΩ = λx .x SΩ impliesK = S (apply both toK).

(91)

The Meaning of “Value” and “Undefined”

Moral: A term without normal form can still behave in a well-defined way. In a sense it has a “value”.

Better idea: Value = Head normal form. Undefined = without head normal form.

(92)

The Meaning of “Value” and “Undefined”

Moral: A term without normal form can still behave in a well-defined way. In a sense it has a “value”.

(93)

Solvability

A closed term is solvable iff M ~P =_β I, for some closed P~. If FV(M) = ~x then M is solvable iff λ~x M is solvable.

Theorem

A term is solvable iff it has a head normal form. Proof for closed terms:

(⇒) IfM ~P =β I then M ~P ^β I. If M ~P head normalizes then alsoM must head normalize.

(⇐) IfM =_β λx1x2. . . x_n.x_iR1. . . R_m then MP . . . P =_β I, forP = λy₁. . . y_m.I.

(94)

Solvability

Theorem

A term is solvable iff it has a head normal form.

Proof for closed terms:

(⇐) IfM =_β λx1x2. . . x_n.x_iR1. . . R_m then MP . . . P =_β I, forP = λy₁. . . y_m.I.

(95)

Solvability

Theorem

A term is solvable iff it has a head normal form.

Proof for closed terms:

(⇐) IfM =_β λx1x2. . . x_n.x_iR1. . . R_m then MP . . . P =_β I,

(96)

The standard theory

We identify all unsolvable terms as “undefined”.

Which solvable terms may be now be consistently identified?

We cannot classify terms by their head normal forms. Too many of them!

We can onlyobserve their behaviour.

(97)

The standard theory

We cannot classify terms by their head normal forms.

Too many of them!

(98)

The standard theory

We cannot classify terms by their head normal forms.

Too many of them!

(99)

Observational equivalence

TermsM, N with FV(M) ∪FV(N) = ~x, are observationally equivalent (M ≡ N) when, for all closed P:

P(λ~x .M) is solvable ⇐⇒ P(λ~x .N) is solvable

Put it differently: for any “context” C [ ]:

C [M] is solvable ⇐⇒ C [N] is solvable Note: If M =_η N then M ≡ N.

(100)

Observational equivalence

P(λ~x .M) is solvable ⇐⇒ P(λ~x .N) is solvable Put it differently: for any “context” C [ ]:

C [M] is solvable ⇐⇒ C [N] is solvable

Note: If M =_η N then M ≡ N.

(101)

Observational equivalence

P(λ~x .M) is solvable ⇐⇒ P(λ~x .N) is solvable Put it differently: for any “context” C [ ]:

C [M] is solvable ⇐⇒ C [N] is solvable Note: If M =_η N then M ≡ N.

(102)

Böhm Trees

BT (λ~x .yP1. . . P_n) = λ~x . y

BT (P1) BT (P2) . . . BT (P_n)

(103)

Example: J = Y(λfxy . x(fy ))

Write Φfor λfxy . x (fy )). Then:

J = YΦ =_β ΦJ

=_β λxy₀. x (Jy₀) =_β λxy₀. x (ΦJy₀)

=β λxy0. x (λy1. y0(Jy1)) =β λxy0. x (λy1. y0(ΦJy1)) =β . . .

The treeBT (J) consists of one infinite path: λxy0. x ——λy1. y0——λy2. y1——λy3. y2—— · · ·

(104)

Example: J = Y(λfxy . x(fy ))

J = YΦ =_β ΦJ =_β λxy₀. x (Jy₀)

=_β λxy₀. x (ΦJy₀)

(105)

Example: J = Y(λfxy . x(fy ))

J = YΦ =_β ΦJ =_β λxy₀. x (Jy₀) =_β λxy₀. x (ΦJy₀)

(106)

Example: J = Y(λfxy . x(fy ))

=β λxy0. x (λy1. y0(Jy1))

=β λxy0. x (λy1. y0(ΦJy1)) =β . . .

(107)