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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] Transitive closure*From*: Stan Rosenberg <stan.rosenberg@acm.org>*Date*: Tue, 21 Mar 2006 23:48:59 -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

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

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