1.4.4: Pairing Functions and Codes

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Cantor’s zig-zag method makes the enumerability of \(\Nat^n\) visually evident. But let us focus on our array depicting \(\Nat^2\). Following the zig-zag line in the array and counting the places, we can check that \(\tuple{1,2}\) is associated with the number \(7\). However, it would be nice if we could compute this more directly. That is, it would be nice to have to hand the inverse of the zig-zag enumeration, \(g\colon \Nat^2 \to \Nat\), such that \[g(\tuple{0,0}) = 0, \; g(\tuple{0,1}) = 1, \; g(\tuple{1,0}) = 2, \; \dots, g(\tuple{1,2}) = 7, \; \dots\nonumber\] This would enable to calculate exactly where \(\tuple{n, m}\) will occur in our enumeration.

In fact, we can define \(g\) directly by making two observations. First: if the \(n\)th row and \(m\)th column contains value \(v\), then the \((n+1)\)st row and \((m-1)\)st column contains value \(v + 1\). Second: the first row of our enumeration consists of the triangular numbers, starting with \(0\), \(1\), \(3\), \(5\), etc. The \(k\)th triangular number is the sum of the natural numbers \(< k\), which can be computed as \(k(k+1)/2\). Putting these two observations together, consider this function: \[g(n,m) = \frac{(n+m+1)(n+m)}{2} + n\nonumber\] We often just write \(g(n, m)\) rather that \(g(\tuple{n, m})\), since it is easier on the eyes. This tells you first to determine the \((n+m)^\text{th}\) triangle number, and then subtract \(n\) from it. And it populates the array in exactly the way we would like. So in particular, the pair \(\tuple{1, 2}\) is sent to \(\frac{4 \times 3}{2} + 1 = 7\).

This function \(g\) is the inverse of an enumeration of a set of pairs. Such functions are called pairing functions.

Definition \(\PageIndex{1}\): Pairing function

A function \(f\colon A \times B \to \Nat\) is an arithmetical pairing function if \(f\) is injective. We also say that \(f\) encodes \(A \times B\), and that \(f(x,y)\) is the code for \(\tuple{x,y}\).

We can use pairing functions encode, e.g., pairs of natural numbers; or, in other words, we can represent each pair of elements using a single number. Using the inverse of the pairing function, we can decode the number, i.e., find out which pair it represents.

Problem \(\PageIndex{1}\)

Give an enumeration of the set of all non-negative rational numbers.

Problem \(\PageIndex{2}\)

Show that \(\Rat\) is countable. Recall that any rational number can be written as a fraction \(z/m\) with \(z \in \Int\), \(m \in \Nat^+\).

Problem \(\PageIndex{3}\)

Define an enumeration of \(\Bin^*\).

Problem \(\PageIndex{4}\)

Recall from your introductory logic course that each possible truth table expresses a truth function. In other words, the truth functions are all functions from \(\Bin^k \to \Bin\) for some \(k\). Prove that the set of all truth functions is enumerable.

Problem \(\PageIndex{5}\)

Show that the set of all finite subsets of an arbitrary infinite countable set is countable.

Problem \(\PageIndex{6}\)

A subset of \(\Nat\) is said to be cofinite iff it is the complement of a finite set \(\Nat\); that is, \(A \subseteq \Nat\) is cofinite iff \(\Nat\setminus A\) is finite. Let \(I\) be the set whose elements are exactly the finite and cofinite subsets of \(\Nat\). Show that \(I\) is countable.

Problem \(\PageIndex{7}\)

Show that the countable union of countable sets is countable. That is, whenever \(A_1\), \(A_2\), … are sets, and each \(A_i\) is countable, then the union \(\bigcup_{i=1}^\infty A_i\) of all of them is also countable. [NB: this is hard!]

Problem \(\PageIndex{8}\)

Let \(f \colon A \times B \to \Nat\) be an arbitrary pairing function. Show that the inverse of \(f\) is an enumeration of \(A \times B\).

Problem \(\PageIndex{9}\)

Specify a function that encodes \(\Nat^3\).