4 ms·

The terminology of first-order logic is indeed quite different from that of Prolog. A key reason for this is that in FOL, we have to distinguish between the syn

by triska 8y ago

The terminology of first-order logic is indeed quite different from that of Prolog. A key reason for this is that in FOL, we have to distinguish between the syntactic entities and their interpretations. So, in FOL, we have predicate symbols that are assigned to relations by an interpretation, we have constant symbols that are assigned to domain elements by an interpretation, we have function symbols that are assigned functions by an interpretation. In addition, many theorems also require that we distinguish between countable and uncountable signatures. In contrast, Prolog is confined to a single kind of interpretations, namely to Herbrand structures, where each term "stands for itself", and where we only need symbols that already occur in the clauses we are considering: https://en.wikipedia.org/wiki/Herbrand_structure https://en.wikipedia.org/wiki/Herbrand_structure So, in Herbrand structures, the interpretation of a term T is simply the symbolic representation of T, i.e., "T". Importantly, one can show that a set of clauses has a model if and only if it has a Herbrand model. This also has important semantic consequences: For example, due to the compactness theorem (and its consequence, the upward Löwenheim–Skolem theorem), one can show that important concepts such as the transitive closure of a relation, the class of connected graphs, and the natural numbers with only the intended model (up to isomorphism) cannot be expressed in first-order logic! https://en.wikipedia.org/wiki/Compactness_theorem https://en.wikipedia.org/wiki/Compactness_theorem Yet, we can readily express these things in Prolog, and in fact almost every Prolog program also does that or needs them! Why? Because Prolog (implicitly) only considers least Herbrand models, so we do not need this layered syntactic view, and also do not run into these semantic issues when programming in Prolog. An argument can be made that in this case, what at first seems like a restriction in fact extends the usefulness of the language. A similar argument can be made also for several constructs within the language.

nmadden 8y ago
While Prolog’s operational semantics are given in terms of least Herband models (at least, before you consider negation), you can also view a Prolog program as a subset of FOL and give a traditional model-theoretic account of the semantics. This may be less useful practically, for the reasons you give, but sometimes it’s nice to consider that a symbol “fred” might actually refer to a person called Fred rather than just be symbols all the way down... (It always surprises me when Prolog texts refer to the least Herband model as the “intended model” - it’s definitely not what I intend when I write Prolog!) So while we can say that an “ancestor” relation in Prolog correctly defines transitive closure within the least Herbrand semantics, at some point we actually have to relate that “semantics” to the real world if we want to know what our programs mean. Edit: putting this all another way, my understanding of (pure, positive) Prolog’s operational semantics is that the least Herbrand model contains exactly those sentences that are true in all models of the program, whether those models are Herbrand or otherwise. So it’s not quite true to say that Prolog only considers the least Herbrand model, but that it may as well only do so because the (operational) result will be the same. It’s been a while since I’ve looked at this any great depth though.
- YeGoblynQueenne 8y ago
  >> (It always surprises me when Prolog texts refer to the least Herband model as the “intended model” - it’s definitely not what I intend when I write Prolog!) Good point.
