Set is countable

By definition

Injection from $A$ to $ℕ$, in other words $∀𝑥, 𝑦 ∈ 𝐴. 𝑓\ 𝑥 = 𝑓\ 𝑦$¹ implies $𝑥 = 𝑦$.

• composition of two injections is injective
• inverse: a surjection² ($∀𝑏 ∈ 𝐵. ∃𝑎 ∈ 𝐴. 𝑓\ 𝑎 = 𝑏$) from $ℕ$ to $A$ where $A$ is not empty
• if $𝐵$ and $𝐶$ are countable, then $𝐵 × 𝐶$ is countable
• if $𝐵$ is countable, then $\text{List}\ B$ is countable

Set is uncountable infinity

Note: coutable = coutable infinity + finite

Diagonalisation

Assume countable, get a surjection $𝑓 ∈ ℕ → A$, change each $f\ n$ in someway and make contradiction.

Common finite sets

• $∅$
  • $\text{List}\ ∅$
  • $T \rightarrow ∅$ (empty)
  • $∅ \rightarrow T$ (only the empty function)
• $T \rightarrow\{*\}$
  • $T \rightarrow (T \rightarrow \{*\})$

Common countable infinity sets

• $\text{List}\ T$ where $T$ is finite but not empty
• $T \rightarrow \mathbb{N}$ where T is finite but not empty
  • $\text{Bool} \rightarrow \mathbb{N}$

Common uncountable sets

• $\mathbb{N} \rightarrow T$ where len(T) > 1, eg.
  • $\mathbb{N} \rightarrow \text{Bool}$
  • $\mathbb{N} \rightarrow \mathbb{N}$
  • $\mathbb{N} \rightarrow (\{*\} \rightarrow \mathbb{N})$
• $T \rightarrow V$ where $V$ is uncountable.

𝜒-computable

Variants:

• 𝜒-semi-decidable: $\underline{f}$ implements $f$ when $f\ a = \text{true}$, not terminate (undefined) else. Just define a new partial function by replacing false in the return value into undefined.

Implement it

Just implement it and prove $⟦ \underline{f}\ ⌜ x ⌝ ⟧ = ⌜ f\ x ⌝$, where $\underline{f}$ is the implemention of $f$.

Example

Prove this is 𝜒-semi-decidable.

f (e1, e2) = if ⟦ e1 ⟧ is defined or ⟦ e2 ⟧ is defined then true else false

We can define a partial function $g$ and its implemention $\underline{g}$:

g (e1, e2) = if ⟦ e1 ⟧ is defined or ⟦ e2 ⟧ is defined then true else undefined

_g_ = 𝜆 p. case p of { Pair(e1, e2) → parallel e1 e2 ⌜ zero ⌝ }

where parallel conceptly means run e1 and e2 step by step and check whether any of them terminates.

parallel = 𝜆e1. 𝜆e2. 𝜆n. case (_terminates‐in_ Pair(e1, n)) of {
  True() -> True(),
  False() -> case (_terminates‐in_ Pair(e2, n)) of {
    True() -> True(),
    False() -> parallel e1 e2 Suc(n) // run next step
  }
}

We have:

$$ \begin{align} & & ⟦ \underline{g}\ ⌜(e_1, e_2)⌝ ⟧ \\ &=& ⟦ \text{parallel}\ ⌜e_1⌝\ ⌜e_2⌝\ ⌜zero⌝ ⟧ \end{align} $$

For $n \in \mathbb{N}$:

• If either $\underline{\text{terminates‐in}}\ \text{Pair}(e_1, n)$ or $\underline{\text{terminates‐in}}\ \text{Pair}(e_1, n)$, then $⟦\text{parallel}\ ⌜e_1⌝\ ⌜e_2⌝\ ⌜n⌝⟧ = ⌜true⌝$.

• Else, $⟦\text{parallel}\ ⌜e_1⌝\ ⌜e_2⌝\ ⌜n⌝⟧ = ⟦\text{parallel}\ ⌜e_1⌝\ ⌜e_2⌝\ ⌜\text{suc}\ n⌝⟧$

So if for any $n$, $\underline{\text{terminates‐in}}\ \text{Pair}(e_1, n)$ or $\underline{\text{terminates‐in}}\ \text{Pair}(e_1, n)$, in other words, $⟦ e_1 ⟧$ is defined or $⟦ e_2 ⟧$ is defined, then

$$ \begin{align} & & ⟦ \underline{g}\ ⌜(e_1, e_2)⌝ ⟧ \\ &=& ⟦\text{parallel}\ ⌜e_1⌝\ ⌜e_2⌝\ ⌜zero⌝⟧ \\ &=& ⌜true⌝ \\ &=& ⌜g (e_1, e_2)⌝ \end{align} $$

Else, $⟦ \underline{g}\ ⌜(e_1, e_2)⌝ ⟧$ is undefined, because it will keep searching on all natural numbers and will never terminate.

