Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 3

13 marca 2020

(2)

Rachunek λ-I

(3)

The λI-calculus

The λI-terms:

– variables;

– applications (MN), where M and N are λI-terms;

– abstractions (λx M), where M is a λI-term, and x ∈FV(M).

TermsS = λxyz.xz(yz) and I = λx.x are λI-terms, but K = λxy .x is not.

(4)

Question

Are λI-terms closed under reductions?

Yes, ifM →_βη N, and M is a λI-term, then so is N.

(5)

Question

Are λI-terms closed under reductions?

Yes, ifM →_βη N, and M is a λI-term, then so is N.

(6)

Theorem: If a λI-term has a normal form then it is SN.

(Write→^` for leftmost beta-reduction.)

Lemma: If M ∈ λI and M →^` N ∈ SNthen M ∈ SN.

Proof: Induction wrt the length of the normal form ofN. Case 1: M = λ~x . yR₁R₂. . . R_k. Then N = λ~x . yR₁⁰ . . . R_k⁰, with Ri → R_i⁰, for some i, and Ri = R_i⁰, otherwise.

Since N ∈ SN, alsoR_i⁰ ∈ SN, with shorter normal form. Thus all R_i are SN, and so isM.

(7)

Theorem: If a λI-term has a normal form then it is SN.

(8)

Theorem: If a λI-term has a normal form then it is SN.

Proof: Induction wrt the length of the normal form ofN.

Case 1: M = λ~x . yR₁R₂. . . R_k. Then N = λ~x . yR₁⁰ . . . R_k⁰, with Ri → R_i⁰, for some i, and Ri = R_i⁰, otherwise.

(9)

Theorem: If a λI-term has a normal form then it is SN.

(10)

Theorem: If a λI-term has a normal form then it is SN.

Since N ∈ SN, alsoR_i⁰ ∈ SN, with shorter normal form.

Thus all R_i are SN, and so isM.

(11)

Theorem: If a λI-term has a normal form then it is SN.

Proof: Induction wrt the length of the normal form ofN.

Case 2:

M = λ~x . (λy P)QR1. . . Rk →_β λ~x . P[y := Q]R1. . . Rk = N. All terms P, Q, R₁, . . . , R_k are SN. Therefore internal

reductions ofM must terminate, and otherwise we have: M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · · ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(12)

Theorem: If a λI-term has a normal form then it is SN.

Proof: Induction wrt the length of the normal form ofN. Case 2:

M = λ~x . (λy P)QR1. . . Rk →β λ~x . P[y := Q]R1. . . Rk = N.

All terms P, Q, R₁, . . . , R_k are SN. Therefore internal reductions ofM must terminate, and otherwise we have: M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · · ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(13)

Theorem: If a λI-term has a normal form then it is SN.

M = λ~x . (λy P)QR1. . . Rk →β λ~x . P[y := Q]R1. . . Rk = N. All terms P, Q, R₁, . . . , R_k are SN.

Therefore internal reductions ofM must terminate, and otherwise we have: M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · · ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(14)

Theorem: If a λI-term has a normal form then it is SN.

M = λ~x . (λy P)QR1. . . Rk →β λ~x . P[y := Q]R1. . . Rk = N. All terms P, Q, R₁, . . . , R_k are SN. Therefore internal

reductions ofM must terminate,

and otherwise we have: M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · · ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(15)

Theorem: If a λI-term has a normal form then it is SN.

reductions ofM must terminate, and otherwise we have:

M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · ·

ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(16)

Theorem: If a λI-term has a normal form then it is SN.

reductions ofM must terminate, and otherwise we have:

M λ~x. (λy Pⁱ ⁰)Q⁰R₁⁰...R_k⁰ → λ~^h x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰ · · · ButN β λ~x . P⁰[y := Q⁰]R₁⁰ . . . R_k⁰, and N is SN.

(17)

Question

Does the proof use the assumption thatM is a lambda-I-term?

Where?

Yes, otherwiseQ is not necessarily normal.

(18)

Question

Does the proof use the assumption thatM is a lambda-I-term?

Where?

Yes, otherwiseQ is not necessarily normal.

(19)

Theorem: If a λI-term has a normal form then it is SN.

Proof: LetM ∈ λI have normal form M⁰.

ThenM ^` M⁰ ∈ SN.

By induction wrt number of steps show thatM is SN.

(20)

Theorem: If a λI-term has a normal form then it is SN.

Proof: LetM ∈ λI have normal form M⁰. ThenM ^` M⁰ ∈ SN.

(21)

Theorem: If a λI-term has a normal form then it is SN.

Proof: LetM ∈ λI have normal form M⁰. ThenM ^` M⁰ ∈ SN.

(22)

Siła wyrazu / Expressive power

(23)

Curry’s fixed point combinator Y

Y = λf . (λx .f (xx ))(λx .f (xx ))

Fact: YF =_β F (YF ), for every F.

Proof: YF →β (λx .F (xx ))(λx .F (xx )) →_β

F ((λx .F (xx ))(λx .F (xx ))) _β← F (YF )

(24)

Curry’s fixed point combinator Y

Y = λf . (λx .f (xx ))(λx .f (xx ))

Proof: YF →β (λx .F (xx ))(λx .F (xx )) →_β

(25)

Curry’s fixed point combinator Y

Y = λf . (λx .f (xx ))(λx .f (xx ))

Proof: YF →β (λx .F (xx ))(λx .F (xx )) →β

(26)

Comment

Lambda calculus is a fantastic world: every function has a fixpoint (every equationX = Anything (X ) has a solution)!

The moral sense is: every recursive definition is well-formed.

The price we pay for it is non-termination.

(27)

YF =

_β

F (YF )

Example: Find an M such that Mxy =_β MxxyM.

Solution: No problem, M = Y(λm λxy . mxxym).

(28)

YF =

_β

F (YF )

Example: Find an M such that Mxy =_β MxxyM.

Solution: No problem, M = Y(λm λxy . mxxym).

(29)

Turing’s fixed-point combinator

Θ = (λxf . f (xxf ))(λxf . f (xxf ))

Fact: ΘF β F (ΘF ), for all F .

Proof: ΘF = (λxf . f (xxf ))(λxf . f (xxf ))F →_β (λf . f ((λxf . f (xxf ))(λxf . f (xxf ))f )F →_β F ((λxf . f (xxf ))(λxf . f (xxf ))F ) = F (ΘF ) Note the β rather than =_β.

(30)

Turing’s fixed-point combinator

Θ = (λxf . f (xxf ))(λxf . f (xxf ))

(31)

Turing’s fixed-point combinator

Θ = (λxf . f (xxf ))(λxf . f (xxf ))

Proof: ΘF = (λxf . f (xxf ))(λxf . f (xxf ))F →_β (λf . f ((λxf . f (xxf ))(λxf . f (xxf ))f )F →_β F ((λxf . f (xxf ))(λxf . f (xxf ))F ) = F (ΘF )

Note the β rather than =_β.

(32)

Turing’s fixed-point combinator

Θ = (λxf . f (xxf ))(λxf . f (xxf ))

(33)

Example

Consider a combinator day = hour hour · · · hour, where each hour is defined as

λabcdefghijklmnopstuwyzr . r (itisafikspointcombinator ).

How manyhours should a day have to be a fixpoint combinator, i.e., to satisfy hour F =β F (hour F )?

Define a Polish or Spanish example.

(34)

Problems

1. Is there a term M such that M =_β MSM ? 2. Can you solve non-fix-point equations like

MxxM =_β MxM ?

3. Can you solve systems of equations with 2 or more unknowns like {P = QSP, Q = PKQP}?

4. Can you solve any equation at all?

5. What are the fixpoints of the operator SI (where S and I are the standard combinators)?

6. Is there a fixpoint combinator in normal form?

7. IsY beta-equal to Θ?

(35)

Conditional

true = λxy .x false = λxy .y if P then Q else R = PQR.

It works:

if true then Q else R β Q if false then Q else R β R.

(36)

Ćwiczenie: Zdefiniować operacje logiczne

Define Boolean logic conjectives: ∨, ∧, →, ¬ as λ-terms.

For example, define a term C so that

C true false =_β C false true =_β C false false = false C true true =β true

Possible solution: C = λpd . p(d true false)false

(37)

Ćwiczenie: Zdefiniować operacje logiczne

Define Boolean logic conjectives: ∨, ∧, →, ¬ as λ-terms.

For example, define a term C so that

C true false =_β C false true =_β C false false = false C true true =β true

Possible solution: C = λpd . p(d true false)false

(38)

A generalization: finite sets

Coding elements of a finite set {a1, . . . , a_n}:

a_i := λx₁. . . x_n. x_i

Selection operator:

case a of (F₁, . . . , F_n) := aF₁. . . F_n

It works:

case a_i of (F1, . . . , F_n) β F_i

(39)

A generalization: finite sets

a_i := λx₁. . . x_n. x_i

Selection operator:

case a of (F₁, . . . , F_n) := aF₁. . . F_n

It works:

(40)

A generalization: finite sets

a_i := λx₁. . . x_n. x_i

Selection operator:

case a of (F1, . . . , F_n) := aF₁. . . F_n

It works:

(41)

A generalization: finite sets

a_i := λx₁. . . x_n. x_i

Selection operator:

case a of (F1, . . . , F_n) := aF₁. . . F_n

It works:

(42)

Ordered pair

Pair = Boolean selector:

hM, Ni = λx .xMN;

π_i = λx₁x₂.x_i (i = 1, 2);

Π_i = λp. pπ_i (i = 1, 2).

It works:

Π₁hM, Ni →_β hM, Niπ₁ β M.

(43)

Ordered pair

Pair = Boolean selector:

hM, Ni = λx .xMN;

π_i = λx₁x₂.x_i (i = 1, 2);

Π_i = λp. pπ_i (i = 1, 2).

It works:

Π₁hM, Ni →_β hM, Niπ₁ β M.

(44)

Question

Will this work: hΠ₁M, Π₂Mi =_β M?

Not when M is not a pair; take e.g. M = x.

Comment: This pairing is not surjective. And one cannot do better: Church-Rosser fails with surjective pairing!

Note the similarity with eta.

(45)

Question

(46)

Question

(47)

Question

(48)

Ordered tuples

Tuple = Selector:

hM₁, . . . , M_ni = λx .xM₁. . . M_n;

π_i = λx1. . . x_n.x_i (i = 1, . . . , n);

Π_i = λt. tπ_i (i = 1, . . . , n).

It works:

Π_ihM₁, . . . , M_ni β M_i

(49)

Ordered tuples

Tuple = Selector:

hM₁, . . . , M_ni = λx .xM₁. . . M_n;

π_i = λx1. . . x_n.x_i (i = 1, . . . , n);

Π_i = λt. tπ_i (i = 1, . . . , n).

It works:

Π_ihM₁, . . . , M_ni β M_i

(50)

Church’s numerals

c

_n

= n = λfx .f

ⁿ

(x ),

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

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

(51)

Definable functions

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

I If f (n₁, . . . , n_k) = m, then F n₁. . . n_k =_β m;

I If f (n₁, . . . , n_k) is undefined

then F n1. . . n_k does not normalize.

FunctionF is well-definable when, in addition:

I If f (n₁, . . . , n_k) is defined thenF n₁. . . n_k ∈ SN.

(52)

Definable functions

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

I If f (n₁, . . . , n_k) = m, then F n₁. . . n_k =_β m;

I If f (n₁, . . . , n_k) is undefined

then F n1. . . n_k does not normalize.

FunctionF is well-definable when, in addition:

I If f (n₁, . . . , n_k) is defined thenF n₁. . . n_k ∈ SN.

(53)

Comment

1. There are other definitions of lambda-definability.

They may slightly differ in the undefined case.

But the main results are the same.

2. The notion of “well definable” is not as common, but it proves technically useful.

(54)

Some well-definable functions

I Successor: succ = λnfx.f (nfx);

We have succ n β n + 1, please check.

Now try to define addition!

I Addition: add = λmnfx.mf (nfx);

I Multiplication: mult = λmnfx.m(nf )x;

I Exponentiation: exp = λmnfx.mnfx;

I Test for zero: zero = λm.m(λy .false)true;

I Constant zero (with k arguments): Zk = λm₁. . . m_k.0;

I Projection on the i -th coordinate: Πⁱ_k = λm₁. . . m_k.m_i.

(55)

Some well-definable functions

(56)

Some well-definable functions

(57)

Some well-definable functions

I Multiplication:

mult = λmnfx.m(nf )x;

(58)

Some well-definable functions

(59)

Some well-definable functions

I Exponentiation:

exp = λmnfx.mnfx;

(60)

Some well-definable functions

(61)

Some well-definable functions

I Test for zero:

zero = λm.m(λy .false)true;

(62)

Some well-definable functions

(63)

Some well-definable functions

I Constant zero (with k arguments):

Zk = λm₁. . . m_k.0;

(64)

Some well-definable functions

(65)

Some well-definable functions

Πⁱ_k = λm₁. . . m_k.m_i.

(66)

Some well-definable functions

I Projection on the i -th coordinate: Πⁱ = λm . . . m .m.

(67)

A challenge: predecessor

p(n + 1) = n, p(0) = 0

Diggression: They say Kleene invented this definition while his tooth was being extracted.

And that Church formulated Church Thesis when Kleene came back from the dentist’s.

Because this construction generalizes to all primitive recursive functions.

(68)

A challenge: predecessor

p(n + 1) = n, p(0) = 0

(69)

A challenge: predecessor

p(n + 1) = n, p(0) = 0

(70)

A challenge: predecessor

p(n + 1) = n, p(0) = 0

(71)

Predecessor is definable

p(n + 1) = n, p(0) = 0

Step = λp.hsucc(pπ1), pπ₁i pred = λn. (n Steph0, 0i)π2

How it works:

Steph0, 0i β h1, 0i Steph1, 0i β h2, 1i Steph2, 1i β h3, 2i,

and so on. (Evaluate pred 4.)

(72)

Predecessor is definable

p(n + 1) = n, p(0) = 0

Step = λp.hsucc(pπ1), pπ₁i pred = λn. (n Steph0, 0i)π₂

How it works:

(73)

Predecessor is definable

p(n + 1) = n, p(0) = 0

How it works:

(74)

Predecessor is definable

p(n + 1) = n, p(0) = 0

How it works:

Steph0, 0i β h1, 0i

Steph1, 0i β h2, 1i Steph2, 1i β h3, 2i,

(75)

Predecessor is definable

p(n + 1) = n, p(0) = 0

How it works:

Steph0, 0i β h1, 0i Steph1, 0i β h2, 1i

Steph2, 1i β h3, 2i,

(76)

Predecessor is definable

p(n + 1) = n, p(0) = 0

How it works:

(77)

Predecessor is definable

p(n + 1) = n, p(0) = 0

How it works:

(78)

Problems

Some of the problems have solutions in the file zadlam.

Try them without looking at the solutions.

1. Define the functionn 7→ 2n²+ 2n + 4.

2. Letf (0, x ) = g (x ) and f (n + 1, x ) = h(n, x , f (n, x )).

Assumeh and g are lambda-definable, show how to lambda-define f.

3. Define the functionn 7→ 2n²− 2n + 4.

4. Define equalityEq so that Eq m n =_β 0 iff m = n.

5. LetC = (λFxy . xF (λz. 1)(yF (λz. 0)))(λfg .gf ).

What is the function from N² to N defined by C?

(79)

Nierozstrzygalność / Undecidability

(80)

Turing machine

We consider deterministic single-tape Turing Machines computing functions fromN to N. The input number is the length of input word and the output number is represented by the head position.

It is convenient to represent machine IDs so that we can have a direct access to head position,

and to the symbol at the left of tape head.

So if the tape contents isabrakadabra, with machine scanning the letter d (at position 6) in state q, we represent it

as the quadruple hakarba, q, dabra, 6i.

(81)

Turing machine

“Superkonfiguracja”.

hw

^R

, q, v , `i,

(Notationw^R is w written backwards, e.g. 011^R = 110.)

I The tape contents is “wv BB. . . ” (where Bis blank);

I The head reads the first cell after w.

I The machine state isq;

I The length ofw is `.

Final configuration when q ∈ Final. The result is`. Initial configuration: Cn= hε, q0, •ⁿ, 0i.

Machine computes a partial function fromN to N.

(82)

Turing machine

hw

^R

, q, v , `i,

Final configuration when q ∈ Final. The result is`. Initial configuration: Cn= hε, q0, •ⁿ, 0i.

(83)

Turing machine

hw

^R

, q, v , `i,

Final configuration when q ∈ Final. The result is`.

Initial configuration: Cn= hε, q0, •ⁿ, 0i.

(84)

Turing machine

hw

^R

, q, v , `i,

Final configuration when q ∈ Final. The result is`.

Initial configuration: Cn= hε, q0, •ⁿ, 0i.

(85)

Assumptions about machines

I The machine is deterministic.

I There is one tape infinite to the right.

I The machine never writes a blank.

I The machine head never moves beyond the left tape end.

(86)

Encoding a Turing Machine

The set of states{q₀, q₁, . . . , q_r} is finite.

States are encoded as projections: q_i = λx0. . . x_r.x_i.

The alphabet {a₀, a₁, . . . , a_m} is finite.

Symbols are encoded as projections: a_i = λx₀. . . x_m.x_i.

Empty wordε is encoded as nil = hB, Ii.

Blank-free wordaw (list a :: w) is encoded as ha, wi. Word manipulation: head = Π1,tail = Π2.

(Check how it works)

(87)

Encoding a Turing Machine

(88)

Encoding a Turing Machine

(89)

Encoding a Turing Machine

Blank-free wordaw (list a :: w) is encoded as ha, wi.

Word manipulation: head = Π1,tail = Π2. (Check how it works)

(90)

Encoding a Turing Machine

Word manipulation: head = Π1,tail = Π2.

(91)

Encoding a Turing Machine

Word manipulation: head = Π1,tail = Π2. (Check how it works)

(92)

Encoding a Turing Machine

Superconfiguration hw^R, q, v , niis encoded

as a quadruplehw^R, q, v, ni.

Initial configuration: Init = λx. hnil , q0, x (λy . h•, y i)nil , 0i. ThenInit n hnil, q0, •ⁿ, 0i.

Stop test: Halt = λc. Π2cd1. . . dr = case Π2c of (d1, . . . , dr), whered_i = true, for q_i ∈ Final, and d_i = false, otherwise. Result extraction: Out = λc. Π4c.

(93)

Encoding a Turing Machine

Initial configuration: Init = λx. hnil , q0, x (λy . h•, y i)nil , 0i. ThenInit n hnil, q0, •ⁿ, 0i.

(94)

Encoding a Turing Machine

Initial configuration: Init = λx. hnil , q0, x (λy . h•, y i)nil , 0i.

ThenInit n hnil, q0, •ⁿ, 0i.

(95)

Encoding a Turing Machine

(96)

Encoding a Turing Machine

Stop test: Halt = λc. Π2cd1. . . dr = case Π2c of (d1, . . . , dr), whered_i = true, for q_i ∈ Final, and d_i = false, otherwise.

Result extraction: Out = λc. Π4c. (Check how it works)

(97)

Encoding a Turing Machine

Result extraction: Out = λc. Π4c.

(98)

Encoding a Turing Machine

Result extraction: Out = λc. Π4c.

(99)

Encoding a machine step

(Superconfiguration: hw^R, q, v, ni.)

We need a term Next s.t. Next(code of C1) ^β (code of C2) whenever the machine can move from C₁ to C₂.

We take: Next = λc. case Π2c of (R⁰, . . . , R^r) = λc. Π2c R⁰. . . R^r, whereRⁱ codes the configuration to be obtained if the machine state in the given configuration c is q_i.

(100)

Encoding a machine step

We need a term Next s.t. Next(code of C1) ^β (code of C2) whenever the machine can move from C₁ to C₂. We take:

Next = λc. case Π2c of (R⁰, . . . , R^r) = λc. Π2c R⁰. . . R^r, whereRⁱ codes the configuration to be obtained if the machine state in the given configuration c is q_i.

(101)

Encoding a machine step

We take Next = λc. Π2c R⁰. . . R^r, where Rⁱ codes the next configuration when the machine state in c is q_i.

How to define Rⁱ? As a case selector on the scanned symbol: Rⁱ = λc. head (Π₃c)R₁ⁱ . . . R_mⁱ ,

whereR_jⁱ is obtained according to the transitionδ(q_i, a_j) determined by stateqi and symbol aj.

(102)

Encoding a machine step

How to define Rⁱ?

As a case selector on the scanned symbol: Rⁱ = λc. head (Π₃c)R₁ⁱ . . . R_mⁱ ,

(103)

Encoding a machine step

How to define Rⁱ? As a case selector on the scanned symbol:

Rⁱ = λc. head (Π₃c)R₁ⁱ . . . R_mⁱ ,

(104)

Encoding a machine step

How to define Rⁱ? As a case selector on the scanned symbol:

Rⁱ = λc. head (Π₃c)R₁ⁱ . . . R_mⁱ ,

whereR_jⁱ is obtained according to the transition δ(q_i, a_j) determined by stateqi and symbol aj.

(105)

Encoding transitions

Given code c of configuration C = hw^R, q_i, a_jv , ni, we need a termR_jⁱ representing the next configuration, depending on the transition tableδ.

If δ(q_i, a_j) = hb, 0, pi (no move) then take

R_jⁱ = hΠ₁c, p, hb, tail (Π₃c)i, Π₄ci

If δ(q, a) = hb, +1, pi (right move) then take

R_jⁱ = hhb, (Π1c)i, p, tail (Π3c), succ(Π4c)i,

If δ(q, a) = hb, −1, pi(left move) then take

R_jⁱ = htail (Π1c), p, hhead (Π1c), hb, (tail (Π3c))ii, pred(Π4c)i. (The head never goes beyond the left tape end.)

(106)

Encoding transitions

(107)

Encoding transitions

(108)

Encoding transitions

R_jⁱ = htail (Π1c), p, hhead (Π1c), hb, (tail (Π3c))ii, pred(Π4c)i.

(The head never goes beyond the left tape end.)

(109)

Special case: a

_j

= B

LetC = hw^R, q_i, a_jv , ni oraz a_j = B.

Thena_jv is “empty”, i.e. Π3c = nil = hblank, Ii.

If δ(q_i, a_j) = hb, 0, pi (no move) then take R_jⁱ = hΠ₁c, p, hb, nil i, Π₄ci

If δ(q, a) = hb, +1, pi (right move) then take R_jⁱ = hhb, (Π₁c)i, p, nil , succ(Π₄c)i,

Rⁱ = htail (Π c), p, hhead (Π c), hb, nil ii, pred(Π c)i.

(110)

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 .

(111)

Encoding a Turing Machine

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

where

(112)

Encoding a Turing Machine

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

λx .W (Init x )W, where