# Finding reflexive, transitive closure

I got a relation like: R: A -> A -> bool.

Using this, I need to find an Rclose: A -> A -> bool such that Rclose is the reflexive, transitive closure of R.

Am trying to do this in Coq in such a way that the resultant Rclose won't have any Prop component and would be computation-friendly. Along with a proof of correctness saying that Rclose really is the refl-trans closure of R.

I was told that this would be a non-trivial thing to do. Any thoughts on directions in which I can explore?

I can reformulate R to another type if needed if the meaning can be preserved.

How can one go about stating the theorem?

Would this be enough?

Inductive path (R: A -> A -> bool): Prop :=
| Self: forall a:A, path R a a
| Step: forall a b c:A,
path R a b -> path R b c -> path R a c.

Theorem foo (A: Type): forall x y:A,
Rclose x y <-> path R x y.


Edit:

I can assume that A is a finite type.

In fact, I had been thinking of making a type like this:

Inductive typ: Type :=
| One: typ
| Add: typ -> typ -> typ.

Fixpoint denote (t: typ): Type :=
match t with
| One => unit
| Add a b => (denote a)+(denote b)%type
end.


and having A like forall t:typ, denote t.

As in, forall {t: typ}, R: denote t -> denote t -> bool

Does that make finding closure possible?

• As noted in Meven's answer this isn't possible in general. Do you have an assumption on A, such as that A is finite, that would make this possible? Commented Jun 24 at 11:22
• In that case, finding the closure of R amounts to writing a (verified) algorithm for finding paths in finite undirected simple graphs. Commented Jun 25 at 7:58
• @NaïmFavier How does one go about doing that? And by R x y, I meant a one-way link. Then I should be looking at a directed graph, right? Commented Jun 25 at 9:46
• Why do you care about extraction? Are you fine with a very naïve algorithm, with terrible efficiency? In any case, you will need quite a bit of non-trivial machinery around finite sets, finite existentials… One good reference point might be MathComp's version of closure, which is nicely boolean, see here: github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/… (however, it is not designed for extraction, but for small-step computation in Coq). Commented Jun 25 at 9:56
• Indeed, if you don't want a symmetric closure then it should be directed graphs. Commented Jun 25 at 10:44

To state it precisely, you assume a type A and decidable relation R : A -> A -> bool (the fact that it targets bool is the decidability part). And you would like to define some Rclose : A -> A -> bool representing its reflexive-transitive closure. However, not all decidable relations have a decidable reflexive-transitive closure.
For instance, take A to be a type of Turing machine states, and R to encode transitions. It is decidable, given two states, whether one can go from one state to another. However, the reflexive transitive closure of R encodes full runs. In particular, if halts : A represents a finished run, Rclos R A halts holds iff A is the starting state of a halting computation. And the halting problem being undecidable says you cannot have such a function…
• Would it be possible if I can say that A is a finite type? I edited the question to include some more detail. Would closure be possible then? Commented Jun 25 at 3:41