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

[Samuel Gélineau]

On 2010-09-25 at 11:19 AM, Benja Fallenstein wrote:
> On Sat, Sep 25, 2010 at 4:37 PM, Samuel Gélineau wrote:
>> 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. [...]
>
> Ok, if that is the only termination guarantee you want from your
> extensions, then you can certainly do it this way [...].
> 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.

Of course I want my Agda proof of termination to reflect the informal
argument. I wanted to show that having a provably-terminating but not
necessarily provably-correct compiler did not immediately lead to a
contradiction, and I used integers because they're simpler to reason
about. I did not expect that using a more realistic termination
predicate would make it easier to arrive at a contradiction, but you
showed otherwise:

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

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.


Let Program be an Agda representation of a piece of Agda code, say, a
string. Let (quote p) be an informal notation for the Program
representing p; this is not an Agda function, but something outside
the system. An implementation of Agda written in Agda would certainly
need terminating implementations of the following functions:

-- decides whether p passes the termination checker, not whether p terminates
termination-checks? : (p : Program) -> Dec (Terminates p)

syntactically-equal? : (p q : Program) -> Dec (p == q)

eval : (p : Program) -> Terminating p -> Program


But given these functions, the following counter-example can be constructed:

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


Since termination-checks?, eval and syntactically-equal? are all
assumed to pass the termination checker, the current Agda termination
checker would also accept p as terminating. Therefore, if
termination-checks?, eval and syntactically-equal? are all correct
(but not necessarily proved to be correct using Agda), p will return
ff if and only if it returns tt, a contradiction.


– Samuel, disappointed again