[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