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

[PVS-Help] Transitive closure

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,