According to Jaap van Oosten's "A General Form of Relative Recursion," given a PCA $A$ and a partial function $f:A\rightharpoonup A$, one can define a new PCA $A[f]$ whose elements are those of $A$, but with a new application operation $a\cdot^f b$ defined as follows:
- Let $[u_0,\ldots,u_{n-1}]$ denote the code for the finite sequence of elements $u_0,\ldots,u_{n-1}\in A$.
- An $f$-dialogue is a sequence $[u_0,\ldots,u_{n-1}]$ such that for any $i<n$ there's a $v_i\in A$ with $a\cdot [b,u_0,\ldots,u_{i-1}]=p\bot v_i$ and $f(v_i)=u_i$
- Finally, $a\cdot^f b$ is defined and equal to $c$ if there is an $f$-dialgue between $a,b$ with $a\cdot [b,u_0,\ldots,u_{n-1}]=p\top c$.
(Here $p$ is the pairing combinator and $\bot,\top$ are the coded booleans, e.g. $ki$ and $k$.)
Van Oosten's paper contains a proof that the resulting structure has the $S$ and $K$ combinators, but it doesn't, that I can see, contain a proof that this new operation is actually functional; that is, that there is at most one such $c$ in the above definition. The doubt that springs to mind is I can see no reason to think there wouldn't be an $f$-dialogue $[w_0,\ldots,w_k]$ such that $a\cdot[b,w_0,\ldots,w_k]=p\top d$ with $d\neq c$, possibly even with the $w_j$ just being the $u_i$ in a different order.
I'm guessing that my concern, and not Jaap, is incorrect. So how do I see that there is at most one $c\in A[f]$ with $a\cdot^f b=c$? Have I accidentally misconstrued some part of the definition?
The answer is that $f$-dialogues of length $n$ between a pair of elements, if they exist, are unique.
Let $[u_0,\ldots,u_{n}]$ and $[w_0,\ldots,w_n]$ be $f$-dialogues between $a$ and $b$. Say the two sequences agree up to the $(i-1)$-th coordinate (where . This means that $$a\cdot [b,u_0,\ldots,u_{i-1}]=a\cdot[b,w_0,\ldots,w_{i-1}]=p\bot v_i$$ for some $v_i\in\operatorname{dom}(f)\subseteq A$ by the defintion of $f$-dialogues. But then by definition the $i$-th coordinate of either dialogue must be $f(v_i)$, so they also agree on the $i$-th coordinate; and by an inductive argument, every coordinate must be the same.