Primitive recursive pairing function (source code)

= Primitive recursive pairing function
{title2=$\langle x,y\rangle$}

A <pairing function> whose forward map and two inverse coordinate functions are <primitive recursive functions>. For example, the Cantor pairing function $\langle x,y\rangle=(x+y)(x+y+1)/2+y$ has such inverses: find the diagonal index by <bounded minimization> over integers at most the encoded value, then recover $x,y$ by subtraction. It enables finite tuples to be decoded within a <primitive recursive> construction.