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

[Fwd: Re: [PVS-Help] Transitive closure]






Shankar and Bruno,

Thank you for your kind and informative replies. At the time I wrote the
question, I was aware of the inductive definition of TC and another one
by Jerry James. (using indexed sets) However, I'm interested in defining
TC in a computational style, namely by using a recursive function. Let
me try to fix the bug in my previous email. Consider the following
recursive function definition in PVS:

closed?(R: pred[[T,T]])(C: pred[[T,T]]): boolean = EXISTS (i: posnat): C
= R^i  
CLOSED(R: pred[[T,T]]): TYPE = (closed?(R))

TC(R: pred[[T,T]])(C: CLOSED(R)): RECURSIVE pred[[T,T]] =
   IF C = union(C, R o C) THEN C
   ELSE TC(R)(union(C, R o C))
   ENDIF

where TC accumulates each successive approximation of the transitive
closure of R into C. The terminating condition is essentially the fix-
point. I believe it is possible to show that TC(R)(R) is a total
function by appealing to the fix-point theorem on CPOs. However, in the
case that R is infinite, TC(R) is not a computable function and cannot
be defined in PVS? (i.e. no measure function exists for TC(R))

Thanks again,

stan

P.S. Here is the power function used in the type definition:

^(R: pred[[T,T]], n: nat): RECURSIVE pred[[T,T]] =     
    IF n=0 THEN =[T]
    ELSE R o (R^(n-1))
    ENDIF
    MEASURE (LAMBDA (R: pred[[T,T]], n: nat): n)


On Thu, 2006-03-23 at 22:28 -0800, Natarajan Shankar wrote:
> 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
>