I'm new to Prolog and logic programing in general, I'm writing a small theorem prover for fun, and in doing so I wrote a normalization procedure. I wanted this procedure to be deterministic and steadfast, so I wrote something like this :
normal(S, R):- var(S), !, S = R.
normal(true(S), R):- !, normal(S, R).
normal(!(S), R):- !, normal(false(S), R).
normal(P => Q, R):- !, normal(false(P and false(Q)), R).
normal(A or B, R):- !, normal(false(false(A) and false(B)), R).
normal(false(S), R):- !, normal(S, NS), normal_false(NS, R).
normal(A and B, R):- !, normal(A, NA), normal(B, NB), normal_and(NA, NB, R).
normal(S, S):- !.
normal_false(S, R):- var(S), !, S = false(R).
normal_false(false(S), S):- !.
normal_false(true, false):- !.
normal_false(false, true):- !.
normal_false(S, false(S)):- !.
normal_and(A, B, R):- var(A), var(B), !, R = A and B.
normal_and(A, true, A):- !.
normal_and(true, B, B):- !.
normal_and(_, false, false):- !.
normal_and(false, _, false):- !.
normal_and(A, B, A and B):- !.
I'm now wondering if this was the right way to do it. It currently seems to work, but I'm wondering if this might not fit the properties I'm expecting in some edge-cases, if there might be some performance problems with the way I wrote it, or if this is just bad coding style/practice in general.
Several questions arise when using the cut.
There are several possibilities here. Starting from pure programs that can be understood declaratively by considering the set of solutions only. In such programs a lot of desirable properties hold, but yours is clearly not one of those. After all, the goal normal_false(false, true) succeeds, yet its generalization normal_false(V, true) fails (as intended). So normal_false/2 is not a pure relation.
Your program treats Prolog variables as objects. It is rather a meta-logical program which is not surprising as you want to implement a prover by reusing Prolog's infrastructure. Here, still many of the nice properties hold, you may for example still use a failure-slice to identify reasons for non-termination. However, using var/1 is particularly error-prone since Prolog cannot enumerate all possible solutions and as a consequence, it is very easy to forget a case or two. In your example (after adding the missing operator declarations):
?- normal(X and true, N).
X = N. % expected
?- normal(true and X, N).
X = true, N = true. % unexpected
In normal/2 in the first clause normal(S, R):- var(S), !, ... the cut ensures that all subsequent clauses consider only the case nonvar(S).
Suspicious is the last clause normal(S, S):- !. which cuts if the arguments unify. At first sight that does not make a difference as it is the last clause. But you would get different results in case of, say freeze(S, ( T = 1 ; T = 2 ) ). But otherwise, normal/2 seems quite OK.
Much less convincing are the cuts in normal_and/2. In addition to above anomalies, this definition is not steadfast. After all, the outcome is influenced by its last argument:
?- normal(true and true, N).
N = true. % expected
?- normal(true and true, true and true).
true. % unexpected
Here the cut came too late.