Church Turing Thesis

How to define a factorial function?

Fixed-point combinator in use

Using recursion and functions defined in advance, we can define

$$\mathbf{fact}:=\lambda n.\mathbf{ite}(\mathbf{iszero}n)\overline{1}(\mathbf{mult}n(\mathbf{fact}(\mathbf{pred}n)))$$

However, the definition of $\mathbf{fact}$ should not contain itself. We can change it a little bit:

$$\mathbf{fact}:=(\lambda f.\lambda n.\mathbf{ite}(\mathbf{iszero}n)\overline{1}(\mathbf{mult}n(f(\mathbf{pred}n))))\mathbf{fact}$$

Define $\mathbf{fac}\equiv \lambda f.\lambda n.\mathbf{ite}(\mathbf{iszero}n)\overline{1}(\mathbf{mult}n(f(\mathbf{pred}n)))$, then interestingly:

$$\mathbf{fact}=\mathbf{fac}\mathbf{fact}$$

which means it is the fixed-point of $\mathbf{fact}$!

Then we can define $\mathbf{fact}\equiv \mathbf{y}\mathbf{fac}$ where $\mathbf{y}$ is the Y combinator.

Example

$$\begin{array}{c}\begin{array}{rl}\mathbf{fact}\overline{2}& \equiv \mathbf{y}\mathbf{fac}\overline{2}\\ & =\mathbf{fac}(\mathbf{y}\mathbf{fac})\overline{2}\\ & {\to }_{\text{betas}}\mathbf{ite}(\mathbf{iszero}\overline{2})\overline{1}(\mathbf{mult}\overline{2}(\mathbf{y}\mathbf{fac}(\mathbf{pred}\overline{2})))\\ & {\to }_{\text{betas}}\mathbf{mult}\overline{2}(\mathbf{y}\mathbf{fac}\overline{1})\\ & \equiv \mathbf{mult}\overline{2}(\mathbf{fact}\overline{1}).\end{array}\end{array}$$

Data Structures in $\lambda$ Calculus

Pair & Tuple

Define $⟨s,t⟩\equiv \lambda x.xst$ to be the pair of term $s$ and $t$. Alternatively, we can write $\mathbf{pair}\equiv \lambda ab.\lambda x.xab$

As a pair, we should be able to get the first and second part:

$${\pi }_1\equiv \mathbf{fst}\equiv \lambda p.p\mathbf{t}$$ $${\pi }_2\equiv \mathbf{snd}\equiv \lambda p.p\mathbf{f}$$

We can easily verify that $\mathbf{fst}⟨s,t⟩{\to }_{\text{betas}}s$ and $\mathbf{snd}⟨s,t⟩{\to }_{\text{betas}}t$.

Similarly, define tuple $⟨s_1,s_2,\dots ,s_k⟩\equiv \lambda x.x{s}_1\dots s_k$ and ${\pi }_i^k\equiv \lambda p.p(\lambda x_1\dots x_k.x_i)$.

List

Define $\mathbf{nil}$ as the empty list.

We write $1::(2::(3::\mathbf{nil}))$ to denote a list of three elements.

We define $\mathbf{nil}=\lambda x.\mathbf{t}$ and $h::t\equiv \mathbf{pair}ht$. (The definition is not unique)

Then we can define head, tail and empty.

$$\begin{array}{rl}\mathbf{head}& \equiv \mathbf{fst}\\ \mathbf{tail}& \equiv \mathbf{snd}\\ \mathbf{empty}& \equiv \lambda l.l\lambda ht.\mathbf{f}\end{array}$$

List Operations

We now define $\mathbf{map},\mathbf{reduce},\mathbf{filter}$ operations for a list.

map

Given a list $l=x_0::x_1::\cdots ::x_{n-1}::\mathbf{nil}$ and a function $f$, $\mathbf{map}lf$ applies $f$ to all entries in the list $l$ to obtain a new list $l^{\prime }=f(x_0)::\cdots ::f(x_{n-1})::\mathbf{nil}$.

filter

For a Boolean function $f$, $\mathbf{filter}lf$ returns the list $l^{\prime }$ containing only elemtents $x_i$ s.t. $f{x}_i{\to }_{\text{betas}}\mathbf{t}$.

reduce

Given a list and a function $f$ taking two arguments, and a term $z$ considered as the neutral element of $f$, $\mathbf{reduce}lfz$ returns a term that is reduced by $f$ going through $l$, beginning with $z$.

Neutral

“Neutral” term can be considered as a term that does nothing when $f$ is applied to another term with it. For example, informally, 0 is neutral to sum operation, and 1 is neutral to product operation.

How to define them with $\lambda$ calc?

We can define $\mathbf{map}$ and $\mathbf{filter}$ from $\mathbf{reduce}$ and define $\mathbf{reduce}$ using fixed-point combinator.

