3
$\begingroup$

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?

$\endgroup$
8
  • $\begingroup$ 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? $\endgroup$ Commented Jun 24 at 11:22
  • 1
    $\begingroup$ In that case, finding the closure of R amounts to writing a (verified) algorithm for finding paths in finite undirected simple graphs. $\endgroup$ Commented Jun 25 at 7:58
  • 1
    $\begingroup$ @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? $\endgroup$
    – J...S
    Commented Jun 25 at 9:46
  • 1
    $\begingroup$ 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). $\endgroup$ Commented Jun 25 at 9:56
  • 1
    $\begingroup$ Indeed, if you don't want a symmetric closure then it should be directed graphs. $\endgroup$ Commented Jun 25 at 10:44

1 Answer 1

6
$\begingroup$

If I understand what you are requiring correctly (as "won't have any Prop component and would be computation-friendly" is a bit vague), what you are asking for is impossible.

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…

$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – J...S
    Commented Jun 25 at 3:41
  • $\begingroup$ By 'no Prop component', I meant extractable. $\endgroup$
    – J...S
    Commented Jun 25 at 3:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.