§ 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 σ → τ.
  1. u ⊩ ℕ if u reduces to a natural number literal
  2. 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