<p>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 <a href="https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem" rel="nofollow noreferrer">Wikipedia page for Hilbert's tenth problem</a>.</p>

CC BY-SA 4.0
2021-02-12T16:55:58.483Z
You can accept your answer by yourself. Accept it if you think your answer is sound and correct.
Hanul Jeon
CC BY-SA 4.0
2021-02-13T12:27:28.990Z
@HanulJeon Thanks for your advice.
Kijeong Lim
CC BY-SA 4.0
2021-02-11T08:57:17.773Z
2021-02-11T08:57:17.773Z
Kijeong Lim
<p>Usually, the unification problem for two given terms <span class="math-container">$t$</span> and <span class="math-container">$s$</span> is to find a substitution <span class="math-container">$\theta$</span> such that <span class="math-container">$\theta t = \theta s$</span>,
which is equal to finding the certain <span class="math-container">$\langle x_1 , \cdots , x_n \rangle$</span> such that <span class="math-container">$t = s$</span> holds.</p>
<p>But in the <span class="math-container">$\lambda$</span>Prolog programming language, by the existence of the logical operator <span class="math-container">$\mathtt{pi}$</span> whose semantics resembles <span class="math-container">$\forall$</span>, an unification problem is of the form
<span class="math-container">$$ \mathcal{Q}_1 x_1 \cdots \mathcal{Q}_n x_n \left[ t_1 = s_1 \land \cdots \land t_m = s_m \right] , $$</span>
where <span class="math-container">$\mathcal{Q}_i$</span> is an universal or existential quantifier.
See <a href="https://repository.upenn.edu/cis_reports/454/" rel="nofollow noreferrer">Miller's paper</a> for more details.</p>
<p>I made my own <span class="math-container">$\lambda$</span>Prolog interpreter without the operator of <span class="math-container">$+$</span> and <span class="math-container">$\times$</span>, in which the currently implemented are numerals and successor.</p>
<p>Now, what I want to do is to add both <span class="math-container">$+$</span> and <span class="math-container">$\times$</span> with their arithmetic semantics, i.e., I want to solve the decision problem:
<span class="math-container">$$ \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] , $$</span>
where <span class="math-container">$\mathcal{Q}_i$</span> is a quantifier, <span class="math-container">$x_i$</span> is a variable, <span class="math-container">$t_j$</span> and <span class="math-container">$s_j$</span> are terms; and terms are <span class="math-container">$\lambda$</span>-terms extended with the constants <span class="math-container">$0$</span>, <span class="math-container">$S$</span>, <span class="math-container">$+$</span> and <span class="math-container">$\times$</span>.</p>

CC BY-SA 4.0
2021-02-09T13:08:40.460Z
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 https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem.
Emil Jeřábek
CC BY-SA 4.0
2021-02-09T15:46:11.493Z
@EmilJeřábek Thanks for your comment. But that is a unification problem -- see https://repository.upenn.edu/cis_reports/454/ 5p
Kijeong Lim
CC BY-SA 4.0
2021-02-09T15:57:32.703Z
@EmilJeřábek The link in your comment is really helpful. I got the information that I have needed. Thank you again.
Kijeong Lim
CC BY-SA 4.0
2021-02-09T18:45:30.580Z
Perhaps you can [edit] your question to clarify it and then write your own answer?
D.W.
CC BY-SA 4.0
2021-02-10T09:15:47.783Z
@D.W. Yes, I've done.
Kijeong Lim
CC BY-SA 4.0
2021-02-10T17:08:27.457Z
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!
D.W.
CC BY-SA 4.0
2021-02-11T07:20:10.020Z
@D.W. Thanks for your advice. I followed it.
Kijeong Lim
CC BY-SA 4.0
2021-02-11T08:52:14.450Z
No, you haven't followed D.W.s advice. Your answer is still contained in the question, and is not an answer!
Jan Johannsen
CC BY-SA 4.0
2021-02-11T08:58:08.783Z
@JanJohannsen Like this? Is it done?
Kijeong Lim
CC BY-SA 4.0
2021-02-11T10:52:30.050Z
Yes, this is how it is supposed to be.
Jan Johannsen
<decidability><logic-programming>
How to solve an unification problem on $\mathbb{N}$?
Kijeong Lim
# How to solve an unification problem on $\mathbb{N}$?

(Asked by: username_0 on 2021-02-09)

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](https://repository.upenn.edu/cis_reports/454/) 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$.

**Tags:** decidability, logic-programming

> **Comments:**
> **username_1**: 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 https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem.  
> **username_0**: @EmilJeřábek Thanks for your comment. But that is a unification problem -- see https://repository.upenn.edu/cis_reports/454/ 5p  
> **username_0**: @EmilJeřábek The link in your comment is really helpful. I got the information that I have needed. Thank you again.  
> **username_2**: Perhaps you can [edit] your question to clarify it and then write your own answer?  
> **username_0**: @username_2 Yes, I've done.  
> **username_2**: 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!  
> **username_0**: @username_2 Thanks for your advice. I followed it.  
> **username_3**: No, you haven't followed username_2s advice. Your answer is still contained in the question, and is not an answer!  
> **username_0**: @JanJohannsen Like this? Is it done?  
> **username_3**: Yes, this is how it is supposed to be.  

---

## 1 answers

### Answer by username_0 on 2021-02-11. Score: 1 | Accepted answer

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](https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem).

> **Comments:**
> **username_4**: You can accept your answer by yourself. Accept it if you think your answer is sound and correct.  
> **username_0**: @HanulJeon Thanks for your advice.  

---

