Neat idea for realizability-based reflection

[jonsterling]

Currently, reflection works like this:

  ⊢ (M=N:A) ∈ H
-------------------[hint-projection]
  Γ;H ⊢ M=N:A

  Γ;(H, M=N:A) ⊢ C ⇐ U
  Γ;(H, M=N:A) ⊢ e ⇐ C
  Γ;H ⊢ p ⇐ Id(A; M; N)
-------------------------------[reflection-scope]
  Γ;H ⊢ reflect p in e ⇐ C

Imagine if we had something slightly different. What if the judgmental equality were precisely when propositional equality is trivial:

  Γ;H ⊢ ♦ ⇐ Id(A; M; N)
---------------------------------[trivial-reflection]
  Γ;H ⊢ M=N:A

And the propositional equality Id(A; M; N) is defined by recursion on types, endowing each type with its correct extensional equality. Note that ♦ is the trivial term (called “bullet” in Nuprl), which is synthesizes type 1, but may be checked with that or any true squashed proposition (such as equality).

And then, we would change the reflect construct to not be about equality, but rather to be about bringing the knowledge that a particular term is the computational realizer for another at a particular type into scope. That is, we have a realizability judgment which looks sort of like this: r ⊩ p : S which means that r is the realizer and p is the proof term for a proposition S. Note that the terms of Nuprl are realizers, not proof terms: the proof terms are terms in the logical framework, namely the equality derivations. In general, there is not enough information in realizers for them to be checked against types, but they can always of course be extracted from terms. The computational realizer for any equality is just ♦.

Therefore, the hints box should be reformulated to be a collection of known realizers, and reflect should introduce evidence about realizers into scope so that realizers may be used instead of proof terms. Behold:

  ⊢ (r ⊩ p : S) ∈ H
------------------------- [hint-projection]
  Γ;H ⊢ r ⇐ S

  Γ;(H, r ⊩ p : S) ⊢ C ⇐ U
  Γ;(H, r ⊩ p : S) ⊢ e ⇐ C
  Γ;H ⊢ r ⊩ p ⇐ S
-------------------------------[reflection-scope]
  Γ;H ⊢ reflect p in e ⇐ C

Then, the example we keep bringing up can be given as a special case.

Let P := Id(U; 0; 1).
Let J := ♦ ⊩ p : P.

  ⊢ J ∈ H,J
 -----------------------------------------[hint-proj]
  Γ,p:P; H,J ⊢ ♦ ⇐ P
 -----------------------------------------[triv-reflect]
  Γ,p:P; H,J ⊢ 0=1:U
 -----------------------------------------[1-intro, substitution]
  Γ,p:P; H,J ⊢ ♦ ⇐ 0
 -----------------------------------------[reflect-scope]
  Γ,p:P; H ⊢ reflect p in ♦ ⇐ 0
 -----------------------------------------[Π-intro]
  Γ;H ⊢ λ[p] reflect p in ♦ ⇐ Π[p:P] 0

The moral of this story I'm telling is that we're not building scoped equality reflection, we're building _scoped realizability_.

Comments? @darinmorrison @psygnisfive

[jonsterling]

A more orderly and better-explained version of this is given here: http://www.jonmsterling.com/posts/2014-06-30-a-type-theory-with-scoped-realizability.html

[jonsterling]

Superceded by #27