Is there research on the notion of co-accessibility? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T11:44:08Z http://mathoverflow.net/feeds/question/114939 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/114939/is-there-research-on-the-notion-of-co-accessibility Is there research on the notion of co-accessibility? Michael Maloney 2012-11-29T23:09:42Z 2012-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 &lt; be a binary relation on X (though the use of &lt; 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 &lt; iff for every element y in X such that y &lt; x, y is also accessible under &lt;. Intuitively, starting at x, all chains x_n &lt; ... &lt; x_1 &lt; 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 &lt; x, then x is accessible under &lt;).</p> <p>We say X is well-founded under &lt; iff every element x in X is accessible under &lt;.</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 &lt; (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#114940 Answer by Joel David Hamkins for Is there research on the notion of co-accessibility? Joel David Hamkins 2012-11-29T23:46:58Z 2012-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&amp;tbo=d&amp;output=search&amp;sclient=psy-ab&amp;q=fixed+point+logic&amp;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>