[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
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
More information about the Agda
mailing list