User michael maloney - MathOverflow

Is there research on the notion of co-accessibility?

2012-11-29T23:09:42Z

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!

Comment by Michael Maloney

2012-11-30T00:20:57Z

Ah, yes. You are correct there. NO set is well-founded under equality. It's a true fact, but not a very interesting one. A practical application is illustrated here to prove the totality of a naively-defined quicksort function (code.galois.com/talk/2010/10-06-mertens.pdf) The relation < used in the paper is sublist-of rather than the "default" notion of tail-of when doing structural induction.

Comment by Michael Maloney

2012-11-30T00:14:43Z

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/…) But I can't make the connection to my problem.

Comment by Michael Maloney

2012-11-29T23:59:18Z

Brian, I made an edit clarifying the base case. The only base case is the vacuous base case: when there are no y such that y < x, then x is accessible under <. You also highlighted an important distinction I missed, Brian. Indeed, every set X is well-founded under equality. This differs from the usual notion of well-founded in mathematics. However, this is the notion I'm interested in. The fact every set is well-founded under equality is not useful. I think you can recover the usual notion with additional limitations on the relation, but I'm not interested in doing so.

Comment by Michael Maloney

2012-11-29T23:56:37Z

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.