Re: predicate definitions in CASL

[Dieter Hutter <hutter@dfki.de>]

[Note: several answers below. BKB]

Don,

> 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)

what about predicates like:

         p(x) <=> (q(x) => T) /\ (not q(x) => p(x))

It's a trick to get p under-specified in case not q(x) holds.

another example is:

   odd(x) <=> (x = 0 \/ (x = suc(suc(pre(pre(x)))) => odd(pre(pre(x))))

which is far from fully determined.

Dieter
----------------------------------------
From: Maura Cerioli <cerioli@disi.unige.it>
To: cofi-language@brics.dk
Subject: Re: predicate definitions in CASL

I'm not sure if I got the point...but I try to answer anyway.

> That is, it appears to me that p(v1,...) is fully determined if F
> contains no occurrence of p 
I suppose you can also have circular definition, using q in F and
defining q in terms of p...but let's say that if no recursion is around
I basically agree
> 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.
I thought that the v1 had to be a variable, so the meaning of "strictly
less argument" it's not fully clear to me.
Moreover, I don't understand if you want an example where there is a
well-founded ordering or if any example is ok.

I think that

datatype int ::= 0 | s(int) | p(int)
var x:int
axioms s(p(x)) = x
       p(s(x)) = x
pred   double(x,y:int)<=> (x=0 and y=0) or double (p(x), p(p(y)))

has (reasonable) models where double is interpreted as
{(n,2n) | n>=0} or as {(z,2z) | z in Z}

But I think that also
{(z,2z) | z in Z} U {(z,2z+1) | z in Z}
is acceptable.

The formula F can be phrased also as
(x=0 and y=0) or 
{exist x1,y1:int. x= s(x1) and y= ss(y1) and double (x1, y1)}
Would you consider this an example of "strictly less arguments"?

Best regards, Maura