[Agda] Fwd: Programming with well-founded/sized recursion

[Patricia Peratto]

My paper

Well-founded relations in Type Theory 

published in

Logic Journal of the IGPL
Volume 5, Issue 6, November 1997
Pages 811-852

defines different well-founded relations
in Martin-Lof's type theory. 
Implements them in Alf.

I hope it helps.

Patricia.

----- Mensaje original -----
De: "Xuanrui Qi" <xqi01 at cs.tufts.edu>
Para: agda at lists.chalmers.se
Enviados: Lunes, 17 de Junio 2019 5:20:28
Asunto: [Agda] Programming with well-founded/sized recursion

Hello,

One of my current Agda developments involve some kind of well-
founded/measure-based recursion. The original development was in Coq,
where I used measure-based termination. Now, as I transcribe my code to
Agda, what should I use to prove termination to the termination checker
?

The data structure I am operating on is a tree, and the termination
proof is just by induction on size. Sized types seem like a good choice
for what I want, but it's hard to find resources to get me started. Are
there any pointers or examples (besides the manual)? Alternatively, are
there combinators that can help me define this kind of recursion using
accessibility predicates?

Which would be the preferred solution if I want to compile my code
eventually?

Thanks,
Xuanrui

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda