Prolog parsing malfunctioning

Question

My code takes an expression like or(lit(true),lit(X)),X) and outputs it as a list of lists.

 tocnf(Tree, Expr) :-
    trans(Tree ,Expr, []).

 trans(lit(X)) -->bbool(X).
 trans(or(lit(X1),lit(X2))) --> bconj(X1), bdisj(X2).
 trans(and(lit(X1),lit(X2))) --> bbool(X1), bconj(X2).

 bdisj(Conj) --> bconj(Conj).

 bconj(Bool) --> bbool(Bool).

 bbool(X) --> [[X]].

this code should take something like

tocnf(lit(X),X) 

output it as

[[X]]

or

 tocnf(or(lit(true),lit(X)),X)  

and output it as

[[true],[X]].

Question is why when I do

  tocnf(or(lit(true), and(lit(X),lit(true))),X) 

it outputs

 false.

Answer 1

Preliminaries

First, a note on style: You should always use the phrase/2 interface to access DCGs, so write tocnf/2 as:

tocnf(Tree, Expr) :-
        phrase(trans(Tree), Expr).

Further, tocnf/2 is a rather imperative name, since it implies a direction of use ("to" CNF). However, the relation also makes sense in other directions, for example to generate answers. Therefore, try to find a better name, that does justice to this general nature of Prolog. I leave this as an exercise.

Declarative debugging

Now, on to your actual question. Apply declarative debugging to find the reason for the failure.

We start with the query you posted:

?- tocnf(or(lit(true), and(lit(X),lit(true))), X).
false.

This means that the program is unexpectedly too specific: It fails in a case we expect to succeed.

Now, we generalize the query, to find simpler cases that still fail. This is completely admissible because your program is written using the monotonic subset of Prolog, as is highly recommended to make declarative debugging applicable.

To generalize the query, I use variables instead of some subterms. For example:

?- tocnf(or(lit(_), and(lit(X),lit(true))), X).
false.

Aha! This still fails, and therefore every more specific query will also fail.

So, we proceed like this, using variables instead of some subterms:

?- tocnf(or(lit(_), and(lit(X),lit(_))), X).
false.

?- tocnf(or(_, and(lit(X),lit(_))), X).
false.

?- tocnf(or(_, and(_,lit(_))), X).
false.

?- tocnf(or(_, and(_,_)), X).
false.

All of these queries also fail.

Now, we take it just one step further:

?- tocnf(or(_, _), X).
X = [[_G793], [_G795]].

Aha! So we have found a case that succeeds, and one slightly more specific though still very simple case that fails:

?- tocnf(or(_, and(_,_)), X).
false.

This is the case I would start with: Think about why your relation does not work for terms of the form or(_, and(_,_)).

Automated solution

A major attraction of pure monotonic Prolog is that the reasoning above can be automated:

The machine should find the reason for the failure, so that we can focus on more important tasks.

One way to do this was generously made available by Ulrich Neumerkel.

To try it out, you need to install:

1. library(diadem) and
2. library(lambda).

Now, to recapitulate: We have found a query that unexpectedly fails. It was:

?- tocnf(or(lit(true), and(lit(X),lit(true))), X).
false.

To find a reason for this, we first load library(diadem):

?- use_module(library(diadem)).
true.

Then, we repost the query with a slight twist:

?- tocnf(or(lit(true), and(lit(X),lit(true))), X).?Generalization.

That is, I have simply appended ?Generalization. to the previous query.

In response, we get:

Generalization = tocnf(or(_, and(_, _)), _) .

Thus, Generalization is a more general goal that still fails. Since the Prolog program we are considering is completely pure and monotonic, we know that every more specific query will also fail. Therefore, I suggest you focus on this simpler and more general case, which was found automatically in this case, and is the same goal we also found manually after several steps.

Unexpected failure is a common issue when learning Prolog, and automated declarative debugging lets you quickly find the reasons.