Then they can be expressed independently as a disjunction of literals, one of them is positive (atDesk).
Then what about the directives?
:- tasty(F), writeln(F), false; true.
If we break it, it will behave differently from the procedural point of view.
I try to develop my own simple Prolog implementation and would like to base it on precise mathematical model, so a program is a list of Horn Clauses, but there are problems…
Who says so? SWI-Prolog creates a choice point internally in the body VM code. Try ?- vm_list(atDesk). I think SICStus does indeed create clauses (not sure), but like so:
Thank you, I tried vm_list(atDesk). Very interesting, it looks like some kind of Asseembly language with a list of commands and GoTOs. Is it how you really store the clauses in SWI Prolog internal representation? Why this procedural format was chosen over structural (list of literals with disjunction between them)?
In the end, modern computers process instructions. We have three options: (1) interpret, i.e., process the representation as is, (2), compile to native code or (3), compile to a VM. That is what most Prolog implementations do. The VM is designed to deal with Prolog, so things like unification, backtracking, choicepoints etc. are VM primitives. The most well known VM is the WAM. SWI-Prolog is (very loosely) based on the ZIP VM. You most notably gain by avoiding full unification based on analysis by the compiler. As a result, many unifications become simple assignment (one side is known to be a variable) or comparison to a constant, etc.