File:Goldfarb1a.pdf

Goldfarb uses the fact that each Diophantine equation can be transformed into a set of equations of the form ${\displaystyle X_{i}+X_{j}=X_{k}}$, ${\displaystyle X_{i}*X_{j}=X_{k}}$, or ${\displaystyle X_{i}=c_{i}}$. He transforms each such set ${\displaystyle H}$ into a set ${\displaystyle S}$ of second-order unification problems. If the solvability of the latter could be decided, so could be the solvability of the Diophantine equation, which is, however, impossible in general (see en:Hilbert's tenth problem). As a last step, the set ${\displaystyle S}$ can easily be transformed to an equivalent single unification problem.

More precisely, let ${\displaystyle g}$ a binary function constant, and ${\displaystyle a,b}$ two nullary constants. For ${\displaystyle n\in {\mathbb {N}}}$ and a term ${\displaystyle t}$, let ${\displaystyle {\overline {n}}t}$ abbreviate the term ${\displaystyle \underbrace {g(a,g(a,\ldots ,g} _{n{\mbox{ occs of }}g}(a,t)\ldots ))}$. For each variable ${\displaystyle X_{i}}$ in an equation of ${\displaystyle H}$, introduce a unary function variable ${\displaystyle F_{i}}$ to be used in ${\displaystyle S}$. To avoid lambda abstractions, Goldfarb denotes the first, second, and third argument in a function expression by ${\displaystyle w_{1}}$, ${\displaystyle w_{2}}$, and ${\displaystyle w_{3}}$, respectively. Goldfarb's construction is such that ${\displaystyle F_{i}(w_{1})={\overline {n}}_{i}w_{1}}$ in a solution of ${\displaystyle S}$ iff ${\displaystyle X_{i}=n_{i}}$ in the corresponding solution of ${\displaystyle H}$.

The first kind of unification problems (File:Goldfarb1a.pdf, case 1 in the Theorem on p.228) ensures that each ${\displaystyle F_{i}}$ can have only instances of the form ${\displaystyle F_{i}(w_{1})={\overline {n}}_{i}w_{1}}$. It is obvious, that instantiating ${\displaystyle F_{i}}$ by the identity function ${\displaystyle F(w_{1})=w_{1}}$ is a solution of the shown equation. In every other solution, ${\displaystyle F_{i}(w_{1})}$ has to be of the form ${\displaystyle g(a,F'_{i}(w_{1}))}$ to match the right-hand side, see File:Goldfarb1b.pdf. Decomposing obtains the unification problem ${\displaystyle g(a,F'_{i}(a)){\stackrel {?}{=}}F'_{i}(g(a,a))}$, which, in turn, equals the unification problem from File:Goldfarb1a.pdf, and hence has the same solution set. File:Goldfarb1c.pdf shows the general form of instance for function variables ${\displaystyle F_{1},F_{2},F_{3}}$, with the small green numbers indicating the total ${\displaystyle g}$ count including first and last occurrence along the diagonal.

The second kind of unification problem, shown in File:Goldfarb2a.pdf, arises from equations of the form ${\displaystyle X_{1}=c_{1}}$; the third kind, shown in File:Goldfarb3a.pdf, arises from ${\displaystyle X_{1}+X_{2}=X_{3}}$. Both kinds are obvious.

The fourth kind arises from ${\displaystyle X_{1}*X_{2}=X_{3}}$. The corresponding unification problem is shown in File:Goldfarb4a.pdf, where ${\displaystyle G}$ is a function variable of arity 3. File:Goldfarb4b.pdf shows the solution term for ${\displaystyle G}$, assuming that ${\displaystyle F_{1},F_{2},F_{3}}$ have solution terms as shown in File:Goldfarb1c.pdf, and ${\displaystyle mn=p}$. To establish that no other solutions exist for ${\displaystyle G}$ requires an additional unification problem, shown in File:Goldfarb4c.pdf, which is a variant of File:Goldfarb4a.pdf with some ${\displaystyle a}$'s turned into ${\displaystyle b}$'s and vice versa. This problem is solved by the very same substituion, as demonstrated in File:Goldfarb4d.pdf.

Files overview:

• File:Goldfarb1a.pdf - unification problem to enforce ${\displaystyle F_{i}={\overline {n}}_{i}w_{1}}$
• File:Goldfarb1b.pdf - partial solution when ${\displaystyle F_{i}\neq w_{1}}$
• File:Goldfarb1c.pdf - enforced form of instance for function variables ${\displaystyle F_{1},F_{2},F_{3}}$
• File:Goldfarb2a.pdf - unification problem for Hilbert Problem equation ${\displaystyle X_{1}=c_{1}}$
• File:Goldfarb3a.pdf - unification problem for Hilbert Problem equation ${\displaystyle X_{1}+X_{2}=X_{3}}$
• File:Goldfarb4a.pdf - File:Goldfarb4a svg.svg - 1st unification problem for Hilbert Problem equation ${\displaystyle X_{1}*X_{2}=X_{3}}$
• File:Goldfarb4b.pdf - 1st unification problem's solution
• File:Goldfarb4c.pdf - 2nd unification problem for Hilbert Problem equation ${\displaystyle X_{1}*X_{2}=X_{3}}$
• File:Goldfarb4d.pdf - 2nd unification problem's solution

Warren D. Goldfarb (1981). "The Undecidability of the Second-Order Unification Problem". Theoretical Computer Science 13: 225–230. DOI:10.1016/0304-3975(81)90040-2.