## “General Recursion using Coinductive Monad” Got Right

Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.

Skip to content
# Termination

## “General Recursion using Coinductive Monad” Got Right

## General Recursion using Coindutive Monad

## Well-Foundedness and Reductivity

## Well-Founded Recursion and Accessibility

## Terminating Unfolds (2)

## Terminating Unfolds (1)

Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.

It would be nice to if we could write the program and prove its termination separately. Adam Megacz published an interesting paper: A Coinductive Monad for Prop-Bounded Recursion. As a practice, I tried to port his code to Agda.

It seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness.

Given a relation

After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. Secondly, to define `unfoldT↓`

using *well-founded recursion*.

I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.