3 deleted 5 characters in body

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 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!

2 added 332 characters in body

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 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!

1

# Is there research on the notion of co-accessibility?

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.

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 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!