# How to solve an unification problem on $\mathbb{N}$?

Usually, the unification problem for two given terms $$t$$ and $$s$$ is to find a substitution $$\theta$$ such that $$\theta t = \theta s$$, which is equal to finding the certain $$\langle x_1 , \cdots , x_n \rangle$$ such that $$t = s$$ holds.

But in the $$\lambda$$Prolog programming language, by the existence of the logical operator $$\mathtt{pi}$$ whose semantics resembles $$\forall$$, an unification problem is of the form $$\mathcal{Q}_1 x_1 \cdots \mathcal{Q}_n x_n \left[ t_1 = s_1 \land \cdots \land t_m = s_m \right] ,$$ where $$\mathcal{Q}_i$$ is an universal or existential quantifier. See Miller's paper for more details.

I made my own $$\lambda$$Prolog interpreter without the operator of $$+$$ and $$\times$$, in which the currently implemented are numerals and successor.

Now, what I want to do is to add both $$+$$ and $$\times$$ with their arithmetic semantics, i.e., I want to solve the decision problem: $$\mathbb{N} \models \mathcal{Q}_1 x_1 \cdots \mathcal{Q}_n x_n \left[ t_1 = s_1 \land \cdots \land t_m = s_m \right] ,$$ where $$\mathcal{Q}_i$$ is a quantifier, $$x_i$$ is a variable, $$t_j$$ and $$s_j$$ are terms; and terms are $$\lambda$$-terms extended with the constants $$0$$, $$S$$, $$+$$ and $$\times$$.

• I don’t understand in what sense this is a unification problem, or perhaps I do not understand the notation. The way it is written, it looks like the satisfaction problem for $(\mathbb N,0,S,+,\times)$ extended with some sort of $\lambda$-calculus. This is undecidable even with no $\lambda$s and with only existential quantifiers, see en.wikipedia.org/wiki/Hilbert%27s_tenth_problem. – Emil Jeřábek Feb 9 at 13:08
• @EmilJeřábek Thanks for your comment. But that is a unification problem -- see repository.upenn.edu/cis_reports/454 5p – 임기정 Feb 9 at 15:46
• @EmilJeřábek The link in your comment is really helpful. I got the information that I have needed. Thank you again. – 임기정 Feb 9 at 15:57
• Perhaps you can edit your question to clarify it and then write your own answer? – D.W. Feb 9 at 18:45