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!