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

[Benja Fallenstein]

On Sat, Sep 25, 2010 at 5:19 PM, Benja Fallenstein
<benja.fallenstein at gmail.com> wrote:
> 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...

Sorry, that came out wrong, strike that!

You can write that quine if the countdown cutoff is set large enough,
of course. What happens is that the self-interpreter is not actually a
full self-interpreter: it can't interpret programs to the same cutoff
number of steps as its environment, because its own cutoff runs out
before that.

I see that this would not necessarily be an obstacle for writing an
Agda *compiler* in Agda, as opposed to an interpreter -- it only needs
to perform the necessary normalizations for type-checking itself
during compilation, it doesn't need to interpret itself interpreting
another program.

- Benja