日々の流転

λ. Categorical Semantics of Linear Logic For All by Valeria de Paiva

線形論理の圏論的なモデルに関して良くまとまっている。 また、論理の圏論的なモデルがどういうものかを知るにも良いと思う。

良く分からなかった部分

• 「categorical duality will produce a model of classical linear logic from one of intuitionistic linear logic, automatically.」という部分。
• DILL category に関する話での「Function spaces in the cartesian category can be induced from the linear ones.」の部分。
  • Andrew Graham Barber の Linear Type Theories, Semantics and Action Calculi や Dual Intuitionistic Linear Logic あたりを読めばよいのだろうけど……
• セオリーの圏に関係する部分。

λ. 米田の補題と多相ラムダ計算

米田の補題の話をしていたので、多相ラムダ計算で対応するものを示してみる。

任意の F:*→* と C:* とが与えられていて、mapF: ∀X:*, Y:*. (X→Y)→(F X → F Y) が関手の条件を満たすとする。(∀X:*. (X → C) → F X) ≅ F C を示す。

id : ∀X:*. X→X
id = (ΛX:*. λx:X. x)

Φ : (∀X:*. (C→X) → F X) → F C
Φ = λα:(∀X:*. (C→X) → F X). α C (id C)

Ψ : F C → (∀X:*. (C→X) → F X)
Ψ = λx:F C. ΛX:*. λf:C→X. mapF C X f x

λα:(∀X:*. (C→X) → F X). Ψ (Φ α)
= {- β reduction -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. mapF C X f (α C (id C)) 
= {- parametricity -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. α X (λc:C. f (id C c)
= {- β reduction and η conversion -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. α X f
= {- η conversion -}
  id (∀X:*. (C→X) → F X)

λx:F C. Φ (Ψ x)
= {- β reduction -}
  λx:F C. mapF C C (id C) x
= {- functor law -}
  λx:F C. id (F C) x
= {- η conversion -}
  id (F C)