Prolog: Check that boolean predicate is of a certain form

Question

I am in first week of learning Prolog and I want to check that a boolean predicate is of a certain form. Specifically, I want to check that true or false is present in the first level or not at all. For example or(P, or(Q, true)) is not in this form since at the top level you have or, then P, or at the second, then Q, true at the third level.

I have the idea to count each level and perform recursion on each term(not sure if this is the right word to use), and check if true or false is present when the level is greater than 1.

Using the answer from here, I wrote the following to count the levels.

checker(Term) :- getLevel(Term, 0).
getLevel(or(T1, T2), L):- getLevel(T1, L+1), getLevel(T2, L+1).

How would I combine this with an if statement (if it exists) to check if there is a true and false and return fail if the level > 1? So or(P, or(Q, true)) would fail.

You have the right idea, but Prolog is not going to evaluate arithmetic expressions unless you use is to force it to, so you'll need to change your body to L1 is L+1, getLevel(T1, L1), getLevel(T2, L1). Using succ/2 instead is even better: succ(L, L1), ... — Daniel Lyons
Do you mean getLevel(or(T1, T2), L):- L1 is L+1, getLevel(T1, L1), getLevel(T2, L1). How would I incorporate this in an if statement? — dreamin

Daniel Lyons Daniel Lyons · Accepted Answer · 2019-02-23T08:14:34

The solution to this particular problem actually does not require any real arithmetic involving the level or any real conditional logic. I would handle it like so:

concrete_boolean(X) :- atom(X), (X = true ; X = false).

checker(or(P, Q)) :- \+ concrete_boolean(P), \+ concrete_boolean(Q).

This fulfills the requirement you stated ("check that true or false are not present in the first level") but this is contradicted by the example you gave ("or(P, or(Q, true)) is not in this form"). Because Prolog predicates succeed or fail rather than "returning", we often replace explicit boolean logic with predicates that appear to only handle the successful (true) case. When the pattern fails to match, the predicate will fail, and this gives us the branching behavior we wanted.

What you probably really are after here is a helper predicate that surfaces terms along with their depth in the tree, which you can then use in some other procedure. For instance, with getLevel/3, you could easily write a predicate that tests for explicit booleans only on odd or even levels of the hierarchy.

For this, you seem pretty close, but you are conflating things by having checker/1 provide the base case to getLevel/2. What I think you actually want is something like this:

getLevel(Term, Part, Level) :- getLevel1(Term, 0, Part, Level).
getLevel1(Term, L0, Term, L0).
getLevel1(or(Left, _), L0, LeftChild, LN) :- 
   succ(L0, L1), 
   getLevel1(Left, L1, LeftChild, LN).
getLevel1(or(_, Right), L0, RightChild, LN) :- 
   succ(L0, L1), 
   getLevel1(Right, L1, RightChild, LN).

I felt pretty good about this testing it with atoms, because it seems to do the right thing:

?- getLevel(or(p, or(q, true)), Term, Level).
Term = or(p, or(q, true)),
Level = 0 ;
Term = p,
Level = 1 ;
Term = or(q, true),
Level = 1 ;
Term = q,
Level = 2 ;
Term = true,
Level = 2.

However, when you try it with variables, things get a little weird:

?- getLevel(or(P,Q), Term, Level).
Term = or(P, Q),
Level = 0 ;
P = Term,
Level = 1 ;
P = or(Term, _2390),
Level = 2 ;
P = or(or(Term, _2396), _2390),
Level = 3 ;
P = or(or(or(Term, _2402), _2396), _2390),
Level = 4 .

This happens when an unbound variable is unified with one of our clause's heads. What started out as P is unified with or(Left, _) rather than just leaving it unbound.

The simplest and best way to resolve this is to decide if you actually want holes in your data structure like this, and if you do, annotate them. As an example:

?- getLevel(or(var(P),var(Q)), Term, Level).
Term = or(var(P), var(Q)),
Level = 0 ;
Term = var(P),
Level = 1 ;
Term = var(Q),
Level = 1.

Prolog also has some tests you can use, namely var/1 and nonvar/1 and ground/1 but in my experience using them usually introduces subtle problems (often with backwards-correctness or data structures with holes) so I'll just mention it here since I'm pretty sure I wouldn't find a correct solution that helps and handles all the weird cases.

Edit: Let's talk about handling variables explicitly.

We can modify what I have in the answer to handle this var/nonvar state:

getLevel(Term, Part, Level) :- getLevel1(Term, 0, Part, Level).
getLevel1(Term, L0, Term, L0).
getLevel1(T, L0, LeftChild, LN) :-
    nonvar(T), T = or(Left, _),
    succ(L0, L1), 
    getLevel1(Left, L1, LeftChild, LN).
getLevel1(T, L0, RightChild, LN) :-
    nonvar(T), T = or(_, Right),
    succ(L0, L1), 
    getLevel1(Right, L1, RightChild, LN).

Implementing checker/1 is fairly straightfoward with this:

checker(Term) :-
    \+ (getLevel(Term, Boolean, 1), 
        nonvar(Boolean), 
        (Boolean = true ; Boolean = false)).

It's tempting to do this instead:

checker(Term) :-
    \+ (getLevel(Term, Boolean, 1), 
        (Boolean = true ; Boolean = false)).

The problem here is that you'll surface P or Q in or(P,Q) and then bind them to true or false, which will then cause the rest of the expression to fail. Prolog really doesn't want you to conflate a domain-specific idea of variable with its internal sense of variable. We can sort of get away with it here using var/1 and nonvar/1 to protect our unifications and ensure they aren't happening against a totally unbound variable. But I remain anxious about the long-term effects and would regard it as a bit of a code smell if I saw it in someone else's program.

Prolog: Check that boolean predicate is of a certain form

1 Answers