Does every clause in prolog correspond to exactly one Horn clause or not?

When we use the OR (;), it seems that Prolog internal engine breaks the clauses into several Horn clauses:

atDesk(R) :- isMorning, receptionist(R); seniorManager(R).

Is broken into

atDesk(R) :- isMorning, receptionist(R); 
atDesk(R) :- seniorManager(R);

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…

I think you’re really talking about a choicepoint: SWI-Prolog -- Glossary of Terms

E.g. this does not translate into multiple Horn clauses:

?- X = 5, (Y = 1 ; Y = 2), Y = 2.
X = 5,
Y = 2.

Edit: There can be many layers of brackets and choicepoints. It’s all about the choicepoints :grinning_face:

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:

atDesk(R) :- helper(R).
helper(R) :- isMorning, receptionist(R).
helper(R) :- seniorManager(R).

Both approaches have their advantages.

1 Like

Just in case the original post had tried to compare the original clause to:


atDesk(R) :- isMorning, receptionist(R);
atDesk(R) :- seniorManager(R);

during some troublkeshooting step.. Yes it would be differnt (using semicolons rather than periods)

Then what about the directives?
:- tasty(F), writeln(F), false; true.

You could look at it like?

% rewrite it to 
temp_helper:- tasty(F), writeln(F), false; true.
% do your canonicalization

% call it
:- temp_helper.

Maybe?

The more impls of prolog I’ve used, the less agreement on the operator priority of ; vs , . (so I dont know which of these you meant).

:- tasty(F), writeln(F), (false; true).

:- tasty(F), ((writeln(F), false); true).

:- (tasty(F), writeln(F), false); (true).

Also, dont know if directives are to suceed only once? or if a all solutions are expected?

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)?

Yes (well, in binary form of course)

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.

3 Likes

Thank you for technical details