A (possibly partial) characteristic function
defined via conditional equations is better than
a PROLOG-like defined predicate because it works well in all data models,
while the predicate needs an initial or a free model.
For example, for l denoting finite lists
head(cons(x,l)) = x
tail(cons(x,l)) = l
null(nil) = true
null(cons(x,l)) = false
memberp(x,l) = true <-- null(l) = false, head(l) = x
memberp(x,l) = true <-- null(l) = false, memberp(x,tail(l)) = true
memberp(x,l) = false <-- null(l) = true
is better than
head(cons(x,l)) = x
tail(cons(x,l)) = l
NULL(nil)
NOTNULL(cons(x,l))
MEMBER(x,l) <-- NOTNULL(l), MEMBER(x,tail(l))
MEMBER(x,l) <-- NOTNULL(l), head(l) = x
For infinite streams l, however, we need
the free model also for the version with the characteristic functions
when we want to guarantee that,
for an infinite list l in that x does not occur,
memberp(x,l) to is unequal to true.
(CP, 1998)
It does not seem to be completely superfluous to note that
the better specification of the previous item is not good.
The following versions are getting better:
Firstly, there is a version with less function symbols:
memberp(x,cons(y,l)) = true <-- y = x
memberp(x,cons(y,l)) = true <-- memberp(x,l) = true
memberp(x,nil ) = false
Secondly, there is a version which is inductively equivalent but
deductively stronger:
or(true ,y ) = true
or(false,y ) = y
or(x ,true ) = true
or(x ,false) = x
eq(x,y) = true <-- x = y
eq(x,y) = false <-- x=/=y
memberp(x,cons(y,l)) = or(memberp(x,l),eq(y,x))
memberp(x,nil ) = false
Finally, there is a version that combines both advantages:
memberp(x,cons(y,l)) = true <-- y = x
memberp(x,cons(y,l)) = memberp(x,l) <-- y=/=x
memberp(x,nil ) = false
This last version is really the best. It has the same deductive
strength as the second. It has the same number of function symbols
as the first. Moreover it provides the easiest unfolding via a
complete case analysis (first syntactically, second semantically
on y=x).
(CP, 2005)