" Declaratively, Prolog programs state what holds . A Prolog program consists of clauses , and each clause is either a fact or a rule . Facts state what is always true. Rules state what is true under certain conditions .
I think this is exactly the beauty of Prolog.
Declaratively, you describe what holds … and you can then treat (and perhaps even derive) from this description several procedural “interpretations” … based on the calling context – and they all hold.
In declarative description what holds is specified explicit, whereas in an imperative language – its implicit in the semantics of the imperative language construct.
Perhaps one way to further clarify this line of thought is to think about Eiffel’s contracts – which specify what holds after the execution of a function.
Here is a paper on semantics of imperative operations:
I think at issue here is whether you can reason about the description – in Prolog the description of what holds enables you to reason about it – whereas in imperative languages – what holds is, as i said, implicit, and if you want to reason about it you have to match each statement (and expression) up with its a description of what holds – i.e. its semantics.
So, i guess, what Markus is referring to as declarative is indeed focused on pure prolog without side-effects.
If i gather this correctly, the meaning of the Prolog program – which shows what facts for given goals hold – is then given by the model found which is based on a particular database state.
I took this understanding, that all facts that are derivable from a program (its rules and facts) are the intended meaning of a program from Shapiro’s Art of Prolog - Shapiro phrased it as so (p.15):
Definition: The meaning of a logic program P, M(P) is the set of ground unit goals deductive from P.
I guess, this is more narrow than strictly necessary.
re: your example with tnot
I searched a bit on semantics of Prolog and there are various approaches, including the approach taken by XSB prolog and now being incorporated into swi-prolog.
The essence i guess is to expand to multi-valued logic – 3 (or even 4) logic states – with one logic state enables reasoning in light of paradoxes – where the logic program can not derive true or false, but leaves it undefined.
I wish I could more deeply understand those approaches.
But, perhaps this is a good reason to start using tabling, also as a means to increase expressiveness – and thereby also the broaden the meaning of logic programs.
I think your tnot example is side-effect free, yet, it does require extending the definition given by Shapiro … since, as you indicated, one wouldn’t, otherwise, find a ground model for it – and it is a valid Prolog program.
I am trying to make sense of the exact meaning of tnot … and its hard to get my heard around it, first because the section in the swi manual on well founded semantics resolution procedure is not penetrable for me [1] (nor the formal papers referred to in the comments, discussing various semantic models).
And second: looking up tnot in XSB manual [2] it states that tnot does not include a cut – which consequences i am still trying to understand.
:tnot/1 on the other hand, does not execute a cut, so that all subgoals in the computation path begun by the negative call will be completely evaluated. The major reason for not executing the cut is to insure that XSB evaluates ground queries to Datalog programs with negation with polynomial data complexity"