[Agda] Programming with well-founded/sized recursion

[Filippo Sestini]

Hi,

I believe the closest Agda equivalent to Coq’s measure-based
termination is well-founded induction. You can find the machinery
for it in the standard library [1].

However, I agree that in your case sized types could be
a better option. There’s a worked out example in the docs
that might help you get started [2].

[1] https://github.com/agda/agda-stdlib/blob/master/src/Induction/WellFounded.agda
[2] https://agda.readthedocs.io/en/v2.6.0.1/language/sized-types.html

Cheers
-- 
Filippo Sestini
http://www.cs.nott.ac.uk/~psxfs5/

> On Jun 17, 2019, at 9:20 AM, Xuanrui Qi <xqi01 at cs.tufts.edu> wrote:
> 
> 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




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.