§ Realisability models
For closed terms u, and type 𝜏 we are going to define u ⊩ 𝜏 (read “u is a
realiser of 𝜏”). Let's say that we have PCF's type: ℕ and σ → τ.
-
u ⊩ ℕ if u reduces to a natural number literal -
f ⊩ σ → τ if for all s⊩σ, f s ⊩ τ.
Some immediate observations:
- This definition is by induction on the types, and assumes little from the terms (it's a logical relation).
- This is “really what we mean” by
x : 𝜏 (except non-termination, not modelled here): realisability has explanatory power. - This relation is usually undecidable.
- It is strongly related to parametricity (in parametricity we associate a binary relation to types, in realisability we associate a (unary) predicate). 4/10
- From this point of view, typing is a (usually decidable) modular approximation of realisability.
- For instance, consider
if x then 1 else (\y -> y). It isn't well-typed. - However, if we add
let x = True in if x then 1 else (λy. y) it becomes a realiser of ℕ [because upon reduction, it produces an N, even though it is not "well-typed".
- Typing and realisability are related by a lemma sometimes referred as adequacy.
Take the rule for λ (simplified):
x:X, y:Y ⊢ z : Z
-----------------------
x:X ⊢ λ(y: Y). z : Y → Z
You interpret it as a statement
∀ v⊩A, (∀ w ⊩ B, u[x\v, y\w] ⊩ C) ⟹ \lambda y.u[x\v] ⊩ C
- Then, you prove this statement. 7/10
Once you've done so for each rule, you can conclude (very easy induction) that
if ⊢ u : A, then u ⊩ A. This gives type safety, since realisers are practically
defined as verifying type safety.
What you've gained along the way is that this proof is an open induction. 8/10
In standard combinatorial proofs of type safety, the induction hypothesis may
depend on every case. Adding a form in your language may require redoing the
entire proof. Here the various case in the adequacy lemma will remain true. So
you can just prove the new cases. 9/10
There are many variants of realisability. Tuned for logic, with models instead
of terms, … My favourite is Krivine's realisability with both terms and stacks,
and magic happening when they interact. But this is another story and shall be
told another time. 10/10