単純型理論のcanonicityの証明
2025-12-2
これは証明支援系 Advent Calendar 2025 2日目の記事です。
このページでは単純型理論のcanonicity、すなわちbool型の閉項がtrueかfalseであることを示します。
imports
open import Data.Unit using (⊤; tt) open import Data.Product using (_×_; proj₁; proj₂; _,′_) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Relation.Binary using (IsEquivalence; Setoid) import Relation.Binary.Reasoning.Setoid as Reasoning
構文
型と文脈
対象言語の型を定義します：
data Type : Set where bool : Type _=>_ : Type → Type → Type infixr 40 _=>_
data宣言ではAgdaにおける型を帰納的に定義することができます。ここではTypeという型を定義しており、その構成子はboolと_=>_の2種類があります。
Agdaでは識別子の一部に_を使うことで、中置演算子や前置演算子、後置演算子などを定義できます。なので、A : TypeかつB : Typeであれば、A => B : Typeとなります。ここでのinfixr宣言は_=>_が右結合の中置演算子であり、優先度が40であることを指定しています。
そして、文脈を定義します：
data Ctx : Set where nil : Ctx [_,_] : Ctx → Type → Ctx
private variable Γ Δ : Ctx A B C : Type
privateブロックは、そのスコープ内で定義された識別子がモジュール外からアクセスできないようにします。このvariableブロックでは、以下で自由に出現するΓとΔ、そしてAとBとCが定義ごとに暗黙に量化されることを意味します。
項と明示的代入
項と明示的代入を相互帰納的に定義します：
data Term : Ctx → Type → Set data Subst : Ctx → Ctx → Set data Term where Var : Term [ Γ , A ] A Abs : Term [ Γ , A ] B → Term Γ (A => B) App : Term Γ (A => B) → Term Γ A → Term Γ B true : Term Γ bool false : Term Γ bool case : Term Γ bool → Term Γ A → Term Γ A → Term Γ A _[_] : Term Γ A → Subst Δ Γ → Term Δ A infix 30 ⟨_,_⟩ data Subst where id : Subst Γ Γ _∘_ : ∀ {Γ₁ Γ₂ Γ₃} → Subst Γ₂ Γ₃ → Subst Γ₁ Γ₂ → Subst Γ₁ Γ₃ Weak : Subst [ Γ , A ] Γ ⟨_,_⟩ : Subst Δ Γ → Term Δ A → Subst Δ [ Γ , A ]
最も直近で束縛された変数は以下のようにVarで表されます：
_ : Term [ Γ , A ] A _ = Var
そして、その1つ外側で束縛された変数は以下のようにWeakを使って表現します：
_ : Term [ [ Γ , A ] , B ] A _ = Var [ Weak ]
Weakの数を増やすことでより外側で束縛された変数を表せます：
_ : Term [ [ [ Γ , A ] , B ] , C ] A _ = Var [ Weak ∘ Weak ]
次に、項と明示的代入それぞれに対し、判断レベルの等価性を定義します：
data _≡T_ : Term Γ A → Term Γ A → Set data _≡S_ : Subst Γ Δ → Subst Γ Δ → Set infix 10 _≡T_ _≡S_ data _≡T_ where Var-ext : ∀ {σ : Subst Δ Γ} {M : Term Δ A} → Var [ ⟨ σ , M ⟩ ] ≡T M
Var-extはVarがσとMの組から第一要素を取り出す射影であることを主張しています。
id-nop : ∀ {M : Term Γ A} → M [ id ] ≡T M ∘-succ : ∀ {Γ₁ Γ₂ Γ₃ A} {M : Term Γ₃ A} {σ : Subst Γ₁ Γ₂} {τ : Subst Γ₂ Γ₃} → M [ τ ∘ σ ] ≡T M [ τ ] [ σ ]
id-nopは「idを作用させても項は何も変わらない」こと、∘-succは「代入を合成してから作用することは順番に作用させることと同じである」ことを言っています。
=>β : ∀ {M : Term [ Γ , A ] B} {N : Term Γ A} → App (Abs M) N ≡T M [ ⟨ id , N ⟩ ] =>η : ∀ {M : Term Γ (A => B)} → Abs (App (M [ Weak ]) Var) ≡T M
=>βと=>ηは関数型についてのβ規則とη規則をそれぞれ表しています。
boolβ₁ : ∀ {M N : Term Γ A} → case true M N ≡T M boolβ₂ : ∀ {M N : Term Γ A} → case false M N ≡T N
boolβ₁とboolβ₂はbool型についてのβ規則を表しています。
bool型がη規則を持たないということは、集合モデルにおいてboolは2点集合以外の集合で解釈される可能性があります。3点集合や無限集合などで解釈される可能性がある以上、canonicityは一般のモデルでは成り立ちません。したがってcanonicityは構文に対しての定理となります。
≡Tが同値関係となるように以下を追加します：
refl-≡T : ∀ {M : Term Γ A} → M ≡T M sym-≡T : ∀ {M N : Term Γ A} → M ≡T N → N ≡T M trans-≡T : ∀ {M N P : Term Γ A} → M ≡T N → N ≡T P → M ≡T P
さらに合同関係にします：
cong-App₁ : ∀ {M M′ : Term Γ (A => B)} {N : Term Γ A} → M ≡T M′ → App M N ≡T App M′ N cong-App₂ : ∀ {M : Term Γ (A => B)} {N N′ : Term Γ A} → N ≡T N′ → App M N ≡T App M N′ cong-Abs : ∀ {M M′ : Term [ Γ , A ] B} → M ≡T M′ → Abs M ≡T Abs M′ cong-case : ∀ {M M′ : Term Γ bool} {N N′ P P′ : Term Γ A} → M ≡T M′ → N ≡T N′ → P ≡T P′ → case M N P ≡T case M′ N′ P′ cong-[]₁ : ∀ {M N : Term Γ A} {σ : Subst Δ Γ} → M ≡T N → M [ σ ] ≡T N [ σ ] cong-[]₂ : ∀ {M : Term Γ A} {σ τ : Subst Δ Γ} → σ ≡S τ → M [ σ ] ≡T M [ τ ]
そして各constructorが代入と交換することを要請します：
comm-Abs : ∀ {M : Term [ Γ , A ] B} {σ : Subst Δ Γ} → Abs M [ σ ] ≡T Abs (M [ ⟨ σ ∘ Weak , Var ⟩ ]) comm-App : ∀ {M : Term Γ (A => B)} {N : Term Γ A} {σ : Subst Δ Γ} → App M N [ σ ] ≡T App (M [ σ ]) (N [ σ ]) comm-true : ∀ {σ : Subst Δ Γ} → true [ σ ] ≡T true comm-false : ∀ {σ : Subst Δ Γ} → false [ σ ] ≡T false comm-case : ∀ {M : Term Γ bool} {N P : Term Γ A} {σ : Subst Δ Γ} → case M N P [ σ ] ≡T case (M [ σ ]) (N [ σ ]) (P [ σ ])
以上の定義より、≡Tは意図通り同値関係となります：
≡T-isEquivalence : ∀ Γ A → IsEquivalence {A = Term Γ A} _≡T_ ≡T-isEquivalence _ _ = record { refl = refl-≡T ; sym = sym-≡T ; trans = trans-≡T }
（Agdaの）型と同値関係の組をsetoidと呼びます：
TermSetoid : ∀ Γ A → Setoid _ _ TermSetoid Γ A = record { Carrier = Term Γ A ; _≈_ = _≡T_ ; isEquivalence = ≡T-isEquivalence Γ A }
data _≡S_ where Weak-ext : ∀ {σ : Subst Δ Γ} {M : Term Δ A} → Weak ∘ ⟨ σ , M ⟩ ≡S σ
Weak-extはWeakがσとMの組から第二要素を取り出す射影であることを主張しています。
∘-lunit : ∀ {σ : Subst Δ Γ} → id ∘ σ ≡S σ ∘-runit : ∀ {σ : Subst Δ Γ} → σ ∘ id ≡S σ
∘-lunitと∘-runitはidが合成の単位元であることを表しています。
∘-assoc : ∀ {Γ₁ Γ₂ Γ₃ Γ₄} {σ : Subst Γ₁ Γ₂} {τ : Subst Γ₂ Γ₃} {θ : Subst Γ₃ Γ₄} → (θ ∘ τ) ∘ σ ≡S θ ∘ (τ ∘ σ)
∘-assocは合成が結合的であることを表しています。
ext-Weak-Var : ∀ {σ : Subst Δ [ Γ , A ]} → ⟨ Weak ∘ σ , Var [ σ ] ⟩ ≡S σ
ext-Weak-Varは[ Γ , A ]への代入σはWeak ∘ σとVar [ σ ]によって一意に決定されることを表しています。
refl-≡S : ∀ {σ : Subst Δ Γ} → σ ≡S σ sym-≡S : ∀ {σ τ : Subst Δ Γ} → σ ≡S τ → τ ≡S σ trans-≡S : ∀ {σ τ θ : Subst Δ Γ} → σ ≡S τ → τ ≡S θ → σ ≡S θ cong-∘₁ : ∀ {Γ₁ Γ₂ Γ₃} {σ : Subst Γ₁ Γ₂} {τ τ′ : Subst Γ₂ Γ₃} → τ ≡S τ′ → τ ∘ σ ≡S τ′ ∘ σ cong-∘₂ : ∀ {Γ₁ Γ₂ Γ₃} {σ σ′ : Subst Γ₁ Γ₂} {τ : Subst Γ₂ Γ₃} → σ ≡S σ′ → τ ∘ σ ≡S τ ∘ σ′ cong-⟨⟩ : ∀ {σ τ : Subst Δ Γ} {M N : Term Δ A} → σ ≡S τ → M ≡T N → ⟨ σ , M ⟩ ≡S ⟨ τ , N ⟩
≡Tと同様に≡Sも同値関係となります：
≡S-isEquivalence : ∀ Γ Δ → IsEquivalence {A = Subst Γ Δ} _≡S_ ≡S-isEquivalence _ _ = record { refl = refl-≡S ; sym = sym-≡S ; trans = trans-≡S }
SubstSetoid : ∀ Γ Δ → Setoid _ _ SubstSetoid Γ Δ = record { Carrier = Subst Γ Δ ; _≈_ = _≡S_ ; isEquivalence = ≡S-isEquivalence Γ Δ }
[ Γ , A ]への代入の等価性を示すための補題を与えます：
[,]-≡S : ∀ {σ τ : Subst Δ [ Γ , A ]} → Weak ∘ σ ≡S Weak ∘ τ → Var [ σ ] ≡T Var [ τ ] → σ ≡S τ [,]-≡S {σ = σ} {τ = τ} e₁ e₂ = begin σ ≈⟨ ext-Weak-Var ⟨ ⟨ Weak ∘ σ , Var [ σ ] ⟩ ≈⟨ cong-⟨⟩ e₁ e₂ ⟩ ⟨ Weak ∘ τ , Var [ τ ] ⟩ ≈⟨ ext-Weak-Var ⟩ τ ∎ where open Reasoning (SubstSetoid _ _)
Reasoningモジュールが提供するbegin ... ≈⟨ ... ⟩ ... ∎といった構文を使うことで、同値関係についての証明を読みやすくできます。おおまかには、x ≈⟨ e ⟩ yは「xとyは等しく、その証明はeによって与えられる」ことを意味し、≈⟨ ... ⟨は対称律の使用を意味します。
上記における{σ = σ}や{τ = τ}の様な記法は、暗黙に束縛される変数に言及するために使われています。
述語
型
型Aを持つ閉項に対する述語[| A |]を定義します。
[|_|] : (A : Type) → Term nil A → Set [| bool |] M = (M ≡T true) ⊎ (M ≡T false)
これはbool型の閉項はtrueかfalseであるという述語です。
[| A => B |] M = ∀ (N : Term nil A) → [| A |] N → [| B |] (App M N)
関数型A => Bの閉項Mは、A型の閉項Nが述語[| A |]を満たすならばApp M Nが述語[| B |]を必ず満たす、という述語です。
[| A |]が項の等価性に対して安定していることを、Aについての帰納法で示します：
stable : ∀ {A M N} → [| A |] M → M ≡T N → [| A |] N stable {A = bool} (inj₁ x) e = inj₁ (trans-≡T (sym-≡T e) x) stable {A = bool} (inj₂ y) e = inj₂ (trans-≡T (sym-≡T e) y) stable {A = A => B} p e N p′ = stable (p N p′) (cong-App₁ e)
文脈
[|_|]C : (Γ : Ctx) → Subst nil Γ → Set
文脈に対しても同様の述語を定義します。
[| nil |]C σ = ⊤ [| [ Γ , A ] |]C σ = [| Γ |]C (Weak ∘ σ) × [| A |] (Var [ σ ])
stable-C : ∀ {Γ σ τ} → [| Γ |]C σ → σ ≡S τ → [| Γ |]C τ stable-C {Γ = nil} p e = tt stable-C {Γ = [ _ , _ ]} p e = stable-C (proj₁ p) (cong-∘₂ e) ,′ stable (proj₂ p) (cong-[]₂ e)
主定理
項M : Term Γ Aは、σをM [ σ ]に写すことによって、Subst nil ΓからTerm nil Aへの（メタレベルの）関数と見なすことができます。我々が示したいのは、この関数が上記の述語をrespectすることです。
同様に、代入τ : Subst Γ Δはσをτ ∘ σに写すことによって、Subst nil ΓからSubst nil Δへの関数と見なすことができます。これもまた、上記の述語をrespectすることを示したいわけです。
この2つの主張をMとτについて相互帰納的に示します：
thm : (M : Term Γ A) → (σ : Subst nil Γ) → [| Γ |]C σ → [| A |] (M [ σ ]) thm-C : (τ : Subst Γ Δ) → (σ : Subst nil Γ) → [| Γ |]C σ → [| Δ |]C (τ ∘ σ)
項
MがVarであるとき、Γは[ Γ′ , A ]の形をしています。この形の文脈に対応する述語は積として定義されていたので、その証明の第二要素を取り出せばよいです：
thm Var σ p = proj₂ p
Abs Mの場合を考えます：
thm (Abs {B = B} M) σ p N p′ = stable ih (sym-≡T e) where
帰納法の仮定より、M [ ⟨ σ , N ⟩ ]が述語[| B |]を満たすことが分かります。
ih : [| B |] (M [ ⟨ σ , N ⟩ ]) ih = thm M ⟨ σ , N ⟩ ( stable-C p (sym-≡S Weak-ext) ,′ stable p′ (sym-≡T Var-ext) )
後は以下の等式を示せば十分です：
e₁ : Weak ∘ (⟨ σ ∘ Weak , Var ⟩ ∘ ⟨ id , N ⟩) ≡S Weak ∘ ⟨ σ , N ⟩ e₁ = begin Weak ∘ (⟨ σ ∘ Weak , Var ⟩ ∘ ⟨ id , N ⟩) ≈⟨ ∘-assoc ⟨ (Weak ∘ ⟨ σ ∘ Weak , Var ⟩) ∘ ⟨ id , N ⟩ ≈⟨ cong-∘₁ Weak-ext ⟩ (σ ∘ Weak) ∘ ⟨ id , N ⟩ ≈⟨ ∘-assoc ⟩ σ ∘ (Weak ∘ ⟨ id , N ⟩) ≈⟨ cong-∘₂ Weak-ext ⟩ σ ∘ id ≈⟨ ∘-runit ⟩ σ ≈⟨ Weak-ext ⟨ Weak ∘ ⟨ σ , N ⟩ ∎ where open Reasoning (SubstSetoid nil _) e₂ : Var [ ⟨ σ ∘ Weak , Var ⟩ ∘ ⟨ id , N ⟩ ] ≡T Var [ ⟨ σ , N ⟩ ] e₂ = begin Var [ ⟨ σ ∘ Weak , Var ⟩ ∘ ⟨ id , N ⟩ ] ≈⟨ ∘-succ ⟩ Var [ ⟨ σ ∘ Weak , Var ⟩ ] [ ⟨ id , N ⟩ ] ≈⟨ cong-[]₁ Var-ext ⟩ Var [ ⟨ id , N ⟩ ] ≈⟨ Var-ext ⟩ N ≈⟨ Var-ext ⟨ Var [ ⟨ σ , N ⟩ ] ∎ where open Reasoning (TermSetoid nil _) e : App (Abs M [ σ ]) N ≡T M [ ⟨ σ , N ⟩ ] e = begin App (Abs M [ σ ]) N ≈⟨ cong-App₁ comm-Abs ⟩ App (Abs (M [ ⟨ σ ∘ Weak , Var ⟩ ])) N ≈⟨ =>β ⟩ M [ ⟨ σ ∘ Weak , Var ⟩ ] [ ⟨ id , N ⟩ ] ≈⟨ ∘-succ ⟨ M [ ⟨ σ ∘ Weak , Var ⟩ ∘ ⟨ id , N ⟩ ] ≈⟨ cong-[]₂ ([,]-≡S e₁ e₂) ⟩ M [ ⟨ σ , N ⟩ ] ∎ where open Reasoning (TermSetoid nil B)
thm (App {A = A} {B = B} M N) σ p = stable u (sym-≡T comm-App) where ih : [| A => B |] (M [ σ ]) ih = thm M σ p u : [| B |] (App (M [ σ ]) (N [ σ ])) u = ih (N [ σ ]) (thm N σ p)
thm true σ p = inj₁ comm-true thm false σ p = inj₂ comm-false
caseについては、thm M σ pに対して場合分けを行います：
thm (case {A = A} M N P) σ p with thm M σ p
M [ σ ]がtrueと等しいときは以下のように示します：
... | inj₁ e = stable u (sym-≡T ( begin case M N P [ σ ] ≈⟨ comm-case ⟩ case (M [ σ ]) (N [ σ ]) (P [ σ ]) ≈⟨ cong-case e refl-≡T refl-≡T ⟩ case true (N [ σ ]) (P [ σ ]) ≈⟨ boolβ₁ ⟩ N [ σ ] ∎ )) where u : [| A |] (N [ σ ]) u = thm N σ p open Reasoning (TermSetoid nil A)
同様に、M [ σ ]がfalseと等しいときは以下のように示します：
... | inj₂ e = stable v (sym-≡T ( begin case M N P [ σ ] ≈⟨ comm-case ⟩ case (M [ σ ]) (N [ σ ]) (P [ σ ]) ≈⟨ cong-case e refl-≡T refl-≡T ⟩ case false (N [ σ ]) (P [ σ ]) ≈⟨ boolβ₂ ⟩ P [ σ ] ∎ )) where v : [| A |] (P [ σ ]) v = thm P σ p open Reasoning (TermSetoid nil A)
thm (M [ τ ]) σ p = stable k ∘-succ where k : [| _ |] (M [ τ ∘ σ ]) k = thm M (τ ∘ σ) (thm-C τ σ p)
代入
thm-C id σ p = stable-C p (sym-≡S ∘-lunit) thm-C (θ ∘ τ) σ p = stable-C u (sym-≡S ∘-assoc) where k : [| _ |]C (τ ∘ σ) k = thm-C τ σ p u : [| _ |]C (θ ∘ (τ ∘ σ)) u = thm-C θ (τ ∘ σ) k thm-C Weak σ p = proj₁ p thm-C ⟨ τ , M ⟩ σ p = stable-C ih₁ e₁ ,′ stable ih₂ e₂ where ih₁ : [| _ |]C (τ ∘ σ) ih₁ = thm-C τ σ p ih₂ : [| _ |] (M [ σ ]) ih₂ = thm M σ p module S = Reasoning (SubstSetoid nil _)
WeakとVarがそれぞれ第一要素と第二要素の射影のように働くことが分かっていれば、以下が成り立つのは明らかでしょう：
e₁ : τ ∘ σ ≡S Weak ∘ (⟨ τ , M ⟩ ∘ σ) e₁ = S.begin τ ∘ σ S.≈⟨ cong-∘₁ Weak-ext ⟨ (Weak ∘ ⟨ τ , M ⟩) ∘ σ S.≈⟨ ∘-assoc ⟩ Weak ∘ (⟨ τ , M ⟩ ∘ σ) S.∎ module T = Reasoning (TermSetoid nil _) e₂ : M [ σ ] ≡T Var [ ⟨ τ , M ⟩ ∘ σ ] e₂ = T.begin M [ σ ] T.≈⟨ cong-[]₁ Var-ext ⟨ Var [ ⟨ τ , M ⟩ ] [ σ ] T.≈⟨ ∘-succ ⟨ Var [ ⟨ τ , M ⟩ ∘ σ ] T.∎
Canonicity
以上より、canonicityが成り立つことが分かります：
canonicity : (M : Term nil bool) → M ≡T true ⊎ M ≡T false canonicity M = stable (thm M id tt) id-nop
計算
neovimのcornelisなら:CornelisNormalize、emacsのagda-modeならC-c C-nから、canonicity (App (Abs false) true)などと入力すると、その項がtrueとfalseのどちらと等しいかがinj₁かinj₂によって表示され、さらにその等価性の証明が以下のように出力されます。
inj₂
(trans-≡T (sym-≡T id-nop)
(trans-≡T (sym-≡T (sym-≡T comm-App))
(trans-≡T
(sym-≡T
(sym-≡T
(trans-≡T (cong-App₁ comm-Abs)
(trans-≡T =>β
(trans-≡T (sym-≡T ∘-succ)
(trans-≡T
(cong-[]₂
(trans-≡S (sym-≡S ext-Weak-Var)
(trans-≡S
(cong-⟨⟩
(trans-≡S (sym-≡S ∘-assoc)
(trans-≡S (cong-∘₁ Weak-ext)
(trans-≡S ∘-assoc
(trans-≡S (cong-∘₂ Weak-ext)
(trans-≡S ∘-runit (trans-≡S (sym-≡S Weak-ext) refl-≡S))))))
(trans-≡T ∘-succ
(trans-≡T (cong-[]₁ Var-ext)
(trans-≡T Var-ext (trans-≡T (sym-≡T Var-ext) refl-≡T)))))
(trans-≡S ext-Weak-Var refl-≡S))))
refl-≡T))))))
comm-false)))