YeGoblynQueenne 8y ago
What you call an interpretation I know as a pre-interpretation (from Foundations of ILP by Nienhuys-Cheng and de Wolf which is my go-to textbook; I think you're going by Lloyd?). A pre-interpretation assigns objects in the domain to terms (including variables!), and an interpretation assigns truth values to atoms of predicates. This distinction is perhaps a bit unwieldy- but, how do you call a truth assignment to predicate atoms, if you call the mapping between entities in the domain of discourse and the terms in the language an "interpretation"? Or is that resolved by having a Herbrand interpretation? >> Yet, we can readily express these things in Prolog, and in fact almost every Prolog program also does that or needs them! Yes but Prolog cheats: it allows any (Prolog) term as an argument to a (Prolog) predicate, including another (Prolog) predicate, as in meta-predicates. Meta-predicates then are not strictly speaking first-order, and so Prolog is not strictly first-order. Or more to the point, Prolog doesn't make a distinction between constants and predicate symbols, or predicate atoms and functions. So it accepts as arguments to (Prolog) predicates (Prolog) terms that are syntactically identical to functions but have predicate symbols instead of function symbols. In FOL, the sets of predicate symbols and function symbols are disjoint, so you can't do that.
- triska 8y ago
  I used interpretation as it occurs for example in Computability and Logic by Boolos, Burgess and Jeffrey. It is also explained here: https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpretations_of_a_first-order_language https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpr... Please note that from a logical perspective, a (pure) Prolog program is always a set of first-order clauses, since all variables that occur in a Prolog program are implicitly quantified to range over individuals and hence terms, not over predicates or sets of predicates etc., which would be characteristic of second- and higher-order logic. This also includes meta-calls and meta-predicates! This is because, in Prolog, if a variable P occurs as a goal anywhere, it is interpreted as call(P), i.e., a universally quantified variable that is the argument of the predicate call/1. And call/1 is expressible in first-order logic, using at most one clause per predicate: call(true). call(X = Y) :- X = Y. call(dif(X,Y)) :- dif(X, Y). call(X #= Y) :- X #= Y. etc. So, even though Prolog programmers call predicates involving meta-calls "higher-order" programming (since predications are passed as arguments), it is not an instance of higher-order reasoning from a logical perspective. An example of a logical higher-order statement must quantify (at least) over predicates, so for example "For all unary predicates, the induction axiom is true." There is no way to express this in Prolog, because its universally quantified variables implicitly always range exclusively over domain elements (Herbrand terms), and you cannot quantify over predicates. Regarding all-solutions predicates like setof/3, which are also higher-order predicates in the sense of Prolog: These predicates are not monotonic (for example, adding a fact may cause a query to fail that previously succeeded), and they therefore do not correspond to predicates in classical logic, where entailment is monotonic.

by triska 8y ago

nmadden 8y ago

While Prolog’s operational semantics are given in terms of least Herband models (at least, before you consider negation), you can also view a Prolog program as a subset of FOL and give a traditional model-theoretic account of the semantics. This may be less useful practically, for the reasons you give, but sometimes it’s nice to consider that a symbol “fred” might actually refer to a person called Fred rather than just be symbols all the way down... (It always surprises me when Prolog texts refer to the least Herband model as the “intended model” - it’s definitely not what I intend when I write Prolog!) So while we can say that an “ancestor” relation in Prolog correctly defines transitive closure within the least Herbrand semantics, at some point we actually have to relate that “semantics” to the real world if we want to know what our programs mean. Edit: putting this all another way, my understanding of (pure, positive) Prolog’s operational semantics is that the least Herbrand model contains exactly those sentences that are true in all models of the program, whether those models are Herbrand or otherwise. So it’s not quite true to say that Prolog only considers the least Herbrand model, but that it may as well only do so because the (operational) result will be the same. It’s been a while since I’ve looked at this any great depth though.

YeGoblynQueenne 8y ago
>> (It always surprises me when Prolog texts refer to the least Herband model as the “intended model” - it’s definitely not what I intend when I write Prolog!) Good point.

YeGoblynQueenne 8y ago

What you call an interpretation I know as a pre-interpretation (from Foundations of ILP by Nienhuys-Cheng and de Wolf which is my go-to textbook; I think you're going by Lloyd?). A pre-interpretation assigns objects in the domain to terms (including variables!), and an interpretation assigns truth values to atoms of predicates. This distinction is perhaps a bit unwieldy- but, how do you call a truth assignment to predicate atoms, if you call the mapping between entities in the domain of discourse and the terms in the language an "interpretation"? Or is that resolved by having a Herbrand interpretation? >> Yet, we can readily express these things in Prolog, and in fact almost every Prolog program also does that or needs them! Yes but Prolog cheats: it allows any (Prolog) term as an argument to a (Prolog) predicate, including another (Prolog) predicate, as in meta-predicates. Meta-predicates then are not strictly speaking first-order, and so Prolog is not strictly first-order. Or more to the point, Prolog doesn't make a distinction between constants and predicate symbols, or predicate atoms and functions. So it accepts as arguments to (Prolog) predicates (Prolog) terms that are syntactically identical to functions but have predicate symbols instead of function symbols. In FOL, the sets of predicate symbols and function symbols are disjoint, so you can't do that.

triska 8y ago
I used interpretation as it occurs for example in Computability and Logic by Boolos, Burgess and Jeffrey. It is also explained here: https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpretations_of_a_first-order_language https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpr... Please note that from a logical perspective, a (pure) Prolog program is always a set of first-order clauses, since all variables that occur in a Prolog program are implicitly quantified to range over individuals and hence terms, not over predicates or sets of predicates etc., which would be characteristic of second- and higher-order logic. This also includes meta-calls and meta-predicates! This is because, in Prolog, if a variable P occurs as a goal anywhere, it is interpreted as call(P), i.e., a universally quantified variable that is the argument of the predicate call/1. And call/1 is expressible in first-order logic, using at most one clause per predicate: call(true). call(X = Y) :- X = Y. call(dif(X,Y)) :- dif(X, Y). call(X #= Y) :- X #= Y. etc. So, even though Prolog programmers call predicates involving meta-calls "higher-order" programming (since predications are passed as arguments), it is not an instance of higher-order reasoning from a logical perspective. An example of a logical higher-order statement must quantify (at least) over predicates, so for example "For all unary predicates, the induction axiom is true." There is no way to express this in Prolog, because its universally quantified variables implicitly always range exclusively over domain elements (Herbrand terms), and you cannot quantify over predicates. Regarding all-solutions predicates like setof/3, which are also higher-order predicates in the sense of Prolog: These predicates are not monotonic (for example, adding a fact may cause a query to fail that previously succeeded), and they therefore do not correspond to predicates in classical logic, where entailment is monotonic.