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

*To*: Bruno Dutertre <bruno@csl.sri.com>*Subject*: Re: [PVS-Help] Transitive closure*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Thu, 23 Mar 2006 22:28:18 -0800*Cc*: stan.rosenberg@acm.org, pvs-help@csl.sri.com*Comments*: In-reply-to Bruno Dutertre <bruno@csl.sri.com>message dated "Wed, 22 Mar 2006 11:46:29 -0800."*In-reply-to*: <4421A995.5040500@csl.sri.com>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <1143002939.2937.12.camel@localhost.localdomain><4421A995.5040500@csl.sri.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

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

**References**:**[PVS-Help] Transitive closure***From:*Stan Rosenberg <stan.rosenberg@acm.org>

**Re: [PVS-Help] Transitive closure***From:*Bruno Dutertre <bruno@csl.sri.com>

- Prev by Date:
**Re: [PVS-Help] Transitive closure** - Next by Date:
**[Fwd: Re: [PVS-Help] Transitive closure]** - Prev by thread:
**Re: [PVS-Help] Transitive closure** - Next by thread:
**[PVS-Help] Re: measure induction** - Index(es):