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

Re: [PVS-Help] Transitive closure




Stan:
  You can use inductive definitions for defining transitive closure
instead of recursion.  These are essentially like pure logic programs
where the predicate defined is the least fixed point of its defining
equivalence.  In the theory below, TC is the transitive closure
and RTC is the reflexive transitive closure.  

closures[ T : TYPE ]: THEORY
BEGIN
     
  relation: TYPE = pred[ [T, T] ]
  P, R: VAR relation
  x, y, z, w: VAR T

  TC(R)(x, y) : INDUCTIVE bool =
     R(x, y) OR (EXISTS z: TC(R)(x, z) AND TC(R)(z, y))

  RTC(R)(x, y) : bool = x = y OR TC(R)(x, y)

END closures

-Shankar

> From:    Bruno Dutertre <bruno@csl.sri.com>
> Subject: 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
> > 
> 
> Hello,
> 
> 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
> -- 
> Bruno Dutertre                             | bruno@csl.sri.com
> CSL, SRI International                     | fax: 650 859-2844
> 333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717