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

[Benja Fallenstein]

Hi Samuel,

On Sat, Sep 25, 2010 at 6:52 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> Of course I want my Agda proof of termination to reflect the informal
> argument.

Ok :-)

> I accept your argument. Alas! it appears Agda cannot be implemented in
> Agda. For the benefit of those who, like me, remember that the devil
> is in the details, let me flesh out your proof in order to make its
> conclusion inescapable.

Thanks!

One small note on the formalization: IIRC, most diagonalization proofs
I've seen have been formally a bit different, like:

> f : Program -> Bool
> f p with termination-checks? p
> f p | (no _) = ff
> f p | (yes t) with eval p t
> f p | (yes t) | r with syntactically-equal? r (quote tt)
> f p | (yes t) | r | (yes _) = ff
> f p | (yes t) | r | (no _) = tt

Then you can use a lemma that for any type X and function f : Program
-> X, you can construct an expression q : X such that q is beta-equal
to (f the-source-of-q). -- In the case of the halting problem,
Kleene's second recursion theorem is the equivalent of this lemma; in
Gödel's incompleteness theorem and Tarski's theorem that no language
can define its own truth predicate, it's the diagonal lemma. It's a
small thing, but it's a nice way to formulate the lemma so that you
can prove it independently and then apply it in the diagonalization
proof.

Note, again, that there is no similar objection to having a hierarchy
of total languages, each of which can evaluate the one below. Of
course, we do not want to write an infinite number of compilers (where
each one can compile the next one), but hopefully there is *some*
sensible way of making this parametric -- the moral equivalent to how
we cannot write an identity function in a predicative language that we
can apply to itself, but we can write

id : {l : Level} -> {X : Set l} -> X -> X
id x = x

id' : {l : Level} -> {X : Set l} -> X -> X
id' = id id

My speculation about an interpreter that takes some kind of large
universe axiom (e.g., a universe à la Tarski and its decoding
function) in my previous mail is my current favored way of trying to
do this, though I've also pondered using the universe hierarchy; with
Agda's ability to compute with Level, perhaps we can write a function
that takes a level l and returns an interpreter which lives at level
(suc l) and can interpret code that makes use of no more than l
levels.

All that is very speculative, though; in terms of concrete
achievements, I'm still stuck trying to write an interpreter for a
plain core dependent type theory that is written in full Agda with
induction-recursion and everything, clearly a much stronger language.

Thanks again,
- Benja