[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Transitive closure

Stan Rosenberg wrote:
> Hi Everyone,
> I would like to continue the discussion thread started by Andre
> regarding a recursive definition of transitive closure. Suppose I define
> 'TC' for an arbitrary R as follows:
> TC(R: pred[[T,T]]): RECURSIVE pred[[T,T]] =
>  lambda (x,y: T): R(x,y) OR 
>    TC(lambda (x,y: T): EXISTS (z: T): R(x,z) AND R(z,y))(x,y)
> (or equivalently the last line could be replaced by TC(R o R)(x,y) for
> readability if using the prelude)
> Is the above function well-defined? I can't think of a measure for the
> general case. (i.e. R is infinite) If on the other hand the claim is
> that no measure function exists, how would you prove the claim?
> Thanks so much,
> stan


This is not a well-defined recursive definition. There's no
measure for this. The definition is basically specifying

   TC(R) = R union TC(R o R).

To get a valid recursive definition, you need to find
a well founded ordering on pred[[T, T]] for which R o R is strictly
smaller than R (for any R). Such an ordering does not exist,
because there are relations R such that R o R = R.

Bruno Dutertre                             | bruno@csl.sri.com
CSL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717