2
$\begingroup$

I want to start off with a disclaimer that I am only a mathematical amateur. Please forgive me for ignorance or any non-standard nomenclature I use here :)

Let's start off with some context.

Let X be a set and < be a binary relation on X (though the use of < is merely suggestive. It has no restrictions related to ordering on it).

Let x be an element of X. We call x accessible under < iff for every element y in X such that y < x, y is also accessible under <. Intuitively, starting at x, all chains x_n < ... < x_1 < x are finite.

(As Joel David Hamkins reminds me, we are concerned with the "smallest" such notion of accessibility. This means that a proof of accessibility forms a finite tree.)

(To clarify Brian Rushton's comment, the only base case is the vacuous case. If there is no element y in X which satisfies y < x, then x is accessible under <).

We say X is well-founded under < iff every element x in X is accessible under <.

This formulation of well-foundedness has a particularly useful for my purposes because it allows us to convert weak induction to strong induction, and it allows us to do so using an arbitrary relation < (assuming we can prove the necessary lemma of well-foundedness).

My ultimate goal is to allow a programmer to write a recursive function using general recursion, then automatically convert it to structural recursion (together with the unproven lemma of well-foundedness mentioned above).

I already know how to do this for recursion.

My problem is that I don't know how to do this for co-recursion.

Co-recursion is analogous to co-induction, which is as I understand it, somewhat non-standard in mathematics. Categorically, I know induction and co-induction are dual to each other. I am convinced there is a dual notion to well-foundedness and accessibility above.

Does anyone know if there is research or writing on this subject? The only possible lead I have seen so far is a paper entitled Non-Wellfounded Sets by Peter Aczel. Any other resources, help, or advice would be greatly appreciated!

Improve this question
$\endgroup$
7
  • $\begingroup$ Your definition of accessible seems to be inductively defined without a 'base case', so that it doesn't seem to be a strong condition. For instance, if $<$ is equality, we can define any subset to be accessible and it will satsisfy the condition. And if $<$ is any relation at all, we can define all elements to be accessible and it satisfied the condition. Does this seem right or is there something missing? $\endgroup$
    – Brian Rushton
    Nov 29, 2012 at 23:34
  • 2
    $\begingroup$ In order to have a well-defined notion of "accessible", you should also say that you want the smallest notion with that property. In other words, you want the least fixed point of the operation you have set up. This will make the collection of accessible points the same as what is normally called the well-founded part of the relation. If you don't qualify the definition in some way, then it doesn't succeed as a definition, since if we say that every point is accessible, then it also satisfies your definition, even if the order is not at all well-founded by the usual meaning of that term. $\endgroup$
    – Joel David Hamkins
    Nov 29, 2012 at 23:34
  • 1
    $\begingroup$ Regarding your edit, the proof of accessibility might not be a finite tree. First, it may not be a tree at all, but second, it might not be finite even when it is a tree, since there are infinite well-founded trees. The well-founded rank of a node can be essentially any ordinal. $\endgroup$
    – Joel David Hamkins
    Nov 29, 2012 at 23:52
  • $\begingroup$ Joel, thank you for your correction. I made an edit above clarifying that. Indeed, Accessibility is defined in Agda or Coq as an inductive datatype where the "smallest relation" restriction is implied. $\endgroup$
    – Michael Maloney
    Nov 29, 2012 at 23:56
  • 1
    $\begingroup$ Since $=$ is reflexive, I would say that the well-founded part is empty, so it is ill-founded. The least fixed of your process is the empty relation. $\endgroup$
    – Joel David Hamkins
    Nov 30, 2012 at 0:06

1 Answer 1

Reset to default
2
$\begingroup$

It seems to me that you are looking for fixed point logic, with many articles available there. See also fixed-point combinators.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I'm not sure the Wikipedia article is relevant. The recursive functions I'm interested are provably total, whereas the fixpoint combinator is the fastest way to define partial functions :) I can't make heads or tails of any of the search results for fixed point logic. I know the notion of a fixed point is relevant here, though. Induction corresponds to folds on types defined with the least fixedpoint operator. Sim for co-induction/greatest fixedpoints. (From homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/…) But I can't make the connection to my problem. $\endgroup$
    – Michael Maloney
    Nov 30, 2012 at 0:14

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.