[Agda] Theoretical limits of termination checking (reference request)

[Kirill Elagin]

On Thu, Sep 4, 2014 at 6:06 PM, Frédéric Blanqui <frederic.blanqui at inria.fr>
wrote:

>  Hi.
>
> You may be interested in the works of Bellantoni, Marion, Avanzini &
> Moser, ... See for instance
> - http://dx.doi.org/10.2168/LMCS-9(4:9)2013
> - http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123
> to cite just very few papers on this topic.
>

Thank you for the references. Looks like those articles together propose,
well, let’s say a programming language, that encodes only functions running
in exponential time.
It seems to me that this is not particularly interesting just because there
are pretty simple typesystems that guarantee that only terminating programs
will typecheck and, furthermore, that all the primitive recursive functions
can be typed (see e.g. “Termination Checking with Types
<http://www2.tcs.ifi.lmu.de/~abel/publications.html#rairo04>”). Together
with the widely known fact that a function is PR iff its running time is
bounded by a PR function this means that this typesystem types all the
exponential time functions and many others.
So those works are probably interesting from the term-rewriting point of
view but bring nothing new into our world of checking termination by typing.

Please, correct me if I missed something!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141011/6a40a1bc/attachment.html