[Agda] Normalization by Evaluation

[Brandon Moore]

Hello

I've been working through Peter Dybjer's slides on normalization by evaluation, and 

I had some trouble with the proof for typed combinators (around slide 70)

http://www.cse.chalmers.se/~peterd/slides/Leicester.pdf

To have an argument to recurse on in the semantics for rec it seems I
have to change ⟦ Nat ⟧ from Exp Nat to ℕ, otherwise I don't know how
to handle the case when the expression in the third argument
has the form of an application (which isn't actually possible in a normal
form of type Nat).

The proof that e ~ nbe e was difficult. To get the proof to go through
I added an auxiliary judgement saying that some domain value ⟦ t ⟧
represented an expression, which seems to be adding back the
proof content which was left out in the first place when writing the
evaluator.

The difficulty in both cases seem to be that  ⟦ t ⟧ allows bad terms
even if the evaluator will not produce them. I tried a few ways to
rewrite the proofs to only talk about values in ⟦ t ⟧ produced by
the evaluator, but I didn't find a version that worked for the values
produced by applying the ⟦ a ⟧ -> ⟦ b ⟧ inside a ⟦ a ⇒ b ⟧.
Is there a better way to go about these proofs?

Brandon.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: combinators.agda
Type: application/octet-stream
Size: 7107 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111123/0a9a91b5/combinators.obj