| >> It's beyond me why anyone considers this contentious. Could you tone this sort of thing down please? Its needlessly confrontational
tone only serves to add irrelevant noise to the converstation. Thank you in
advance. >> ?- L = [_,_,_], \+ (member(X, L), \+ (X < 2)). Thank you for clarifying your intention with the original example. In that
case, you could redefine </2 to avoid raising an error. Off the top of my head: 1 < 2.
2 < 3.
3 < 4.
etc. Again it's a matter of implementation - in this case, of the predicate
</2, rather than \+/2.>> ?- forall(s(N), (N = 0; N = s(M), s(M))). In your previous comment you said that "You can absolutlely prove theorems
over infinite domains with [SMT2]", constrasting it with Prolog that if I
understand correctly, you claim cannot. In my reply to your comment, I gave
examples of theorems over infinite domains (integers and lists), that can be
proven with Prolog. You given an example of how one of those theories can "go infinite" if you
make the right query. It can, but if you make a different query, it doesn't go
infinite and Prolog proves it. So, Prolog can prove theories over infinite
domains. EDIT: >> My only claim is that, it's much easier to understand why this happens if one
thinks of Prolog as a search language over structural terms, rather than as a
logic language where such a statement could be expected to be useful (if not
necessarily decidable). Your claim would be clearer if you explained what you mean by "logic
language". Given what you've said so far I honestly have no idea what you mean
by that. In any case, what you say above sounds like the well-understood fact that
Prolog programs have a declarative and a procedural reading and that one must
be aware of the internal machinery of the interpreter to avoid infinite
recursion. |
These sorts of comments (and your earlier notation nitpicking) come across as smug and condescending. Why start a conversation with someone you don't appear to respect?
> In any case, what you say above sounds like the well-understood fact that Prolog programs have a declarative and a procedural reading and that one must be aware of the internal machinery of the interpreter to avoid infinite recursion.
Yes, hence why I don't understand why my statement is so contentious. I wasn't being hyperbolic with that remark; I really don't understand the strong negative reaction to my off-the-cuff explanation of the above fact.
You're clearly an intelligent person, and I like to think I am too, and since intelligent people should not disagree, let me restate my thesis in clearer terms:
By "logic language" I mean, a language which allows one to express and reason about logical relations (roughly in the sense of first-order logic). Yes, my definition is intentionally vague, as are all language classifications.
Core Prolog (meaning, Horn clauses + terms + SLD + ISO definitions of predicates) allows expressing only the logical relations of equality (=/2) and inequality (dif/2; to contrast, </2 is nonlogical in core Prolog), and then, only over structured terms (i.e., atoms + compounds), and even then, is limited by its resolution strategy. This stands in contrast to languages like SMT2 and TLA+, which permit arbitrary relations over various, even abstract, domains (such as SMT2's capability to express relations on uninterpreted functions) and which do not specify, nor are associated with, a particular resolution strategy. (TLA+ for example, is strongly associated with TLC, but there is also TLAPS, and it is specified expressly independent of any resolution strategy.)
Therefore, for someone who is wondering why Prolog programs should be written in terms of something so concrete as lists, when first-order logic rarely utilizes them, it is best to think of Prolog not as a language for reasoning about logical relations (a "logic language"), but as a language for search and unification of structured terms.