$$\mathbf{map}\equiv \lambda lf.\mathbf{reduce}l(\lambda ab.\mathbf{pair}(fa)b)\mathbf{nil}$$

To define $\mathbf{reduce}$, first we want $\mathbf{reduce}\mathbf{nil}fz=z$. Then we want to set $\mathbf{reduce}(h::t)fz$ to $fh(\mathbf{reduce}\mathbf{tfz})$.

So we may define $\mathbf{reduce}$ as the fixed-point of

$$\mathbf{red}\equiv \lambda slfz.\mathbf{ite}(\mathbf{empty}l)z(f(\mathbf{head}l)(s(\mathbf{tail}l)fz))$$ $$\mathbf{reduce}\equiv \mathbf{y}\mathbf{red}$$

Functional Programming

It has several advantages:

1. No side effects
2. First-class and higher-order functions
3. Declarative style
4. Concurrency made easier (don’t really understand this now…)

Church-Turing Thesis

We now try to prove that $\lambda$ calculus is equivalent with Turing Machine.

Facts about TM

• TM can be encoded as binary strings (or integers).
• A configuration of a TM at certain time step is the collection of
  • tape content
  • current state
  • head position
• There is universal TM that when given $⟨M⟩$ and a string $w$ as input, it can simulates the computation of $M$ on input $w$.
• Variants of TMs are equivalent
• A non deterministic TM accepts if there exists an accepting branch.

Undecidability

• A languae or problem is Turing recognizable if it is the collection of strings $L(M)$ accepted by a Turing machine $M$.
• A language or problem is decidable if there is a machine recognizing it and the machine always halt.
• Halting problem is undecidable

$$HALT=\{⟨M,w⟩|M\text{ halts on input }w\}$$

Reduction

Reduction can be used to prove undecidability of more problems.

Problem $A$ reduces to $B$ means that it’s possible to decide $A$ using an algorithm for $B$ as a subroutine.

We write $A{\le }_{T}B$ to denote $A$ is Turing reducible to $B$. If $B$ is decidable, then $A$ is also decidable.

$\lambda$ Calculus is Turing Complete

A computational model is said to be Turing Complete if it can simulate any Turing machine.

$M$ is a Turing machine, we define a $\lambda$ term ${\mathbf{simulate}}_M$ simulating the machine $M$ in the sense that for all list $\alpha$ representing a possible initial configuration of the machine. ${\mathbf{simulate}}_M\alpha {\to }_{\text{betas}}{\alpha }_{\text{final}}$ if the machine terminates with final configuration ${\alpha }_{\text{final}}$. The leftmost $\beta$ reduction does not lead to a normal form if the machine does not halt.

Note

Note that here the information of the position of HEAD is encoded in the state list $\alpha$. It can be seen as we double the possible character on the tape, one representing that HEAD is currently pointing this cell while the other representing the opposite.

A useful insight is that the next state of a cell is only determined by the states of the two ceils next to it and itself. Then we can claim that there is a term ${\mathbf{local}}_M$ representing this function:

$${\mathbf{local}}_M⟨{\gamma }_{j-1},{\gamma }_j,{\gamma }_{j+1}⟩{\to }_{\text{betas}}{\gamma }_j^{\prime }$$

We can also easily define a term $\mathbf{pack}$ that pack the list into a list of this kind of tuple. Similarly, there is a term $\mathbf{terminate}$ that checks whether a configuration is terminating.

Then we define ${\mathbf{next}}_M\equiv \lambda l.\mathbf{map}(\mathbf{pack}l){\mathbf{local}}_M$, which depends on $M$ only.

Finally we get:

$$\begin{array}{c}{\mathbf{sim}}_M\equiv \lambda sl.(\mathbf{terminate}l)l(s({\mathbf{next}}_{M}l)),\end{array}$$ $${\mathbf{simulate}}_M\equiv \mathbf{y}{\mathbf{sim}}_M$$

Let’s check what happen if $M$ doesn’t halt. It means that $\mathbf{terminate}$ always returns false.

$$\begin{array}{rl}{\mathbf{simulate}}_{M}l& \equiv (\mathbf{y}{\mathbf{sim}}_M)l\\ & {\to }_{\beta }((\lambda x.{\mathbf{sim}}_M(xx))(\lambda x.{\mathbf{sim}}_M(xx)))l\\ & {\to }_{\beta }{\mathbf{sim}}_M((\lambda x.{\mathbf{sim}}_M(xx))(\lambda x.{\mathbf{sim}}_M(xx)))l\\ & {\to }_{\text{betas}}((\lambda x.{\mathbf{sim}}_M(xx))(\lambda x.{\mathbf{sim}}_M(xx)))({\mathbf{next}}_{M}l)\end{array}$$

It is trivial that it will never end.