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

*To*: stan.rosenberg@acm.org*Subject*: Re: [PVS-Help] Transitive closure*From*: Bruno Dutertre <bruno@csl.sri.com>*Date*: Wed, 22 Mar 2006 11:46:29 -0800*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <1143002939.2937.12.camel@localhost.localdomain>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com*User-Agent*: Mozilla Thunderbird 0.7.3 (X11/20040803)

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:
**[PVS-Help] Transitive closure** - Next by Date:
**Re: [PVS-Help] Transitive closure** - Prev by thread:
**[PVS-Help] Transitive closure** - Next by thread:
**Re: [PVS-Help] Transitive closure** - Index(es):