[Agda] Termination checker correctness proof

Jesper Cockx Jesper at sikanda.be
Tue May 7 14:04:29 CEST 2013

Dear Agda mailing list,

I'm currently writing my master thesis on pattern matching with dependent
types, and I have a question about the termination checker in Agda.

On the wiki page on
there is the following definition of the termination order:

   1. Constructor elimination: if cons is a constructor, x < cons a1..an x
   2. Application: if y<x then (ya)<x where a is a vector of terms.

but I can't find a proof why this termination order is correct, i.e. why it
is well-founded. Specifically rule 2 seems suspicious because evaluating ya
could give something that's not smaller than x.

A proof would certainly need the fact that data types are strictly
positive, otherwise we get non-termination problems like the type

One way to argue correctness of the termination checker would be that
pattern matching can be translated to a case tree, which can be translated
to eliminators, which are terminating by some type theoretic metatheory.
But I would like to have a more direct proof that doesn't use the
equivalence with case trees.

Can someone give me an argument or a reference which shows that this
termination order is well-founded? This would be much appreciated.

Best regards,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130507/58074063/attachment.html

More information about the Agda mailing list