[Agda] Fixpoint in Agda

[Jannis Limperg]

> I am particularly interested in computing the least fixpoint via Ascending Chain Condition (ACC),
> for the purpose of verified program analysis.

The standard technique for encoding non-structural fixpoints in type
theory uses a descending chains condition: You'll define a well-founded
ordering (that is, a relation < such that there is no infinite
descending chain x1 > x2 > ...) and prove your functions decreasing on
that ordering <. This is formalised in Agda's standard library,
specifically Induction.WellFounded [1].

Unfortunately, it's a little hard to see what's going on there due to
some of the abstractions used. If you can read Coq, you can take a look
at its version [2], which is more direct but otherwise works exactly the
same way. Searching for 'well-founded induction/recursion' will point
you towards more resources.

Cheers,
Jannis


[1]
https://github.com/agda/agda-stdlib/blob/master/src/Induction/WellFounded.agda

[2] https://coq.inria.fr/library/Coq.Init.Wf.html