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

*To*: pvs-help@csl.sri.com*Subject*: [Fwd: Re: [PVS-Help] Transitive closure]*From*: Stan Rosenberg <stan.rosenberg@acm.org>*Date*: Tue, 28 Mar 2006 02:53:04 -0500*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>*Reply-To*: stan.rosenberg@acm.org*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

To: Natarajan Shankar <shankar@csl.sri.com>Subject: Re: [PVS-Help] Transitive closureFrom: Stan Rosenberg <stan.rosenberg@acm.org>Date: Tue, 28 Mar 2006 02:51:17 -0500In-reply-to: <200603240628.k2O6SIel019829@positron.csl.sri.com>References: <1143002939.2937.12.camel@localhost.localdomain><4421A995.5040500@csl.sri.com><200603240628.k2O6SIel019829@positron.csl.sri.com>Reply-to: stan.rosenberg@acm.orgShankar 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 >

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