[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
predicate definitions in CASL
A quick question about predicate definitions in CASL.
The CASL Language Summary says that in
p(v1,...) <=> F
p may appear in F and may have any interpretation satisfying the
equivalence.
I am trying to explain this to a student and can't think of any
example of when the "any interpretation" part would come into play
apart from silly things like
p(x) <=> p(x)
That is, it appears to me that p(v1,...) is fully determined if F
contains no occurrence of p or if every occurrence of p in F has an
argument that is strictly less than (v1,...) in some well-founded
ordering, with the same reasoning as for recursively-defined
functions.
Can anybody help, by providing a counterexample or confirming that
none exists? I'm sure that this is either obvious or wrong.
Best regards, Don