3 ms·
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
by nmadden 7y 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 7y 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.