3 ms·

This was a fun read, but there are some strawmen and misunderstandings in the article. > This should be acceptable as conjunction is commutative. Ah, but Prol

This was a fun read, but there are some strawmen and misunderstandings in the article. > This should be acceptable as conjunction is commutative. Ah, but Prolog's comma (,) is not logical conjunction, and all Prolog programmers know this! The case is quite similar to, for example, && in C, which is also not logical conjunction. Both of these operators mean "and then", not simply "and". In certain cases, there is no difference, so often you can read either of these as a simple "and", but you cannot do that in general. And yes, we do lazily call it "and" or "conjunction", but we never forget that these words are not to be interpreted in the strict logical sense. So there is no need to introduce "conjunctive quantifiers" to Prolog, it already has them, written as a comma. > (∐ X ∈ 0..2) even(X) > Would be the exactly same as writing: > even(0) ⊔ even(1) ⊔ even(2) > 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. No, this is an incomplete model of what you can do in Prolog. If you write: ?- X = f(A, B). 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't. Not until you do something that tries to bind them. "Reinventing" Prolog in this way gives you something that is not Prolog. > We may also present prolog's disjunction through disjunctive choice: > even(0). > even(s(s(N))) :- even(N). > Corresponds to: > even(X) :- > X = 0 ⊔ (X = s(s(N)) ∧ even(N)). It also corresponds to: even(X) :- X = 0 ; (X = s(s(N)), even(N)). The author may not be aware that Prolog already has (again, not-fully-logical) disjunction? > It might be this gives us a sound concept of negation in the language, but I haven't concluded that it'd do so because I'm not certain. For example, the negation of the above one might be: > ¬even(X) :- > X != 0 ⊓ (X != s(s(N)) ∨ ¬even(N)). 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't work.

feanaro 8y ago
> 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't work. Won't it? Either: 1. X = 0, in which case ¬even(X) is false. 2. X != 0, in which case a. X can't be unified with s(s(N)), in which case ¬even(X) is true (since X can then only be s(0)). b. X can be unified with s(s(N)) for some N, in which case we restart the procedure for that N. N is either I. even, in which case we'll eventually evaluate even(0), which is a base case. II. odd, in which case we'll eventually be unable to unify the argument X with some s(s(N)). By negation as failure[^naf], we'll eventually prove ¬even(X). [^naf]: https://en.wikipedia.org/wiki/Negation_as_failure https://en.wikipedia.org/wiki/Negation_as_failure
- tom_mellior 8y ago
  You're right, from the point of view of a sufficiently strong logic and a sufficiently strong prover for that logic! But: > N is either ... In a type system like Prolog's, N can also be any of: f(Y) apple_pie N (a free variable) You assume a type and mode system in which X and N must be bound, and they must be bound to ground natural number terms. You also assume that the logic programming system can deduce positive information from the failing unification on an infinite domain (that X must be s(0) if it is not 0 and not of the form s(s(N)))). It's possible that the article's author also had all these implicit assumptions, but it's not clear to me that they did.
  - feanaro 8y ago
    Right, thanks for the insight. A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. This is because `apple_pie` is obviously neither `0` nor `s(s(N))`. Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Is this right? Am I missing something?
    - 8y ago

feanaro 8y ago

> 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't work. Won't it? Either: 1. X = 0, in which case ¬even(X) is false. 2. X != 0, in which case a. X can't be unified with s(s(N)), in which case ¬even(X) is true (since X can then only be s(0)). b. X can be unified with s(s(N)) for some N, in which case we restart the procedure for that N. N is either I. even, in which case we'll eventually evaluate even(0), which is a base case. II. odd, in which case we'll eventually be unable to unify the argument X with some s(s(N)). By negation as failure[^naf], we'll eventually prove ¬even(X). [^naf]: https://en.wikipedia.org/wiki/Negation_as_failure https://en.wikipedia.org/wiki/Negation_as_failure

tom_mellior 8y ago
You're right, from the point of view of a sufficiently strong logic and a sufficiently strong prover for that logic! But: > N is either ... In a type system like Prolog's, N can also be any of: f(Y) apple_pie N (a free variable) You assume a type and mode system in which X and N must be bound, and they must be bound to ground natural number terms. You also assume that the logic programming system can deduce positive information from the failing unification on an infinite domain (that X must be s(0) if it is not 0 and not of the form s(s(N)))). It's possible that the article's author also had all these implicit assumptions, but it's not clear to me that they did.
- feanaro 8y ago
  Right, thanks for the insight. A further thought: `apple_pie` wouldn't actually be problematic, in the sense that we could deduce `¬even(apple_pie)` from the way it's currently written. This is because `apple_pie` is obviously neither `0` nor `s(s(N))`. Of course, this might not be desirable philosophically since it might be preferable to consider applying `even` to `apple_pie` nonsense since they are of different types (informally speaking). Is this right? Am I missing something?
  - 8y ago