Is there research on the notion of co-accessibility? - MathOverflow most recent 30 from http://mathoverflow.net2013-05-19T11:44:08Zhttp://mathoverflow.net/feeds/question/114939http://www.creativecommons.org/licenses/by-nc/2.5/rdfhttp://mathoverflow.net/questions/114939/is-there-research-on-the-notion-of-co-accessibilityIs there research on the notion of co-accessibility?Michael Maloney2012-11-29T23:09:42Z2012-11-29T23:56:01Z
<p>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 :)</p>
<p>Let's start off with some context. </p>
<p>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).</p>
<p>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. </p>
<p>(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.)</p>
<p>(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 <).</p>
<p>We say X is well-founded under < iff every element x in X is accessible under <.</p>
<p>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). </p>
<p>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).</p>
<p>I already know how to do this for recursion. </p>
<p><strong>My problem is that I don't know how to do this for co-recursion.</strong></p>
<p>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.</p>
<p>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!</p>
http://mathoverflow.net/questions/114939/is-there-research-on-the-notion-of-co-accessibility/114940#114940Answer by Joel David Hamkins for Is there research on the notion of co-accessibility?Joel David Hamkins2012-11-29T23:46:58Z2012-11-29T23:46:58Z<p>It seems to me that you are looking for <a href="http://www.google.com/?oq=fixed+point+logic#hl=en&tbo=d&output=search&sclient=psy-ab&q=fixed+point+logic&oq=fixed+point+logic" rel="nofollow">fixed point logic</a>, with many articles available there. See also <a href="http://en.wikipedia.org/wiki/Fixed-point_combinator" rel="nofollow">fixed-point combinators</a>. </p>