定数の写像

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

読書案内 · 依存マップ

定数域の間の関数は、各定数記号を置き換え、変数をそのままにすることで一階の構文に作用します。本章では項と論理式に対するこの作用を定義して合成との両立を証明し、さらに論理式の写像を特殊化して、定数域が空型である無パラメータ論理式を任意の定数域上の論理式へ移します。

var 0 ∈̇ con k という論理式は、二つの対象を二つの仕方で指しています。var 0 は自由変数を経由し、con k は定数域、つまりある型 K を経由して指すのです。ここで関数 f : K → K' が与えられたとき、改名後の論理式はどんな形になるべきでしょうか。自然な答えは、動くのは定数だけ、というものです。con k は con (f k) になり、変数・所属関係・論理式全体の形はそのまま保たれます。本章ではまず項の上で、次に論理式の上でこの改名を定義します。使うのは構文の章の型 Term と Formula とそのすべての構成子、すなわち原子関係 _∈̇_ と _≐_、論理結合子、そして束縛形式 ∀̇∈ と ∃̇∈ を含む量化子です。

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

module FOL.Manipulation.ConstantMapping where

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

特別な定数域が一つ、後で独自に扱うことになります。空型 ⊥* です。定数域が ⊥* である論理式には定数がまったく現れず、本章の末尾では、そのような論理式が任意の K 上の論理式へどう写るかを扱います。それまでの議論は、定数域の間の任意の関数に対して行われます。

import Cubical.Data.Empty as Empty

構文への作用

構文は定数域に関して関手的です。写像 K → K' は項や論理式を通り抜けて定数だけを改名し、de Bruijn 変数と論理構造は保存します。本節ではこの作用を定義し、合成に関する法則は次節で証明します。

項に対する作用には選びようがありません。mapTm は改名関数 f : K → K' と自由変数の個数 n の項を受け取り、同じ個数 n の項を返します。定数 con k は con (f k) になり、変数 var i はそのまま返ります。これは定数記号の改名だけであり、代入ではなく、変数にはいかなる作用も持ちません。

mapTm : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Term K n → Term K' n
mapTm f (con k) = con (f k)
mapTm f (var i) = var i

mapFo : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}

