[Agda] Termination checker correctness proof

[Jesper Cockx]

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
termination<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker>,
there is the following definition of the termination order:


   1. Constructor elimination: if cons is a constructor, x < cons a1..an x
   b1..bn,
   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
Bad<http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell>
.

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,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130507/58074063/attachment.html