Do there exist a set of inductive rules and a fixed point of these rules but is neither the least nor the greatest fixed points?


Here's a non-trivial example:

Suppose we want to define inductively a subset of reals, so we work on the complete lattice $\mathcal{P}(\mathbb{R})$ ordered by inclusion.

Then, consider the rules $$ \dfrac{\qquad}{0} \qquad \dfrac{x}{x+1} $$ This induces the (monotonic, Scott-continuous) function $f : \mathcal{P}(\mathbb{R}) \to \mathcal{P}(\mathbb{R})$ given by $$ f(X) = \{0\} \cup \{ x+1 \ |\ x\in X\} $$

All of the following are fixed points of $f$:

  • $\mathbb{N}$ (least)
  • $\mathbb{Z}$
  • $\{x/2 \ |\ x\in \mathbb{Z}\}$
  • $\{x/3 \ |\ x\in \mathbb{Z}\}$
  • etc.
  • for any natural $k \geq 1$, the set $\{x/k \ |\ x\in \mathbb{Z} \}$
  • $\mathbb{Q}$
  • $\mathbb{R}$ (greatest)

If we want our definition to be well-formed, beyond specifying the rules, we need to single out one the fixed points. This is typically done by taking the least (induction) or the greatest (coinduction).

  • $\begingroup$ A minor nit, but without specifying least/greatest or some other property to uniquely pick out the appropriate subset, this doesn't inductively define a subset of the reals. $\endgroup$ – Derek Elkins left SE Mar 22 '17 at 3:35
  • $\begingroup$ @DerekElkins Agreed. I added a note about that. $\endgroup$ – chi Mar 22 '17 at 9:04
  • $\begingroup$ @DerekElkins The answer doesn't claim that it defines anything. It says to suppose that we want to define something, gives some rules and says that those rules have a whole bunch of fixed points. $\endgroup$ – David Richerby Mar 22 '17 at 9:06
  • $\begingroup$ @DavidRicherby Indeed, that was my intention. Still, I can see that it is possible to read a bit beyond what I wrote, so I added a final note anyway. $\endgroup$ – chi Mar 22 '17 at 9:11
  • 1
    $\begingroup$ @thbl2012 The greatest fixed point is very sensitive to the choice of the complete lattice you work on. Here, I started with $\mathbb{R}$ as the top element of my lattice, but I could have chosen e.g. $\mathbb{Q}$ or $\mathbb{C}$. Another common choice it the set of finite or infinite symbolic applications of the ocnstructors, where, as you say, you do have the largest fixed point being $\mathbb{N} \cup \{\infty\}$ where $\infty$ here represents the successor applied on itself infinitely many times. Hence, your professor is completely correct, (s)he simply chose another complete lattice. $\endgroup$ – chi Mar 22 '17 at 16:11

Any set is a fixed point of the empty set of rules or of the trivial rule $x\in X\Rightarrow x\in X$.


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.