1

If we consider a relation $R$ and then its symmetric-reflexive-transitive closure --say $R^*$--, is there a recursion principle associated with $R^*$?

It seems to me that such unique function is not able to distinguish between the symmetric-transitive cases. Makes sense?

Thanks in advance.

Alistair -L.
  • 163
  • 4
  • 1
    What kind of "recursion principle" are you looking for? Could you be more specific (or maybe give an example)? – Luca Bressan Sep 09 '13 at 17:22
  • @LucaBressan: Sure. If we consider the usual inductive definition of natural numbers, then its recursion principle says that there is only one function $f:\mathbb{N}\rightarrow X$ such that $f(0) = x$ and $f(n+1)=g(f(n), n+1)$, for $x\in X$ and $g:X\times\mathbb{N}\rightarrow X$. Does this helps? – Alistair -L. Sep 09 '13 at 18:35
  • I'm still not sure what you mean, because the natural numbers are not a binary relation. Are you thinking the relation $R$ as a dependent type in a suitable type theory? – Luca Bressan Sep 09 '13 at 18:45

1 Answers1

1

I think that the best setting in which your problem could be approached is that of proof-relevant dependent type theories, but I'll try to give you an answer that doesn't rely on much theory.

What you call "recursion principle" is easy to state for natural numbers for the simple reason that, given $n$, there is only one way to prove that it is a natural number: either $n = 0$, so the proof follows by the axiom that $0 \in \mathbb{N}$, or $n = \mathsf{s}(m)$, and so one reduces to prove that $m$ is a natural number (and goes on in this way).

For a given binary relation $S \subseteq D \times D$ and $x, y \in D$ there could be more than one proof for $x S y$. For example, consider a relation $R$ and the smallest equivalence relation $R^*$ containing $R$, as in your question. If $x R x$ for some $x$, then $x R^* x$ could be proven either from the fact that $x R x$ or from the reflexivity of $R^*$. In a proof-relevant environment this distinction matters.

So, in order to construct a recursion principle, we need to consider the sets $R^*(x, y)$ of "proofs that $x R^* y$" for all $x, y$. These sets could be defined inductively in this way:

  1. If $x R y$, then $\mathsf{sup}(x, y) \in R^*(x, y)$ (a proof that $xRy$ is a proof that $x R^* y$, i.e. $R^* \supseteq R$);
  2. If $x = y$, then $\mathsf{refl}(x, y) \in R^*(x, y)$ (reflexivity);
  3. If $s \in R^*(y, x)$, then $\mathsf{sym}(s) \in R^*(x, y)$ (symmetry);
  4. If $s_1 \in R^*(x, z)$ and $s_2 \in R^*(z, y)$, then $\mathsf{trans}(s_1, s_2) \in R^*(x, y)$ (transitivity).

Then the recursion principle is the following (I denote $A \rightarrow B$ the set of functions from $A$ to $B$ for simplicity; $\prod$ is the cartesian product):

Let $X$ be a set, and suppose we are given functions $$f \in R \rightarrow X,$$ $$g \in D \rightarrow X,$$ $$h \in \prod_{y \in D} \prod_{x \in D} (R^*(y, x) \times X \rightarrow X),$$ $$k \in \prod_{x \in D} \prod_{z \in D} \prod_{y \in D} (R^*(x, z) \times X \times R^*(z, y) \times X \rightarrow X)$$ Then there is a unique function $$F \in \prod_{x \in D} \prod_{y \in D} (R^*(x, y) \rightarrow X)$$ such that: $$F(\mathsf{sup}(x, y)) = f(x, y)$$ $$F(\mathsf{refl}(x, y)) = g(x) = g(y)$$ $$F(\mathsf{sym}(s)) = h(s, F(s))$$ $$F(\mathsf{trans}(s_1, s_2)) = k(s_1, F(s_1), s_2, F(s_2))$$

Luca Bressan
  • 6,845
  • Oh, fantastic! I like that specially because I was trying to come up with something similar. Just for your information, I am toying with various alternative but equivalent $\alpha$-equivalence definitions in the context of $\lambda$-calculus; thus, the binary relation I was thinking of was $\alpha$-conversion. I am not familiar with dependent type theory. Very much appreciated your effort, and kudos for the presentation. – Alistair -L. Sep 09 '13 at 20:05
  • You're welcome. I can't see how this could be related to $\alpha$-conversion, but $\lambda$-calculus is indeed connected to type theory in general. If you want you could try to describe recursion principles for simpler (non-dependent) types, as the type of binary trees or lists. In the literature they are called "elimination rules". – Luca Bressan Sep 09 '13 at 20:13