Agda in Agda [Was: [Agda] Pie in the sky]

[Samuel Gélineau]

On 2010-09-25 at 1:52 AM, Benja Fallenstein wrote:
> On Sat, Sep 25, 2010 at 7:22 AM, Samuel Gélineau wrote:
>> [...] Somebody should write a
>> provably-terminating Agda compiler in Agda; this would make it much
>> easier to ensure that further language extensions preserve
>> termination.
>
> Yes, but since an Agda type checker needs to normalize arbitrary Agda
> code, this isn't *trivial* (there's some potentially relevant work by
> Turing, Gödel and Tarski) :-)

Turing? Since the termination checker is conservative, I don't see how
the halting problem is an obstacle here.

Gödel's second incompleteness theorem? I just want a _terminating_
Agda compiler, not an Agda proof that such a compiler will only accept
programs which prove true theorems.


Let me expand on this. Agda needs a termination checker because it
needs to evaluate parts of the program at compile-time, and it needs
to be sure that those evaluations will terminate in order to ensure
that compilation itself will terminate. So an Agda compiler written in
Agda would need a predicate (Terminates : Program -> Set) to represent
the fact that a program has passed its termination checker, and it
would also need a function (eval : (p : Program) -> Terminates p ->
Program) which passes said termination checker.

Now for simplicity, assume (Terminates p) is just an integer n
bounding the number of steps which the termination checker thinks it
would take for p to be evaluated. Given this, eval could simply
decrement this bound each time it recurs, and return a phony value
once it reaches zero. If the termination checker guesses some bounds
incorrectly, the compiler will start reporting type errors when two
expressions should have the same normal form, but the compiler will
still provably terminate. We don't need a provably-correct Agda
compiler written in Agda; we only need a provably-terminating Agda
compiler written in Agda.


Besides, it is mainly the Agda extensions which I wanted to write in
Agda, to make sure they don't mess up termination. It would be
perfectly fine for large parts of the plain
compiler-without-extensions to be postulated or hidden through FFI.

– Samuel