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$ – Emil Jeřábek Feb 9 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$ – 임기정 Feb 9 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$ – 임기정 Feb 9 at 15:57
  • $\begingroup$ Perhaps you can edit your question to clarify it and then write your own answer? $\endgroup$ – D.W. Feb 9 at 18:45
  • 1
    $\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. Feb 10 at 17:08

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 Feb 12 at 16:55
  • $\begingroup$ @HanulJeon Thanks for your advice. $\endgroup$ – 임기정 Feb 13 at 12:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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