変数の改名

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

有限な変数文脈の間の写像は、定数を固定したまま自由変数を改名して項と論理式へ作用します。環境の一致関係を用いる一つの意味論的定理が、弱化、交換、縮約をまとめて扱います。

構文の章が指摘した欠落、つまり代入も弱化もないことには理由があります。量詞の節が拡張された文脈の本体を直接受け取るため、変数を動かすための古典的な仕組みは不要でした。本書が実際に必要とする変数の移動は一つの装置で賄えます。それが改名です。写像 ρ : Fin n → Fin m を論理式へ押し通し、弱化、交換、縮約を一つの正しさの定理で同時に扱います。

公式の自由変数が n 個のスロットで索引づけられているとき、それを m 個のスロットの文脈で捉えたい場面を考えます。写像 ρ : Fin n → Fin m が各変数の行き先を決め、改名とはこの写像を公式のすべての自由変数に作用させることです。難所は量詞です。量詞の本体はスロットを一つ余分に持つ文脈で生きるので、ρ を束縛変数を乱さないように各束縛子の下で拡張する必要があります。

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.Renaming where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

そして改名は一つの正しさの定理で測られます。旧環境と新環境の間の適切な関係のもとで、改名された公式は元の公式と同じ命題を表します。命題は任意の命題値をとる任意の集合論的構造の上で計算されるので、定理は充足関係そのものとまったく同じ一般性を持ち、シーケント計算で慣用される構造規則、すなわち弱化、交換、縮約は、すべて ρ の特定の選択として得られます。

open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics

構文の水準

renameTm と renameFo は写像 Fin n → Fin m を構文へ通します。束縛子の下では、liftρ が新しく束縛された変数を固定し、元の変数を与えられた写像で移します。

有界量詞の下に自由変数を持つ公式を取りましょう。たとえば二つのスロットの文脈における ∀̇∈ x₀ (var 1 ∈̇ var 0) です。束縛変数は本体のスロット 0 であり、本体のスロット 1 は外側の自由変数 0 にあたります。改名 ρ : Fin n → Fin m は外側の変数を動かしますが、束縛子の下では Fin (suc n) → Fin (suc m) 上の写像、つまり束縛されたスロット 0 をスロット 0 へ送り、各旧スロット suc i を suc (ρ i) へ送るものが必要になります。この拡張が liftρ ρ であり、束縛変数が決して乱されないことを保証します。

liftρ : ∀ {n m} → (Fin n → Fin m) → Fin (suc n) → Fin (suc m)
liftρ ρ zero    = zero
liftρ ρ (suc i) = suc (ρ i)

持ち上げが手に入れば、改名は項へ、さらに公式へと構造的再帰で拡張できます。renameTm の型が考えのすべてを述べています。n 個の自由変数スロットを持つ項が m 個のスロットを持つ項になるのです。定数 con k は自由変数をまったく名指さないのでそのまま通ります。定数は文脈ではなくアルファベットに属し、その解釈は別の問題です。項のもう一つの形式である変数において、初めて ρ が実際に働きます。

renameTm : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Term K n → Term K m
renameTm ρ (con k) = con k

公式でも同じ流れです。renameFo は同じ形をし、n 個のスロット上の公式を m 個のスロット上の公式へ変えます。原子の節は項の引数を改名するので、例の公式では、外側のスロットにかぎれば var 1 ∈̇ var 0 は var (ρ 1) ∈̇ var (ρ 0) になります。命題結合子と偽はそれ自身は変数を持たず、改名された部分公式から再帰的に組み立て直されます。

renameTm ρ (var i) = var (ρ i)

renameFo : ∀ {ℓc} {K : Type ℓc} {n m} → (Fin n → Fin m) → Formula K n → Formula K m
renameFo ρ (t ∈̇ u)  = renameTm ρ t ∈̇ renameTm ρ u
renameFo ρ (t ≐ u)  = renameTm ρ t ≐ renameTm ρ u
renameFo ρ (φ ∧̇ ψ)  = renameFo ρ φ ∧̇ renameFo ρ ψ

通常の量詞は、再帰呼び出しが初めて変わる場所です。本体は拡張された文脈に住むので、呼び出しには ρ ではなく liftρ ρ が渡されます。これは例で述べた規則そのものです。束縛スロットはゼロに留まり、外側の改名は移された形でのみ本体に届きます。

