I'm trying to solve an exercise on inductive definitions, the premiss is:

Let $\to$ be a relation on $A$ and $\to^*$ its reflexive, transitive closure, which is defined by following two rules:

  1. $a \to^*a$ (reflexive)
  2. ${a \to^*b \quad b \to c \over a \to^*c }$ (step)

The questions are:

  1. What are the induction rules for $\to^*$?
  2. Show that $\to^*$ is reflexive.
  3. Show that $\to^*$ is transitive.

The first question startles me, I view ${a \to^*b \quad b \to c \over a \to^*c }$ as the induction rule. Is this the complete answer?

And can I show the reflexivity with ${a \to^*b \quad b \to a \over a \to^*a }$?


Here's a fully formal articulation in the language of Agda. First, inductive rules correspond to indexed families.

data Star {A : Set}(R : A → A → Set) : A → A → Set where
    Refl : {a : A} → Star R a a
    Trans : {a b c : A} → Star R a b → R b c → Star R a c

Here the Refl data constructor corresponds to your first rule, and the Trans data constructor corresponds to your second rule. R represents $\to$, so Star R corresponds to $\to^*$. The induction rule corresponds to the eliminator for the data type, i.e. roughly the fold on that type (though things are a bit more complicated in a dependently typed language).

ind : {A : Set}{R : A → A → Set}{P : A → A → Set} 
    → ({a : A} → P a a) → ({a b c : A} → P a b → R b c → P a c)
    → {a b : A} → Star R a b → P a b
ind r t Refl = r
ind r t (Trans s x) = t (ind r t s) x

This says that if you give me some binary relation $P$ and you show that $\forall a \in A. P(a,a)$ holds and $\forall a,b,c\in A. P(a,b)\land R(b,c) \Rightarrow P(a,c)$ (i.e. when $P(a,b)$ and $R(b,c)$ hold, then $P(a,c)$ holds) then I can provide you a proof of $P(a,c)$ whenever $R^*(a,c)$ holds, where $R^*$ is the reflexive, transitive closure of $R$.

Question 2 is completely trivial. The formal proof of the statement is Refl. Question 3 is not much harder. It's asking to show that if $a \to^* b$ and $b \to^* c$ then $a \to^* c$, while the inductive rule only gives the case when $b \to c$ in a single step. Obviously, we just need to recursively apply the single-step rule. This leads to the following code:

trans : {A : Set}{R : A → A → Set}{a b c : A} → Star R a b → Star R b c → Star R a c
trans r Refl = r
trans r (Trans s x) = Trans (trans r s) x

For your purposes, you should probably define the equivalent of trans in terms of the induction rule, i.e. in terms of ind. I'll leave that as a very simple exercise.

  • $\begingroup$ Thanks for the explanation. It helped me understand the Star type in Agda. $\endgroup$ – Henry Story Oct 28 '20 at 13:03
  1. No. Induction rules for this case look like this:

    Let $P$ be some property of relations on $A$ (you already know some examples of such properties: symmetry, transitivity, etc.). To show that $P(\rightarrow^*)$ holds Let $P$ be some binary relation on $A$. To show that $P(a, b)$ holds whenever $a \rightarrow^* b$, it should be enough to prove something that only mentions $\rightarrow$ and $P$, but not $\rightarrow^*$. What? Namely, there will be 2 premisses, one corresponding to "reflective" and another to "step".

  2. Well, first you'd need to prove that $a \rightarrow^* b$ and $b \rightarrow a$ hold for any $a$ and $b$, and of course you can't. The puzzling thing is that the proof is utterly trivial. Does it maybe say "transitive" instead?

  • $\begingroup$ Also - proving transitivity is the next subtask. Since you already mentioned it, I'll include it :) $\endgroup$ – mike Apr 24 '17 at 14:42
  • 3
    $\begingroup$ 2. Surely $\to^*$ is reflexive, by definition rule 1: $a \to^*a$. $\endgroup$ – Thumbnail Apr 24 '17 at 14:43
  • $\begingroup$ Could you elbaborate on 1, e.g. transitivity only comes into play when you consider $\to^*$, not if you only look at $\to$. $\endgroup$ – mike Apr 24 '17 at 14:59
  • $\begingroup$ What I currently have for 1 is: ${n~\in~\mathbb{N}\quad \to^*:= \to^n \quad P(\to^{n-1}~\circ~\to)\over P(\to^n) }$ $\endgroup$ – mike Apr 24 '17 at 14:59
  • $\begingroup$ @mike I did (decided to add a paragraph there instead of a comment). I'll tell you that your suggested answer is wrong because 1) the conclusion should be $P(\rightarrow^*)$; 2) $:=$ normally means "set". It makes no sense to place as a premise of a rule. If you mean "equals", then this rule would be inapplicable whenever there is no such $n$: a very simple example is $A = \mathbb{N}, P(x,y) := y = x+1$. $\endgroup$ – Alexey Romanov Apr 24 '17 at 15:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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