[Agda] Normalization by Evaluation

[Peter Dybjer]

Dear Brandon,

One way to do the proof can be found in section 2.5 of

http://www.cse.chalmers.se/~peterd/papers/Glueing.pdf

The key idea is to define a family of predicates "Gl_A" by induction on types A, which carves out the good values in the semantics.

Peter
________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Brandon Moore [brandon_m_moore at yahoo.com]
Sent: Wednesday, November 23, 2011 11:02 AM
To: agda at lists.chalmers.se
Subject: [Agda] Normalization by Evaluation

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.