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$.

  • 3
    $\begingroup$ 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. $\endgroup$ Commented Feb 9, 2021 at 13:08
  • $\begingroup$ @EmilJeřábek Thanks for your comment. But that is a unification problem -- see repository.upenn.edu/cis_reports/454 5p $\endgroup$ Commented Feb 9, 2021 at 15:46
  • $\begingroup$ @EmilJeřábek The link in your comment is really helpful. I got the information that I have needed. Thank you again. $\endgroup$ Commented Feb 9, 2021 at 15:57
  • $\begingroup$ Perhaps you can edit your question to clarify it and then write your own answer? $\endgroup$
    – D.W.
    Commented Feb 9, 2021 at 18:45
  • 2
    $\begingroup$ Please don't append "Edit: <more stuff>". Instead, revise the question to read well for someone who encounters it for the first time. We have revision history, so no need to mark what has changed. Please don't put your answer in the post. Instead, write your answer below, in the 'Your Answer' box. Thank you! $\endgroup$
    – D.W.
    Commented Feb 10, 2021 at 17:08

1 Answer 1


I have concluded that one cannot add both + and × in the λProlog programming language with their arithmetic semantics since the decision problem is undeciable. Because if it was decidable then Hilbert's tenth problem would have a positive answer. See the Wikipedia page for Hilbert's tenth problem.

  • $\begingroup$ You can accept your answer by yourself. Accept it if you think your answer is sound and correct. $\endgroup$
    – Hanul Jeon
    Commented Feb 12, 2021 at 16:55
  • $\begingroup$ @HanulJeon Thanks for your advice. $\endgroup$ Commented Feb 13, 2021 at 12:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.