(Logical Relation) W logical relation of arity W R = (R_{σ} ∈ (D_{σ}^{W}) | σ ∈)

f ∈ R_{στ} ⇔ ∀d∈R_{σ}. \underline{λ}i∈W.f(i)(d(i)) ∈ R_{τ} ⇔ ∀d∈R_{σ}. ∘fd ∈ R_{τ}

σ τ R W R all P ⊆ D^{W}

R W R_{=}P

(Main Lemma for Logical Relations)

R W λ x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢

M : τ d_{j} ∈

R_{σ_{j}} j=1, .., n \underline{λ}i∈W. x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M(d⃗(i)) ∈ R_{τ}

d⃗(i) = ⟨d_{1}(i), …, d_{n}(i)⟩

i ∈ W Γ ⊢ M : σ λ M Γ, x:σ ⊢

M : τ Γ ≡ x_{1}:σ_{1}, …, x_{n}:σ_{n}

d_{j} ∈ R_{σ_{j}} j=1, …, n \underline{λ}i∈W. Γ ⊢ λx:σ.M(d⃗(i)) ∈ R_{στ} .

d ∈ R_{σ}

\underline{λ}i∈W. Γ ⊢ λx:σ.M(d⃗(i))(d(i)) = \underline{λ}i∈W. Γ, x:σ ⊢ M(⟨d⃗(i), d(i)⟩)

R_{τ} Γ ⊢ M : στ Γ ⊢ N : σ d_{j} ∈

R_{σ_{j}} j=1, …, n \underline{λ}i∈W. Γ ⊢ M(N)(d⃗(i)) ∈ R_{τ} .

Γ ⊢ M(N)(d⃗(i)) = Γ ⊢ M(d⃗(i))(Γ ⊢ N(d⃗(i))) \underline{λ}i∈W. Γ ⊢ M(d⃗(i))(Γ ⊢ N(d⃗(i))) ∈ R_{τ}

R_{στ} \underline{λ}i∈W. Γ ⊢ M(d⃗(i)) ∈ R_{στ}

\underline{λ}i∈W. Γ ⊢ N(d⃗(i)) ∈ R_{σ}

M N λ R W M λ σ \underline{λ}i∈W. M ∈

R_{σ} ?? R W d ∈ D_{σ} R– invariant δ_{W} (d) := \underline{λ}i∈W.d ∈ R_{σ} ?? the denotation of a closed λ– term is Rinvariant for