So $\underline{g}$ is an implementation of $g$.

Not 𝜒-computable

Reducing the halting problem

Assume $f$ is 𝜒-computable, witness by $\underline{f}$. Implement $\underline{halts}$ with $\underline{f}$.

halts p = if p terminates then true else false

Self-applying

Self-applying and lead to contradiction.

Example

Prove this is not 𝜒-semi-decidable.

f (e1, e2) = if ⟦ e1 ⟧ is defined and ⟦ e2 ⟧ is defined then false else true

Assume 𝜒-semi-decidable funcition $g$ implemented as $\underline{g}$:

g (e1, e2) = if ⟦ e1 ⟧ is defined and ⟦ e2 ⟧ is defined then undefined else true

$\underline{g}$ has a pair of parameters which is hard to handle, we define another function $h$ with $g$ to solve this.

$$ \underline{h}\ e = \underline{g}\ ⌜( _⌞e_⌟\ _⌞code\ e_⌟\ ,\ _⌞e_⌟\ _⌞code\ e_⌟ )⌝ $$

Or in other words:

$$ \underline{h}\ e = \underline{g}\ Pair(Apply(e, code\ e), Apply(e, code\ e)) $$

Self-apply $h$.

$$ \begin{align} & & ⟦ \underline{h}\ ⌜\underline{h}⌝ ⟧ \\ & = & ⟦ \underline{g}\ Pair(Apply(⌜\underline{h}⌝, code\ ⌜\underline{h}⌝), Apply(⌜\underline{h}⌝, code\ ⌜\underline{h}⌝)) ⟧ \\ & = & ⟦ \underline{g}\ Pair(Apply(⌜\underline{h}⌝, ⌜⌜\underline{h}⌝⌝), Apply(⌜\underline{h}⌝, ⌜⌜\underline{h}⌝⌝)) ⟧ \\ & = & ⟦ \underline{g}\ ⌜(\underline{h}\ ⌜\underline{h}⌝, \underline{h}\ ⌜\underline{h}⌝)⌝ ⟧ \\ & = & ⌜ g\ (\underline{h}\ ⌜\underline{h}⌝, \underline{h}\ ⌜\underline{h}⌝) ⌝ \\ & = & ⌜ \text{if}\ ⟦ \underline{h}\ ⌜\underline{h}⌝ ⟧\ \text{is defined then undefined else true} ⌝ \end{align} $$

If $⟦ \underline{h}\ ⌜\underline{h}⌝ ⟧$ is defined, then ⟦h ⌜ h ⌝⟧ is undefined by the last equation, which is a contradiction, and vice versa.

Variant: Self-applying with encode-decode

Some times we want to prove something related to $\mathbb{N}$ instead of $\text{CExp}$, which makes self-applying harder.

We can define $\text{encode}$ to encode $\text{CExp}$ into $\mathbb{N}$ and its reverse operation $\text{decode}$. Both of these functions are $\chi$-computable.

Example

Prove this function is not $\chi$-computable for every $\chi$-computable $f$:

g f n = if f n is defined then undefined else 0

We can define:

$$ \begin{align} app& ∈ &ℕ& &⇀&\ ℕ\\ app&\ &n& &=&\ encode\ ⟦apply\ (decode\ n)\ ⌜n⌝⟧ \end{align} $$

implemented as:

$$ \underline{app} = 𝜆n. \underline{encode} (\underline{eval}\ Apply(\underline{decode}\ n, \underline{code}\ n)) $$

It is simple to prove $⟦\underline{app}\ ⌜ n ⌝⟧ = ⌜ \text{app}\ n ⌝$.

Assume $g_{app}$ is 𝜒-computable, then $⟦\underline{g_{app}}\ ⌜ n ⌝⟧ = ⌜ g_{app}\ n ⌝$.

Let $m = \text{encode}\ \underline{g_{app}}$, thus $\text{decode}\ m = \underline{g_{app}}$.

We can prove:

$$ \begin{align} & & ⟦\underline{g_{app}}\ ⌜ m ⌝⟧ \\ &=& ⌜ g_{app}\ m ⌝ \\ &=& ⌜ \text{if app m is defined then undefined else 0} ⌝ \\ &=& ⌜ \text{if}\ encode\ ⟦apply (decode\ m) ⌜ m ⌝⟧ \text{is defined then undefined else 0} ⌝ \\ &=& ⌜ \text{if}\ encode\ ⟦\underline{g_{app}}\ ⌜ m ⌝⟧ \text{is defined then undefined else 0} ⌝ \\ &=& ⌜ \text{if}\ ⟦\underline{g_{app}}\ ⌜ m ⌝⟧\ \text{is defined then undefined else 0} ⌝ \\ \end{align} $$

Then it is a contradictory and app is a counter-example of $f$ in "$g$ is $\chi$-computable for every $\chi$-computable $f$":