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

[Benja Fallenstein]

Hi,

On Sat, Sep 25, 2010 at 4:37 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> 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) :-)

(replying out of order:)

> 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.

Ok, if that is the only termination guarantee you want from your
extensions, then you can certainly do it this way, and I suppose doing
it in Agda would give a little more assurance that you got all your
t's dotted than doing the same trick in Haskell. When you brought this
up in the context of replacing discussion about whether a proposed
language extension is terminating, I did think you meant the
implementation should be in effect a formalization of the informal
arguments why the extension terminates, not just force termination
through a time-out.

I admit that this is probably colored by the fact that I *do* want a
provably-correct compiler...

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

It's true that a termination checker doesn't need to solve the halting
problem in order to recognize itself as terminating. What I had in
mind is that a total language that is closed under enough operations
to allow you to write quines, or you could write the program "p =
normalize p and if its normal form is tt, return ff, otherwise return
tt." Counting down gets around that by not having such closure
properties... it's just that I don't find that fact all that
interesting, since I can already 'sleep 3600; killall ghc'...

> 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.

Yes, incompleteness is probably less relevant given what you seem to want.

> 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.

Ok, that makes sense, if you can separate the implementation of the
extensions from the implementation of the compiler so that the
termination of the former becomes clear, and if Agda is a strong
enough language for implementing interesting extensions in a
provably-terminating way.

- Benja