原子論理式が、この作用の論理式への拡張のされ方を示します。t ∈̇ u の mapFo による像は mapTm f t ∈̇ mapTm f u です。同じ関係が、写像後の二つの項に、同じ個数 n の上で施されます。したがって先の例 var 0 ∈̇ con k は var 0 ∈̇ con (f k) に写り、動くのは定数だけです。

      → (K → K') → Formula K n → Formula K' n
mapFo f (t ∈̇ u)  = mapTm f t ∈̇ mapTm f u
mapFo f (t ≐ u)  = mapTm f t ≐ mapTm f u
mapFo f (φ ∧̇ ψ)  = mapFo f φ ∧̇ mapFo f ψ
mapFo f (φ ∨̇ ψ)  = mapFo f φ ∨̇ mapFo f ψ

量化された論理式は、論理構造が損なわれないことを示します。mapFo の下で、量化子の前置きはそのまま保たれ、自由変数の個数 suc n の本体は再帰的に写像されて同じ個数で返ります。各論理結合子は写像後の部分式の上で再構成されます。この操作は束縛子を増やしも減らしもせず、どの構成子も形を変えません。定数を含まない偽 ⊥̇ はそのまま写ります。

mapFo f (φ ⇒̇ ψ)  = mapFo f φ ⇒̇ mapFo f ψ
mapFo f ⊥̇        = ⊥̇
mapFo f (∃̇ φ)    = ∃̇ mapFo f φ
mapFo f (∀̇ φ)    = ∀̇ mapFo f φ
mapFo f (∀̇∈ t φ) = ∀̇∈ (mapTm f t) (mapFo f φ)

有界量化子 ∀̇∈ と ∃̇∈ は、項と論理式を併せ持つため、両方の操作が一度に現れる場合です。束縛する項 t は mapTm で改名され、本体は mapFo で写像されます。これにより mapFo は構文だけを変換し、論理式を解釈したり環境に触れたりすることは決してありません。

mapFo f (∃̇∈ t φ) = ∃̇∈ (mapTm f t) (mapFo f φ)

二つの写像を続けて施すことは一つの写像と同じです。f で写してから g で写すことは、λ k → g (f k) による一度の写像とパスとして一致します。定数域への作用のこの関手性は、後の章が中間の定数域を消去するのに使うものであり、構文の水準に属する法則です。

合成法則は可換な正方形として述べられます。項をまず f : K → K' で写し、次に g : K' → K'' で写すなら、その結果は合成 λ k → g (f k) による一度の写像と一致するはずです。mapTm-comp はまさにこれを Term K'' n のパスとして述べます。定数の場合、両辺はともに con (g (f k)) まで計算され、一致はすでに定義的等式として成り立つので、この場合は refl で証明できます。変数の場合は定数が現れないため、両辺は再び同じ項です。

mapTm-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (t : Term K n)
           → mapTm g (mapTm f t) ≡ mapTm (λ k → g (f k)) t
mapTm-comp f g (con k) = refl
mapTm-comp f g (var i) = refl

論理式に対しては、同じ正方形が mapFo-comp によって述べられます。正方形の二つの経路、すなわち mapFo g (mapFo f φ) と mapFo (λ k → g (f k)) φ は、同じ型 Formula K'' n のパスです。正方形は項に対してすでに証明されているので、原子論理式の場合に項について新たな議論は要りません。合同 cong₂ が二つの項のパスを、再構成された原子の間のパスへ持ち上げます。

mapFo-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (φ : Formula K n)
           → mapFo g (mapFo f φ) ≡ mapFo (λ k → g (f k)) φ
mapFo-comp f g (t ∈̇ u)  = cong₂ _∈̇_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (t ≐ u)  = cong₂ _≐_ (mapTm-comp f g t) (mapTm-comp f g u)

構造的な再帰によって正方形は論理結合子を通り抜けます。各部分式が正方形の自らのインスタンスを持ち、合同が二つの部分式のパスの上で結合子を再構成します。偽 ⊥̇ は定数も部分式も含まないため、両経路は同じ論理式まで計算され、この場合は refl です。

mapFo-comp f g (φ ∧̇ ψ)  = cong₂ _∧̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ∨̇ ψ)  = cong₂ _∨̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g ⊥̇        = refl
mapFo-comp f g (∃̇ φ)    = cong ∃̇_ (mapFo-comp f g φ)

量化子の場合で帰納が閉じます。前置量化子は一つの部分式に作用し、有界形式 ∀̇∈ と ∃̇∈ は項と本体を対にするので、項のパスと本体のパスの両方が使われます。Formula のすべての構成子が扱われたため、合成の正方形はすべての論理式で可換になります。この関手性は純粋に構文的な事実であり、後の章が中間の定数域を消去する必要が生じたときはいつでも利用できます。

mapFo-comp f g (∀̇ φ)    = cong ∀̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇∈ t φ) = cong₂ ∀̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
mapFo-comp f g (∃̇∈ t φ) = cong₂ ∃̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)

この写像のよく使われる例は、定数を一切持たない定数域から任意の定数域への移行です。無パラメータ論理式の定数域は空型であり、型 Formula (⊥* {ℓ}) n がその条件を表します。この型の論理式には定数の節がまったく現れませんが、n 個の自由変数のスロットはどれでも使えます。型 K への改名には関数 ⊥* → K が必要ですが、空型はまさにそのような関数が唯一つ、定義すべき場合分けもなく存在する型です。どこにも送るべき定数がないからです。これを提供するのが消去子 Empty.rec* であり、これに沿って定数を改名すると、無パラメータ論理式を任意の定数域上の論理式へ写せます。

embed はまさに mapFo Empty.rec* です。空の定数アルファベットからの関数 ⊥* → K は唯一なので、それをそのまま改名に用います。するとすべての定数の位置 (実際には一つもありません) がどこかに送られます。変わるのは定数域だけです。長さ n の自由変数の文脈と束縛子はそのままなので、embed は論理式を閉じたり変数への環境を与えたりするものではありません。

embed : ∀ {ℓ ℓ'} {K : Type ℓ'} {n} → Formula (⊥* {ℓ}) n → Formula K n
embed = mapFo Empty.rec*

まとめ

mapTm と mapFo は、定数域の写像が構文の水準で行う作用を表します。定数は改名され、変数・束縛子・個数はそのままです。mapFo-comp はこの作用が合成に関して関手的であることを証明し、embed は無パラメータの場合の例で、後の定数の改名とパラメータ抽象化の基礎になります。