I have a predicate that relates a modal logic formula to its negative normal form. All connectives except the modal operators, conjunction, and disjunction are eliminated, and negation is pushed as far into the leaves of the expression as possible.
The rewrite/2✱ predicate has a catch-all clause rewrite(A, A). that is textually last. With this catch-all clause available, it's possible to extract a formula in negated normal form. In this example, e is a biconditional connective like in Łukasiewicz notation, and 4 and 7 are variables in the modal logic (and hence Prolog constants).
Z unified with the formula in negative normal form.
?- rewrite(e(4, 7), Z).
Z = a(k(4, 7), k(n(4), n(7)))
However, rewrite(<some constant>, <some constant>) always succeeds and I'd like it not to succeed. The catch-all clause really should be a catch-all, not something that could potentially fire if another clause is applicable.
?- rewrite(e(4, 7), e(4, 7)).
true.
I tried replacing the rewrite(A, A). with a guarded version:
wff_shallowly(WFF) :-
WFF = l(_);
WFF = m(_);
WFF = c(_, _);
WFF = f;
WFF = t;
WFF = k(_, _);
WFF = a(_, _);
WFF = n(_);
WFF = e(_, _).
rewrite(A, A) :- \+ wff_shallowly(A).
I thought that this would prevent the catch-all clause from being applicable if and only if A isn't headed by an atom/constructor with special meaning. However, after making that change, the rewrite always fails if invoked recursively.
?- rewrite(4, Z).
Z = 4.
?- rewrite(c(4, 7), Z).
false.
What's the correct way to set up a catch all clause.
✱ full text of program for reference:
% so the primitive connectives are
% l <-- necessity
% m <-- possibility
% c <-- implication
% f <-- falsehood
% t <-- truth
% k <-- conjunction
% a <-- alternative
% n <-- negation
% e <-- biconditional
wff_shallowly(WFF) :-
WFF = l(_);
WFF = m(_);
WFF = c(_, _);
WFF = f;
WFF = t;
WFF = k(_, _);
WFF = a(_, _);
WFF = n(_);
WFF = e(_, _).
% falsehood is primitive
rewrite(f, f).
% truth is primitive
rewrite(t, t).
% positive connectives
rewrite(a(A, B), a(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(k(A, B), k(C, D)) :- rewrite(A, C), rewrite(B, D).
rewrite(l(A), l(C)) :- rewrite(A, C).
rewrite(m(A), m(C)) :- rewrite(A, C).
% implication
rewrite(c(A, B), a(NC, D)) :-
rewrite(n(A), NC), rewrite(B, D).
% biconditional
rewrite(e(A, B), a(k(C, D), k(NC, ND))) :-
rewrite(A, C),
rewrite(n(A), NC),
rewrite(B, D),
rewrite(n(B), ND).
% negated falsehood is truth
rewrite(n(f), t).
% negated truth is falsehood
rewrite(n(t), f).
% double negation elimination
rewrite(n(n(A)), C) :- rewrite(A, C).
% negated alternation
rewrite(n(a(A, B)), k(NC, ND)) :-
rewrite(n(A), NC), rewrite(n(B), ND).
% negated conjunction
rewrite(n(k(A, B)), a(NC, ND)) :-
rewrite(n(A), NC), rewrite(n(B), ND).
% negated biconditional
rewrite(n(e(A, B)), a(k(C, ND), k(NC, D))) :-
rewrite(A, C),
rewrite(n(A), NC),
rewrite(B, D),
rewrite(n(B), ND).
% negated necessity
rewrite(n(l(A)), m(NC)) :- rewrite(n(A), NC).
% negated possibility
rewrite(n(m(A)), l(NC)) :- rewrite(n(A), NC).
% catch all, rewrite to self
rewrite(A, A) :- \+ wff_shallowly(A).
These problems all go away if you use a clean representation of your data.
In this case, it means that you shall, in complete analogy to how you represent all other entities systematically via different functors, also use a dedicated functor to represent (modal) variables.
For example, let us use the functor v/1 to represent variables. This means that we use v(1), v(7) etc. to represent the modal variables 1, 7 etc.
Instead of your "catch all" clause, I add the following clauses that state what holds about modal variables:
% (negated) variable rewrite(n(v(V)), n(v(V))). rewrite(v(V), v(V)).
Now we get:
?- rewrite(e(v(4), v(7)), Z). Z = a(k(v(4), v(7)), k(n(v(4)), n(v(7)))).
Note that we of course have to use the v/1 wrapper in queries, and also get the wrapper in answers. This is slightly harder to read and write than if the wrapper were not present. However, it makes reasoning about such formulas much easier, and I therefore strongly recommend to use it.
It is a straight-forward exercise to convert between such formulas and the defaulty representation you are currently using. It is called "defaulty" precisely because it requires a default ("catch all") case, and also because that is considered faulty. It is good practice to get rid of such representations as soon as possible, and then write the main logic around a clean representation.
A clean representation is good for generality, and also for efficiency: Your Prolog system's argument indexing can now readily tell all clauses apart via the principal functor of the first argument, and this improves performance in the important use case where that argument is fully instantiated (e.g., in the example you posted).