Dialogical logic programming
This was a fun read, but there are some strawmen and misunderstandings in the article.<p>&gt; This should be acceptable as conjunction is commutative.<p>Ah, but Prolog&#x27;s comma (,) is <i>not</i> logical conjunction, and all Prolog programmers know this! The case is quite similar to, for example, &amp;&amp; in C, which is also <i>not</i> logical conjunction. Both of these operators mean &quot;and then&quot;, not simply &quot;and&quot;. In certain cases, there is no difference, so <i>often</i> you can read either of these as a simple &quot;and&quot;, but you cannot do that in general. And yes, we do lazily call it &quot;and&quot; or &quot;conjunction&quot;, but we never forget that these words are not to be interpreted in the strict logical sense.<p>So there is no need to introduce &quot;conjunctive quantifiers&quot; to Prolog, it already has them, written as a comma.<p>&gt; (∐ X ∈ 0..2) even(X)<p>&gt; Would be the exactly same as writing:<p>&gt; even(0) ⊔ even(1) ⊔ even(2)<p>&gt; All variables in Prolog can be interpreted as this kind of choice-existential quantifiers such as above. Binding a variable is similar to doing a choice. If the choice is wrong, we attempt to backtrack from it as long as we have other choices we can examine.<p>No, this is an incomplete model of what you can do in Prolog. If you write:<p><pre><code>    ?- X = f(A, B).
</code></pre>
then A and B are not choice-existentially quantified. They do not, at this point, correspond to choices that you can enumerate and backtrack over. A and B are simply entirely unconstrained variables. Many many people misunderstand Prolog logical variables as something like lazy streams of possible solutions, but they aren&#x27;t. Not until you do something that tries to bind them. &quot;Reinventing&quot; Prolog in this way gives you something that is not Prolog.<p>&gt; We may also present prolog&#x27;s disjunction through disjunctive choice:<p>&gt; even(0).<p>&gt; even(s(s(N))) :- even(N).<p>&gt; Corresponds to:<p>&gt; even(X) :-<p>&gt;     X = 0 ⊔ (X = s(s(N)) ∧ even(N)).<p>It also corresponds to:<p><pre><code>    even(X) :-
        X = 0 ; (X = s(s(N)), even(N)).
</code></pre>
The author may not be aware that Prolog already has (again, not-fully-logical) disjunction?<p>&gt; It might be this gives us a sound concept of negation in the language, but I haven&#x27;t concluded that it&#x27;d do so because I&#x27;m not certain. For example, the negation of the above one might be:<p>&gt; ¬even(X) :-<p>&gt;     X != 0 ⊓ (X != s(s(N)) ∨ ¬even(N)).<p>If all you know about N is that X is different from s(s(N)), then there is no relation between X and N, and the recursive call to ¬even(N) will not tell you anything about X. So this won&#x27;t work.