renameFo ρ (φ ∨̇ ψ)  = renameFo ρ φ ∨̇ renameFo ρ ψ
renameFo ρ (φ ⇒̇ ψ)  = renameFo ρ φ ⇒̇ renameFo ρ ψ
renameFo ρ ⊥̇        = ⊥̇
renameFo ρ (∃̇ φ)    = ∃̇ renameFo (liftρ ρ) φ
renameFo ρ (∀̇ φ)    = ∀̇ renameFo (liftρ ρ) φ

有界量詞は二つの写像を同時に使います。例の公式はまさにここにあります。∀̇∈ t φ では、限界 t は外側の文脈に住むので ρ で改名され、本体 φ は liftρ ρ で改名されます。したがって ρ の下で ∀̇∈ x₀ (var 1 ∈̇ var 0) は ∀̇∈ (改名された限界) (var (suc (ρ 0)) ∈̇ var 0) になります。自由変数 0 への言及は移動に従って改名を追い、スロット 0 の束縛された出現はそのままです。これで構文の水準は完成です。次の節は、結果が最初の公式と同じ意味を持つかを問います。

renameFo ρ (∀̇∈ t φ) = ∀̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)
renameFo ρ (∃̇∈ t φ) = ∃̇∈ (renameTm ρ t) (renameFo (liftρ ρ) φ)

意味論の水準

Agrees ρ γ δ は、ρ で対応する変数に二つの環境が等しい値を割り当てることを表します。この条件は束縛子の下で環境を拡張しても保たれ、構造帰納法によって改名後の項の表示と論理式の充足関係が等しいと分かります。

構文だけでは改名が意味を保つかを言えず、環境を比較する必要があります。環境は構造の台の要素からなるベクトルで、長さは文脈と一致します。大きい文脈には γ : S ^ m、小さい文脈には δ : S ^ n です。問いはこう変わります。ρ の視点から、γ と δ はいつ同じ割り当てとみなせるのか。

module Sat {ℓ} (𝒮 : ZFStructure ℓ)
           {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) where

  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝒮

答えが関係 Agrees ρ γ δ です。小さい文脈の各索引 i について、δ の i での値と γ の ρ i での値が台におけるパスとして等しくなければなりません。参照の向きに注意してください。ρ は小さい文脈から大きい文脈へ向かうので、δ が i に割り当てるのは γ が ρ i に割り当てる値とちょうど同じです。n = 2 の例では、本体の変数 1 での一致は lookup (ρ 0) γ ≡ lookup 1 δ と読めます。つまり大きい環境は像の位置で小さい環境と一致しなければなりません。

  open Sem using ( _^_ )
  open Sem.At K ι using ( _⊨_; ⟦_⟧ )

  Agrees : ∀ {n m} → (Fin n → Fin m) → S ^ m → S ^ n → Type ℓ
  Agrees ρ γ δ = ∀ i → lookup (ρ i) γ ≡ lookup i δ

正しさの定理：改名された論理式の大きい環境における意味は、元の論理式の小さい環境における意味と同じです。まず項から始め、いつもの帰納法に進みます。各場合は同余性であり、束縛子の場合は agrees∷ を経由します。弱化 (使われない変数の挿入)、交換、縮約はすべて特殊例で、ρ を選ぶことによって得られます。

定理は公式の帰納法で進むので、一致関係は量詞の下の一歩を生き延びなければなりません。実際に生き延びます。両方の環境に位置ゼロで同じ要素 x を加えると、x ∷ γ と x ∷ δ は liftρ ρ の下で一致します。索引ゼロでは計算から両辺とも x を読み、索引 suc i での要求は既存の ag i に帰着します。この補題 agrees∷ は、構文の持ち上げに対応する意味論上の対応物です。

  agrees∷ : ∀ {n m} {ρ : Fin n → Fin m} {γ : S ^ m} {δ : S ^ n}
            (x : S) → Agrees ρ γ δ → Agrees (liftρ ρ) (x ∷ γ) (x ∷ δ)
  agrees∷ x ag zero    = refl
  agrees∷ x ag (suc i) = ag i

すべては二つの定理にかかっています。項については、γ と δ が ρ の下で一致するという仮定のもとで、大きい環境 γ で renameTm ρ t を評価したものは、小さい環境 δ で t を評価したものへのパスになります。公式では同様の主張が充足の命題を比較します。仮定 Agrees ρ γ δ が主張に実質を与えます。環境の間に何の関係もなければ、表示の等しいことは成り立ちようがありません。

  ⟦⟧-rename : ∀ {n m} (ρ : Fin n → Fin m) (t : Term K n)

