1.4.5: An Alternative Pairing Function

\(\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} } }\)

There are other enumerations of \(\Nat^2\) that make it easier to figure out what their inverses are. Here is one. Instead of visualizing the enumeration in an array, start with the list of positive integers associated with (initially) empty spaces. Imagine filling these spaces successively with pairs \(\tuple{n,m}\) as follow. Starting with the pairs that have \(0\) in the first place (i.e., pairs \(\tuple{0,m}\)), put the first (i.e., \(\tuple{0,0}\)) in the first empty place, then skip an empty space, put the second (i.e., \(\tuple{0,2}\)) in the next empty place, skip one again, and so forth. The (incomplete) beginning of our enumeration now looks like this \[\small \begin{array}{@{}c c c c c c c c c c c@{}} \mathbf 1 & \mathbf 2 & \mathbf 3 & \mathbf 4 & \mathbf 5 & \mathbf 6 & \mathbf 7 & \mathbf 8 & \mathbf 9 & \mathbf{10} & \dots \\ \\ \tuple{0,1} & & \tuple{0,2} & & \tuple{0,3} & & \tuple{0,4} & & \tuple{0,5} & & \dots \\ \end{array}\nonumber\] Repeat this with pairs \(\tuple{1,m}\) for the places that still remain empty, again skipping every other empty place: \[\small \begin{array}{@{}c c c c c c c c c c c@{}} \mathbf 1 & \mathbf 2 & \mathbf 3 & \mathbf 4 & \mathbf 5 & \mathbf 6 & \mathbf 7 & \mathbf 8 & \mathbf 9 & \mathbf{10} & \dots \\ \\ \tuple{0,0} & \tuple{1,0} & \tuple{0,1} & & \tuple{0,2} & \tuple{1,1} & \tuple{0,3} & & \tuple{0,4} & \tuple{1,2} & \dots \\ \end{array}\nonumber\] Enter pairs \(\tuple{2,m}\), \(\tuple{2,m}\), etc., in the same way. Our completed enumeration thus starts like this: \[\small \begin{array}{@{}cc c c c c c c c c c@{}} \mathbf 1 & \mathbf 2 & \mathbf 3 & \mathbf 4 & \mathbf 5 & \mathbf 6 & \mathbf 7 & \mathbf 8 & \mathbf 9 & \mathbf{10} & \dots \\ \\ \tuple{0,0} & \tuple{1,0} & \tuple{0,1} & \tuple{2,0} & \tuple{0,2} & \tuple{1,1} & \tuple{0,3} & \tuple{3,0} & \tuple{0,4} & \tuple{1,2} & \dots \\ \end{array}\nonumber\] If we number the cells in the array above according to this enumeration, we will not find a neat zig-zag line, but this arrangement: \[\begin{array}{ c | c | c | c | c | c | c | c } & \mathbf 0 & \mathbf 1 & \mathbf 2 & \mathbf 3 & \mathbf 4 & \mathbf 5 & \dots \\ \hline \mathbf 0 & 1 & 3 & 5 & 7 & 9 & 11 & \dots \\ \hline \mathbf 1 & 2 & 6 & 10 & 14 & 18 & \dots & \dots \\ \hline \mathbf 2 & 4 & 12 & 20 & 28 & \dots & \dots & \dots \\ \hline \mathbf 3 & 8 & 24 & 40 & \dots & \dots & \dots & \dots \\ \hline \mathbf 4 & 16 & 48 & \dots & \dots & \dots & \dots & \dots \\ \hline \mathbf 5 & 32 & \dots & \dots & \dots & \dots & \dots & \dots \\ \hline \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \ddots\\ \end{array}\nonumber\] We can see that the pairs in row \(0\) are in the odd numbered places of our enumeration, i.e., pair \(\tuple{0,m}\) is in place \(2m+1\); pairs in the second row, \(\tuple{1,m}\), are in places whose number is the double of an odd number, specifically, \(2 \cdot (2m+1)\); pairs in the third row, \(\tuple{2,m}\), are in places whose number is four times an odd number, \(4 \cdot (2m+1)\); and so on. The factors of \((2m+1)\) for each row, \(1\), \(2\), \(4\), \(8\), …, are exactly the powers of \(2\): \(1= 2^0\), \(2 = 2^1\), \(4 = 2^2\), \(8 = 2^3\), …In fact, the relevant exponent is always the first member of the pair in question. Thus, for pair \(\tuple{n,m}\) the factor is \(2^n\). This gives us the general formula: \(2^n \cdot (2m+1)\). However, this is a mapping of pairs to positive integers, i.e., \(\tuple{0,0}\) has position \(1\). If we want to begin at position \(0\) we must subtract \(1\) from the result. This gives us:

Example \(\PageIndex{1}\)

The function \(h\colon \Nat^2 \to \Nat\) given by \[h(n,m) = 2^n (2m+1) - 1\nonumber\] is a pairing function for the set of pairs of natural numbers \(\Nat^2\).

Accordingly, in our second enumeration of \(\Nat^2\), the pair \(\tuple{0,0}\) has code \(h(0,0) = 2^0(2\cdot 0+1) - 1 = 0\); \(\tuple{1,2}\) has code \(2^{1} \cdot (2 \cdot 2 + 1) - 1 = 2 \cdot 5 - 1 = 9\); \(\tuple{2,6}\) has code \(2^{2} \cdot (2 \cdot 6 + 1) - 1 = 51\).

Sometimes it is enough to encode pairs of natural numbers \(\Nat^2\) without requiring that the encoding is surjective. Such encodings have inverses that are only partial functions.

Example \(\PageIndex{2}\)

The function \(j\colon \Nat^2 \to \Nat^+\) given by \[j(n,m) = 2^n3^m\nonumber\] is an injective function \(\Nat^2 \to \Nat\).