項の証明は短い。項の中身が少ないからです。定数は環境に依存せず ι k を表すので、二つの評価は refl で同じです。変数 var i は小さい側では lookup i δ、大きい側では lookup (ρ i) γ を表し、索引 i での一致がまさに両者をつなぐパスなので、ag i がこの場合を閉じます。本質は一つ上の公式の定理にあります。

              (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
            → ⟦ renameTm ρ t ⟧ γ ≡ ⟦ t ⟧ δ
  ⟦⟧-rename ρ (con k) γ δ ag = refl
  ⟦⟧-rename ρ (var i) γ δ ag = ag i

  ⊨-rename : ∀ {n m} (ρ : Fin n → Fin m) (φ : Formula K n)

公式の定理は二つの命題の間のパスを述べます。大きい側の γ ⊨ renameFo ρ φ と、小さい側の δ ⊨ φ です。まず例の有界量詞を考えます。その本体にはさらに束縛子がありません。残りの場合はここで述べる同余と再帰という二つの型のどちらかに従います。原子公式では、項の定理が改名された項と元の項の表示の間のパスを与え、cong₂ がそのパスを集合の所属関係や等号を通して運びます。結合子の場合も対応する論理演算に cong₂ を使い、偽は refl で足ります。

             (γ : S ^ m) (δ : S ^ n) → Agrees ρ γ δ
           → (γ ⊨ renameFo ρ φ) ≡ (δ ⊨ φ)
  ⊨-rename ρ (t ∈̇ u)  γ δ ag = cong₂ _∈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (t ≐ u)  γ δ ag = cong₂ _≈ˢ_ (⟦⟧-rename ρ t γ δ ag) (⟦⟧-rename ρ u γ δ ag)
  ⊨-rename ρ (φ ∧̇ ψ)  γ δ ag = cong₂ _⊓_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)

無制限の存在量詞 ∃̇ φ の下では、充足は台のすべての候補要素 x を渡るので、証明は両側の x の関数が各点で等しいことを示さねばならず、ここで funExt が登場します。各 x で両側の環境は拡張 x ∷ γ と x ∷ δ であり、agrees∷ x ag により liftρ ρ の下で一致します。これは小さい公式での帰納法の仮定にほかなりません。ここが設計全体の要点です。一致関係は拡張の下で保たれるように作られているので、再帰呼び出しがそのまま通ります。

  ⊨-rename ρ (φ ∨̇ ψ)  γ δ ag = cong₂ _⊔_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ (φ ⇒̇ ψ)  γ δ ag = cong₂ _⇒_ (⊨-rename ρ φ γ δ ag) (⊨-rename ρ ψ γ δ ag)
  ⊨-rename ρ ⊥̇        γ δ ag = refl
  ⊨-rename ρ (∃̇ φ)    γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))

非有界な全称量化子 ∀̇ φ は双対で、∃[ x ] P x の代わりに ∀[ x ] P x を使い、funExt と agrees∷ の手順は同じです。有界全称量詞 ∀̇∈ t φ は二つの材料を組み合わせます。その充足は、x ∈ˢ ⟦ t ⟧ γ から本体の充足への含意についての x に対する ∀[ x ] P x です。限界は項の定理が供給する x ∈ˢ_ を通る cong を寄与し、本体は liftρ ρ での再帰呼び出しを寄与し、cong₂ _⇒_ が両者を含意の間の求めるパスへ接合します。

  ⊨-rename ρ (∀̇ φ)    γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    ⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag)))
  ⊨-rename ρ (∀̇∈ t φ) γ δ ag = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⇒_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

有界存在量詞 ∃̇∈ t φ が鏡像の形で帰納を閉じます。x に対する ∃[ x ] P x、改名された限界 x ∈ˢ ⟦ t ⟧ γ を ⊓ で本体の充足に結び、agrees∷ を経る同じ再帰呼び出しです。決して使われなかったものに注目してください。ρ の単射性です。定理は任意の写像 Fin n → Fin m` に対して述べられているので、二つの変数を一つへ畳み込むこと (縮約) も、変数を間隔を空けて並べること (弱化) も、順序を入れ替えること (交換) も、同じく許されます。

  ⊨-rename ρ (∃̇∈ t φ) γ δ ag = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
    cong₂ _⊓_ (cong (x ∈ˢ_) (⟦⟧-rename ρ t γ δ ag))
              (⊨-rename (liftρ ρ) φ (x ∷ γ) (x ∷ δ) (agrees∷ x ag))))

まとめ

変数の改名は、構文写像、環境の一致、定理 ⊨-rename からなります。文脈の写像を選ぶことで、この一つのインターフェースを弱化、交換、縮約へ特殊化できます。