仕様 tableAt は、二つの定義域条件 total、onC と十個の構成子の節を組み合わせます。一つの構成子の節は、どのように意味論的再帰の一段階になるのでしょうか。本章はまず各節を候補となる値集合の正確な外延条件として読み、次に再帰的に構成した集合 SatW も同じ条件を満たすことを示します。周囲の議論からさらに、一致するコード、その部分値、表要素が与えられれば、外延性によって二つの値を同一視できます。局所的な橋渡しだけでは、表全体の単値性や一意性は証明されません。

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

議論はレベル ℓ-suc ℓ の排中律を明示的な引数として受け取ります。それでも、復号の証人の型が命題的に切り詰められているとき、結論が述べるのは単なる存在だけです。この古典的仮定が証人を選択済みのデータに変えることはありません。

open import Base.Prelude
open import Base.Classical using ( LEM )

以下の構成はすべて、固定した仮定 lem に相対して述べられます。これにより、局所的な節の読み補題が後で全体の健全性と完全性の証明に使われても、その論理的な費用が明示されたままになります。

module L.Coding.SatisfactionClauseSemantics {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

この証明では二つの言語が出会います。内部の論理式は L の中で符号化された表を記述し、外部の論理式は W が表示する構造で再帰的に解釈されます。橋渡しはすべての論理式構成子を保たなければならず、有界量化子の境界は現在の環境における項の値によって与えられます。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _∧̇_; _∨̇_; _⇒̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∃̇∈; ∀̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

有限環境は内部では順序対 (i,v) のグラフとして表されます。順序対の単射性から添字と値を復元でき、lookup-spec は正準なグラフが各ホストレベルのスロットに対応する対をちょうど含むことを述べます。後で envSet W n に属するという主張から得られるのは、その集合が長さ n で W に値を取る何らかの割り当てのグラフだという単なる存在です。

open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.Model {ℓ} using ( prAtL; container )

内部の節が順序対の成分を調べるときは、有界論理式だけを使います。container は二つの成分をともに含む一つの構成可能集合を与えるので、対の読み補題は非有界な探索なしに成分を束縛できます。同様に consAtL の読み補題は x ∷ δ のグラフを δ のグラフと結び付け、量化子に必要な意味論的な一歩を与えます。

open import L.Coding.Expressions {ℓ} using ( sucAtL; consAtL )
import L.Coding.Expressions {ℓ} as CodingExpressions
module E = CodingExpressions.PairExpression
open import L.Axioms.Basic {ℓ} using ( extensionalL )
open import L.Coding.Quantification {ℓ} using

ここでは三種類の有限添字を区別しなければなりません。自然数 n は論理式のアリティ、# n はコード内でそのアリティを表す集合論的な数項、Fin m は長さ m のホストレベルのベクトルのスロットを選びます。i0 から i19 までの名前とシフト sh が扱うのは最後の種類だけです。束縛子がベクトルの先頭に値を加えるたびに、以前のスロットはその分だけずらされます。

  ( i0; i1; i2; i3; i4; i5; i6; i8; i9; i11; i12; i14; i16; i17; i19; sh
  ; pr-out; pr-in; down; sndS; suc-out; suc-in
  ; sndEx; sndAll; bothEx
  ; sndEx-out; sndAll-in; bothEx-out; bothAll-in
  ; fillSnd; fillBoth; useSnd; useBoth )

共通の表の枠組みには、固定された入れ子の形があります。環境塔の要素は (ar,F)、論理式キーは (ar,p)、そのペイロードは (tag,r)、表の要素は (c,yc) を符号化します。以下の読み補題はこれらの対を順にほどき、構成子の関係が環境集合 F 上の候補値 yc の外延を述べられるようにします。

open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.Coding.SatisfactionClauses {ℓ}
  using ( extB; fstAll; subAt; subSucAt; tmIs; module Rel; module Clause )

外部の環境は有限ベクトルですが、表に保存されるのは集合論的なグラフです。両者を行き来するには、ホストレベルの有限参照と対象レベルの対の所属の双方が必要です。積と直和は論理式や項の構成子から生じる場合を記録しますが、それらの場合を符号化された集合そのものと混同しません。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.Vec using ( _∷_; []; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )

意味論的な比較の多くは、二方向の含意から得られる命題間のパスです。命題的切り詰めも同じく本質的です。対の分解や復号された環境の証人は命題の内部では利用できますが、それらの証人の大域的な選択は得られません。

open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

すべてのコードは累積階層の中にあります。したがって順序対のコードと数項 # n は実際の集合であり、それらの単射性によって、後の証明はコード間の等式からアリティ、タグ、ペイロードを復元できます。累積階層の h-集合構造により、こうして得られる等式は命題値になります。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )

内部の割り当ては構成可能な台 S に値を取りますが、そこで現れる等式と所属は fst で射影した底集合について述べられます。有界絶対性が、この台における内部論理式の解釈を与えます。したがって各読み補題は最後に射影された集合についての具体的な主張を返し、外部の再帰と比較できる形になります。

open hPropStructure 𝒮ʟ using ( S )
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

共通の枠組みを読む

中心となる型は、集合 y についての外延的な事実を記録します。y のすべての要素が F に属し性質を満たすこと、また逆に、F の中で性質を満たすすべての要素が y に属することです。値の集合は、選ばれた列挙ではなく、このような事実によって記述されます。

ExtFact : (y F : V ℓ) (P : S → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ)
ExtFact y F P = ((z : S) → ⟨ fst z ∈ y ⟩ → ⟨ fst z ∈ F ⟩ × P z)
              × ((z : S) → ⟨ fst z ∈ F ⟩ → P z → ⟨ fst z ∈ y ⟩)

外延的な集合の構成子の読みは定義的です。構成子の充足は文字どおり、二つの所属の方向の対であり、性質は束縛変数で延長された環境のもとで評価されます。

module _ {j : ℕ} (y F : Fin j) (φ : Formula S ( + j)) (δ : S ^ j) where
  extB-out : ⟨ δ ⊨ extB y F φ ⟩ → ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩)
  extB-out h = h

埋めも同じく定義的です。外延的な事実は、構成子の充足にほかなりません。

  extB-in : ExtFact (fst (lookup y δ)) (fst (lookup F δ)) (λ z → ⟨ (z ∷ δ) ⊨ φ ⟩) → ⟨ δ ⊨ extB y F φ ⟩
  extB-in h = h

y と y' が F 上で同じ外延条件を満たすと仮定します。すなわち、F の要素については、どちらの集合への所属も性質 P によって特徴付けられます。外延性により、底集合の等しさは二方向の所属の変換へ帰着します。順方向では、y の要素をその外延条件の外向きの半分で読み、続いて y' の外延条件の内向きの半分を適用します。

ext-unique : (y y' F : S) (P : S → Type (ℓ-suc ℓ))
           → ExtFact (fst y) (fst F) P → ExtFact (fst y') (fst F) P → fst y ≡ fst y'
ext-unique y y' F P (o1 , i1') (o2 , i2') =
  cong fst (extensionalL {a = y} {b = y'} (λ z → ⇔toPath
    (λ hz → i2' z (o1 z hz .fst) (o1 z hz .snd))

逆方向の変換が同値を閉じます。右側の要素は、まず F に属し性質を満たす要素として認められ、外延的な事実のもう半分が、y の中での所属を返します。二つの変換を合成すれば、y と y' の底の集合の等しさが得られます。同一視されるのは底の集合であり、選ばれた符号化の証拠ではありません。

    (λ hz → i1' z (o2 z hz .fst) (o2 z hz .snd))))

部分論理式の値を使うため、表のスロット T、アリティのスロット ar、ペイロードのスロット a、そして四つの新しい要素を期待する本体を固定します。読み補題は一致する表の対 (c₁,ya) を取り出し、古い環境の前に、値 ya、キー c₁、対の成分を収める集合、表の要素そのものの構成可能な表示をこの順に置きます。

module _ {j : ℕ} (T ar a : Fin j) (body : Formula S ( + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)

射影されたアリティを A、射影されたペイロードを Av と書きます。部分キーの一致条件は一つの等式 fst c₁ ≡ pr A Av となり、集合論的に符号化されたキーと、その二成分を与えたホストレベルのスロットとが区別されます。

    Av = fst (lookup a δ)

subAt が成り立つなら、底の対が (c₁,ya) であり、キーが c₁=(A,Av) を満たすすべての表要素から本体が従います。本体は ya ∷ c₁ ∷ s ∷ e' ∷ δ で評価されます。ここで e' はその表要素を表し、s は対の二成分を取り出すためだけの容器です。どちらも追加の意味論的な値ではありません。

  subAt-out : ⟨ δ ⊨ subAt T ar a body ⟩ → (c₁ ya : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
            → fst c₁ ≡ pr A Av
            → ⟨ (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                 ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩
  subAt-out h c₁ ya m e =

証明はまず、表上の有界全称を (c₁,ya) の具体的な表示 e' に適用します。次に対の読み補題が二成分 c₁ と ya を与え、最後に pr-in が等式 c₁=(A,Av) を内部の含意が要求する前件へ変換します。残るのは四スロット拡張での本体そのものです。

    useBoth i0 (down TS (pr (fst c₁) (fst ya)) m ∷ δ) c₁ ya refl (prAtL i1 (sh  ar) (sh  a) ⇒̇ body)
      (h (down TS (pr (fst c₁) (fst ya)) m) m)
      (pr-in i1 (sh  ar) (sh  a)
        (ya ∷ c₁ ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
           ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) e)

埋めはその逆です。一致するすべての表の項目とその容器について本体が証明できれば、表の項目の上の有界全称が成立します。この読み手がしないことに注意してください。項目を一つ選ぶことも、値 ya が一意だと主張することもなく、一致するすべての項目の上で量化するだけです。

  subAt-in : ((c₁ ya s e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A Av
              → ⟨ (ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
           → ⟨ δ ⊨ subAt T ar a body ⟩
  subAt-in g e' e'∈ = bothAll-in i0 (prAtL i1 (sh  ar) (sh  a) ⇒̇ body) (e' ∷ δ)
    (λ c₁ ya s s∈ c₁∈ ya∈ e hp → g c₁ ya s e' e'∈ e (pr-out i1 (sh  ar) (sh  a) (ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp))

第二の部分節の読みは、アリティが上がった形に対して述べられます。その本体は六つの枠を延長します。量化された論理式の部分論理式は、上げられたアリティで読まれるからです。

module _ {j : ℕ} (T ar a : Fin j) (body : Formula S ( + j)) (δ : S ^ j) where
  private
    Tv = fst (lookup T δ)
    TS = lookup T δ
    A = fst (lookup ar δ)

外側の論理式のアリティの値が名付けられ、上げられたアリティは証明の内部で別に復元されます。

    Av = fst (lookup a δ)

持ち上げられた読み補題は、キーが (ar',Av) である表要素と、等式 fst ar' ≡ sucV A を使います。本体は ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ で評価されます。二つの容器 s' と s は、有界論理式から持ち上げられたキーと表要素の成分を利用できるようにするだけです。

  subSucAt-out : ⟨ δ ⊨ subSucAt T ar a body ⟩ → (c₁ ya ar' : S) (m : ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩)
               → (e : fst c₁ ≡ pr (fst ar') Av) → fst ar' ≡ sucV A
               → ⟨ (ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ ya ∷ c₁
                    ∷ container (down TS (pr (fst c₁) (fst ya)) m) c₁ ya refl .fst
                    ∷ down TS (pr (fst c₁) (fst ya)) m ∷ δ) ⊨ body ⟩

証明は与えられた表要素から出発し、まず (c₁,ya) を分解して四スロットの主張 h4 を得ます。次に fstAll へ第一成分の候補 ar' を与え、pr-in で c₁=(ar',Av) を、suc-in で ar'=suc A を証明します。本体を使う前に必要な条件は、まさにこの二つの等式です。

  subSucAt-out h c₁ ya ar' m e es =
    (h4 (container c₁ ar' (lookup a δ) e .fst) (container c₁ ar' (lookup a δ) e .snd .fst)
        ar' (container c₁ ar' (lookup a δ) e .snd .snd .fst)
        (pr-in (sh  i1) i0 (sh  (sh  a)) δ6 e))
      (suc-in (sh  ar) i0 δ6 es)

局所名 e'S は、特定の表要素 (c₁,ya) の構成可能な表示であり、その対が T に属することから得られます。環境 δ4 は δ の前に ya、c₁、その対の成分を収める容器、e'S をこの順に置きます。表全体の表示が入っているわけではありません。

    where
    e'S = down TS (pr (fst c₁) (fst ya)) m
    δ4 : S ^ ( + j)
    δ4 = ya ∷ c₁ ∷ container e'S c₁ ya refl .fst ∷ e'S ∷ δ
    δ6 : S ^ ( + j)

選んだ表要素に useBoth を適用すると、表上の外側の量化と対の分解が一度に除かれます。得られる h4 は δ4 における残りの fstAll の主張です。そこではなお c₁ の第一成分の候補を与え、その成分が後続アリティであることを示す必要があります。

    δ6 = ar' ∷ container c₁ ar' (lookup a δ) e .fst ∷ δ4
    h4 : ⟨ δ4 ⊨ fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body) ⟩
    h4 = useBoth i0 (e'S ∷ δ) c₁ ya refl (fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body)) (h e'S m)

逆方向では、表要素のあらゆる分解と、そのキーの第一成分のあらゆる分解について、一様に本体を証明すれば十分です。仮定中の二つの等式により、キーが (suc A,Av) である要素だけが関係します。特定の表要素や持ち上げられたアリティを大域的に選ぶことはありません。

  subSucAt-in : ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
                 → fst c₁ ≡ pr (fst ar') Av → fst ar' ≡ sucV A
                 → ⟨ (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) ⊨ body ⟩)
              → ⟨ δ ⊨ subSucAt T ar a body ⟩
  subSucAt-in g e' e'∈ = bothAll-in i0 (fstAll i1 (sh  a) (sucAtL (sh  ar) i0 ⇒̇ body)) (e' ∷ δ)

導入の証明は、二段の全称的な対の読みから現れる成分を受け取ります。pr-out で等式 c₁=(ar',Av) を、suc-out で ar'=suc A を復元し、それらの等式、表への所属、六スロットの環境を一様な仮定 g に渡します。

    (λ c₁ ya s s∈ c₁∈ ya∈ e s' s'∈ ar' ar'∈ hp hs →
      g c₁ ya ar' s s' e' e'∈ e
        (pr-out (sh  i1) i0 (sh  (sh  a)) (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hp)
        (suc-out (sh  ar) i0 (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) hs))

TmIsV t z v は、命題的切り詰めの下で項コードの二つの形を記録します。定数の場合は t=(#0,v) です。変数の場合は、t=(#1,i) かつグラフ要素 (i,v) が z に属する添字 i が単に存在します。任意の関係 z に対するこの主張には、単値性も一意性も含まれません。

TmIsV : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
TmIsV t z v = ∥ (t ≡ pr (# ) v) ⊎ (Σ[ i ∈ V ℓ ] ((t ≡ pr (# ) i) × ⟨ pr i v ∈ z ⟩)) ∥₁

局所的な読み補題は、項コード、環境グラフ、候補値、二つのタグ数項という五つのホストレベルのスロットでパラメータ化されます。仮定 q0 と q1 は最後の二スロットを #0 と #1 に同一視し、局所名 Tv と Z は項コードとグラフを、符号化の等式が置かれる累積階層へ射影します。

module _ {j : ℕ} (t z v N0 N1 : Fin j) (δ : S ^ j)
  (q0 : fst (lookup N0 δ) ≡ # ) (q1 : fst (lookup N1 δ) ≡ # ) where
  private
    Tv = fst (lookup t δ)
    Z = fst (lookup z δ)

残る二つの射影は、候補値 Vv とタグ一のスロットに実際に入っている集合 N1v を名付けます。内部論理式は N1v を参照しますが、TmIsV の変数の場合は正準な数項 #1 を使うため、証明は q1 に沿って等式を輸送しなければなりません。

    Vv = fst (lookup v δ)
    N1v = fst (lookup N1 δ)

内側の有界存在が動くのはグラフ z の要素 q であり、添字そのものではありません。その対のアトムは q=(i,v) を主張し、添字 i はすでに項コードの第二成分として復元されています。したがって内部論理式は、その固定した添字と候補値を組にした要素がグラフに含まれることを述べます。

    inner : Formula S ( + j)
    inner = ∃̇∈ (var (sh  z)) (prAtL i0 i1 (sh  v))

Inner i s は、この有界存在の意味を詰め直します。そこから得られるのは、グラフ要素 q、q∈Z の証明、そして q ∷ i ∷ s ∷ δ において対のアトム q=(i,Vv) が成り立つ証明だけです。スロット s は項コードの成分を取り出すための容器です。

    Inner : (i s : S) → Type (ℓ-suc ℓ)
    Inner i s = ∥ Σ[ q ∈ S ] (⟨ fst q ∈ Z ⟩ × ⟨ (q ∷ i ∷ s ∷ δ) ⊨ prAtL i0 i1 (sh  v) ⟩) ∥₁

Outer は sndEx から読み出した変数の場合の全体をまとめます。ペイロードの表示 i と容器 s が単に存在し、Tv=pr N1v (fst i) が成り立ち、内側の有界存在が i ∷ s ∷ δ で成り立ちます。この等式が項コードと同一視するのはタグ一の対であり、i とタグそのものではありません。

    Outer : Type (ℓ-suc ℓ)
    Outer = ∥ Σ[ i ∈ S ] Σ[ s ∈ S ] ((Tv ≡ pr N1v (fst i)) × ⟨ (i ∷ s ∷ δ) ⊨ inner ⟩) ∥₁

内側の証人 q から pr-out により fst q=pr (fst i) Vv が得られ、既知の所属 q∈Z をこの等式に沿って輸送すると、必要なグラフ要素 (i,Vv) の所属が得られます。同時に q1 は、外側の等式に現れる実際のタグスロット N1v を #1 に書き換えます。この二つが TmIsV の変数の場合の二つの成分そのものです。

    viaQ : (i s : S) → Tv ≡ pr N1v (fst i) → Inner i s → TmIsV Tv Z Vv
    viaQ i s e = PT.map
      (λ { (q , (q∈ , hp)) → inr (fst i , ( e ∙ cong (λ a → pr a (fst i)) q1
         , subst (λ u → ⟨ u ∈ Z ⟩) (pr-out i0 i1 (sh  v) (q ∷ i ∷ s ∷ δ) hp) q∈ )) })

viaI は、単に存在する外側の分解を TmIsV へ消去します。TmIsV 自身も命題的に切り詰められているため、この消去は各局所的な対の分解を変換するだけで、後で使う一つの分解を選び出すことはありません。

    viaI : Outer → TmIsV Tv Z Vv
    viaI = PT.rec squash₁ (λ { (i , s , (e , hq)) → viaQ i s e hq })

対象論理式 tmIs は二つのコード形の選言です。定数の場合、pr-out が Tv=pr(q0,Vv) を読み出し、q0=#0 によってそれを TmIsV の第一の場合へ変換します。変数の場合、sndEx-out が Outer を生成し、viaI がそれをグラフ所属の場合へ変換します。

    cases : ⟨ δ ⊨ prAtL t N0 v ⟩ ⊎ ⟨ δ ⊨ sndEx t N1 inner ⟩ → TmIsV Tv Z Vv
    cases (inl h) = ∣ inl (pr-out t N0 v δ h ∙ cong (λ a → pr a Vv) q0) ∣₁
    cases (inr h) = viaI (sndEx-out t N1 inner δ h)

公開された消去補題 tmIs-out は、外側の選言の命題的切り詰めの下でこの場合分けを行います。結論は一つの候補値 Vv について述べるだけで、二つの候補値が等しいことは示しません。Z が任意の多値関係なら、同じ変数コードが複数の値で tmIs を満たしえます。

  tmIs-out : ⟨ δ ⊨ tmIs t z v N0 N1 ⟩ → TmIsV Tv Z Vv
  tmIs-out h = PT.rec squash₁ cases h

逆方向では、build が二つの具体的なコード形のどちらからでも tmIs の充足を再構成します。定数の等式は pr-in で変換します。変数の場合は、ペイロードの添字とグラフ要素を S の要素として表示し、その後 sndEx の入れ子になった有界存在を組み立て直します。

  private
    build : (Tv ≡ pr (# ) Vv) ⊎ (Σ[ i ∈ V ℓ ] ((Tv ≡ pr (# ) i) × ⟨ pr i Vv ∈ Z ⟩))
          → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
    build (inl e) = ∣ inl (pr-in t N0 v δ (e ∙ cong (λ a → pr a Vv) (sym q0))) ∣₁
    build (inr (i , (e , hp))) = ∣ inr (fillSnd t δ (lookup N1 δ) iS e' inner hq N1 refl) ∣₁

iS はペイロード i の構成可能な表示であり、対の等式 Tv=(#1,i) の第二成分として復元されます。qS はグラフ要素 (i,Vv) の構成可能な表示であり、その対が Z に属することから得られます。これらは S 内の証人であって、新しい意味論的な添字や値ではありません。

      where
      iS : S
      iS = sndS (lookup t δ) (# ) i e
      qS : S
      qS = down (lookup z δ) (pr i Vv) hp

等式 e' は正準なタグの等式を、sndEx が要求する実際のタグ一スロットに書き換えます。補助環境 δ3 は δ の前に、グラフ要素 qS、ペイロードの表示 iS、外側の項コードの対を収める容器をこの順に置きます。残る目標 hq は、iS ∷ container ∷ δ における内側の有界存在そのものです。

      e' : Tv ≡ pr N1v (fst iS)
      e' = e ∙ cong (λ a → pr a i) (sym q1)
      δ3 : S ^ ( + j)
      δ3 = qS ∷ iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ
      hq : ⟨ (iS ∷ container (lookup t δ) (lookup N1 δ) iS e' .fst ∷ δ) ⊨ inner ⟩

hq を証明するには、グラフから qS を選びます。その所属は与えられた事実 hp であり、pr-in は反射性によって、その底集合が iS と Vv の対であることを示します。これで変数の場合に必要なグラフ要素がちょうど得られます。

      hq = ∣ qS , (hp , pr-in i0 i1 (sh  v) δ3 refl) ∣₁

最後に tmIs-in は、TmIsV の命題的切り詰めを tmIs の充足を表す命題へ消去し、どちらの場合にも build を適用します。tmIs-out と合わせて意味論の二方向が得られますが、大域的な選択や一意性の主張は導入されません。

  tmIs-in : TmIsV Tv Z Vv → ⟨ δ ⊨ tmIs t z v N0 N1 ⟩
  tmIs-in = PT.rec (snd (δ ⊨ tmIs t z v N0 N1)) build

Frame は、表 T、台 w、コード領域 C、環境塔 E のホストレベルのスロットに加え、十個のタグスロット N と周囲の割り当て γ を固定します。仮定 Tags γ N は各タグスロットを対応する数項と同一視し、k : Fin 10 で選ばれた節を関係 relN (toℕ k) として読めるようにします。

module Frame {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
    Ev = fst (lookup E γ)

枠組みは有界全称の列によって順にほどかれます。最も内側では inner9 k がすべての表要素を動き、その第一成分が c であるとき sndAll によって値 yc を取り出します。得られた十二スロットの環境で relN (toℕ k) が成り立たなければなりません。これは一致するすべての要素についての全称条件であり、一つの値を探す存在条件ではありません。

    module Cl = Clause T w C E N
    module R = Rel T w N
    inner9 : Fin  → Formula S ( + m)
    inner9 k = ∀̇∈ (var (sh  T)) (sndAll i0 i5 (R.relN (toℕ k)))
    inner7 : Fin  → Formula S ( + m)

その前の段階では入れ子になったキーを取り出します。inner4 k は、第一成分が現在のアリティ ar であるすべての c∈C を動き、そのペイロード p を得ます。続いて inner7 k は p のタグが N k のスロットにある数項であることを要求し、残りのデータ r を取り出します。対を分解するたびに成分と容器が先頭へ加わるため、以前の枠組みのスロットへの参照はシフトによって保たれます。

    inner7 k = sndAll i0 (sh  (N k)) (inner9 k)
    inner4 : Fin  → Formula S ( + m)
    inner4 k = ∀̇∈ (var (sh  C)) (sndAll i0 i2 (inner7 k))

一つの節の実例について、At は塔の対 (ar,F)、論理式キー c=(ar,p)、タグ付きペイロード p=(N k,r)、表の対 (c,yc) を固定します。所属 q∈ と e∈ はそれぞれ E と T における射影された対について述べます。このモジュール自身は c∈C を証明せず、r を復号せず、表の値の一意性も示しません。

  module At (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩)
            (ec : fst c ≡ pr (fst ar) (fst p)) (k : Fin )
            (ep : fst p ≡ pr (fst (lookup (N k) γ)) (fst r))
            (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩) where
    qS eS : S

qS と eS は、二つの射影された対の所属を構成可能な台の要素へ持ち上げます。それらの底集合はそれぞれ定義により pr (fst ar) (fst F) と pr (fst c) (fst yc) です。十二スロットの環境を組み立てるとき、有界な対の読み補題を適用するための表示としてだけ使われます。

    qS = down (lookup E γ) (pr (fst ar) (fst F)) q∈
    eS = down (lookup T γ) (pr (fst c) (fst yc)) e∈

枠は、基礎の対が (ar,F) である塔の実際の要素 qS から始まります。新しい四つの枠には F、ar、対への分解の証人、qS が入り、続く三つにはペイロード p、c=(ar,p) の証人、符号 c が入ります。このように、順次拡張される環境は、数学的データと、対象言語の節がそのデータを得るために用いた有界な証人の両方を保持します。

    δ4 : S ^ ( + m)
    δ4 = F ∷ ar ∷ container qS ar F refl .fst ∷ qS ∷ γ
    δ7 : S ^ ( + m)
    δ7 = p ∷ container c ar p ec .fst ∷ c ∷ δ4
    δ9 : S ^ ( + m)

十二の枠の環境がこの入れ子を完成させます。先頭には候補値 yc があり、表の対 (c,yc) の二成分を取り出すコンテナと、底集合がその対である実際の表要素 eS が続き、その後に先の九つの対象が並びます。関係の本体はこの環境で読み取られます。

    δ9 = r ∷ container p (lookup (N k) γ) r ep .fst ∷ δ7
    δ12 : S ^ ( + m)
    δ12 = yc ∷ container eS c yc refl .fst ∷ eS ∷ δ9

外向きの読み取りは第 k 節の充足から出発し、その枠の一つの実例に対応するデータをすべて固定します。塔の対から得られる ar と F、C に属するコード c=(ar,p)、タグ付きペイロード p=(#k,r)、そして (c,yc) が T に属する候補値 yc です。そのうえで、対応する十二の枠の環境における relN (toℕ k) の充足を返します。ここで表について仮定するのは対 (c,yc) の所属であり、実際の表要素とそのコンテナは局所的に構成されます。

  clause-out : (k : Fin ) → ⟨ γ ⊨ Cl.clause k ⟩
             → (ar F c p r yc : S) (q∈ : ⟨ pr (fst ar) (fst F) ∈ Ev ⟩) → ⟨ fst c ∈ Cv ⟩
             → (ec : fst c ≡ pr (fst ar) (fst p)) → (ep : fst p ≡ pr (# (toℕ k)) (fst r))
             → (e∈ : ⟨ pr (fst c) (fst yc) ∈ Tv ⟩)
             → ⟨ At.δ12 ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈ ⊨ R.relN (toℕ k) ⟩

対応するデータを固定すると、モジュール A は十二の枠すべてに対して整合した一つの実現を与えます。最初の除去が塔の対を開き、最後の useSnd が実際の表の要素を (c,yc) として開きます。その間には符号とタグの層を通る必要があります。そこで先に h4 を名づけることで、結論が構成子の関係を別に仮定したものではなく、一つの外側の節を順次特殊化して得られることが明示されます。

  clause-out k h ar F c p r yc q∈ c∈ ec ep e∈ =
    useSnd i0 (A.eS ∷ A.δ9) c yc refl (R.relN (toℕ k)) i5 refl (h9 A.eS e∈)
    where
    module A = At ar F c p r yc q∈ ec k (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) e∈
    h4 : ⟨ A.δ4 ⊨ inner4 k ⟩

三つの中間判断は、共通の枠の三つの意味論的な層を示します。δ4 では h4 が塔の項目 (ar,F) を開き、C の符号を調べられる状態にあります。δ7 では h7 がさらに c=(ar,p) を分解しています。δ9 では h9 が p をタグ k のペイロード r と同定し、T の項目を調べられる状態にあります。最後の除去で、選んだ表の要素を (c,yc) と分解し、構成子の関係に到達します。

    h4 = useBoth i0 (A.qS ∷ γ) ar F refl (inner4 k) (h A.qS q∈)
    h7 : ⟨ A.δ7 ⊨ inner7 k ⟩
    h7 = useSnd i0 (c ∷ A.δ4) ar p ec (inner7 k) i2 refl (h4 c c∈)
    h9 : ⟨ A.δ9 ⊨ inner9 k ⟩
    h9 = useSnd i0 A.δ7 (lookup (N k) γ) r (ep ∙ cong (λ a → pr a (fst r)) (sym (tg k))) (inner9 k) (sh  (N k)) refl h7

逆向きの構成では、完全に対応するすべての枠から構成子の関係を証明できると仮定します。そのような枠は、塔の要素 q=(ar,F)、C に属する符号 c=(ar,p)、タグの分解 p=(#k,r)、表の要素 e=(c,yc)、および四つの対の証人 s、s1、s2、s3 からなります。これらすべてのデータについて表示された環境で関係を証明できることが、第 k 節を再構成するために必要な前提そのものです。

  clause-in : (k : Fin )
            → ((q ar F s c p s1 r s2 e yc s3 : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F)
               → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (fst ar) (fst p) → fst p ≡ pr (# (toℕ k)) (fst r)
               → ⟨ fst e ∈ Tv ⟩ → fst e ≡ pr (fst c) (fst yc)
               → ⟨ (yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) ⊨ R.relN (toℕ k) ⟩)

証明は全称量化された枠を論理的な順序で組み直します。まず E の任意の q と、そこから取り出される各分解 q=(ar,F) を扱い、次に C の任意の c と、それに一致する各分解 c=(ar,p) を扱います。続いて p のタグとペイロードを同定し、最後に T の任意の e と各分解 e=(c,yc) を扱います。有界な導入のたびに新しい値が環境の先頭に置かれ、対応する s 変数が論理式に必要な対分解の証人を保持します。

            → ⟨ γ ⊨ Cl.clause k ⟩
  clause-in k g q q∈ = bothAll-in i0 (inner4 k) (q ∷ γ) (λ ar F s s∈ ar∈ F∈ eq c c∈ →
    sndAll-in i0 i2 (inner7 k) (c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ p s1 s1∈ p∈ ec →
      sndAll-in i0 (sh  (N k)) (inner9 k) (p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ r s2 s2∈ r∈ ep e e∈ →
        sndAll-in i0 i5 (R.relN (toℕ k)) (e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ) (λ yc s3 s3∈ yc∈ ee →

ホスト側の規則 g を適用する前に、ペイロードの等式を tg k と合成し、タグの枠に格納された集合を正準な数項 #k に書き換えます。したがって規則が受け取るのは、外向きの読み取りに現れる等式 p=(#k,r) そのものです。こうして clause-in と clause-out は、一致する各枠において、第 k 節とその関係の間の二方向を与えます。

          g q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec (ep ∙ cong (λ a → pr a (fst r)) (tg k)) e∈ ee))))

全域性は、切り詰められた存在として外向きに読まれます。符号領域の各要素に対して、全域性の条項が、その第一成分をもつ表の項目の存在を保証し、表の項目の切り詰められた分解が値 yc を復元します。

  total-out : ⟨ γ ⊨ Cl.total ⟩ → (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
  total-out h c c∈ = PT.rec squash₁
    (λ { (e , (e∈ , hs)) → PT.map
      (λ { (yc , s , (ee , _)) → yc , subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ })
      (sndEx-out i0 i1 ⊤̇ (e ∷ c ∷ γ) hs) })

c∈C を固定して仮定 h を c に適用すると、命題的切り詰めの下で、表要素 e、その T への所属、および分解を述べる証明が得られます。読み補題 sndEx-out がさらに e を (c,yc) に分解し、その等式に沿って e の所属を運ぶことで (c,yc)∈T を示します。二段の分解はいずれも切り詰めの内部にとどまるので、結論は存在を与えるだけで、正準な値を選びません。

    (h c c∈)

逆に、C の各 c について、(c,yc) が T に属するような値 yc が命題的に切り詰められて存在すると仮定します。down はその所属の証明を、基礎の集合がその対である T の要素 e : S に実現し、fillSnd は e を c と yc に分解する有界な証人を与えます。残る本体は真なので、このデータから全域性の節を構成できます。値の大域的な選択も一意性の主張も含まれません。

  total-in : ((c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁) → ⟨ γ ⊨ Cl.total ⟩
  total-in g c c∈ = PT.map
    (λ { (yc , m) → down (lookup T γ) (pr (fst c) (fst yc)) m
       , ( m , fillSnd i0 (down (lookup T γ) (pr (fst c) (fst yc)) m ∷ c ∷ γ) c yc refl ⊤̇ (λ b → b) i1 refl ) })
    (g c c∈)

領域条件は、あらかじめ選ばれた対ではなく、T の任意の要素 e から出発します。その外向きの読み取りは、e=(c,yc) かつ c が C に属するような c と yc を、命題的切り詰めの下で復元します。したがって表の各要素の第一成分は指定された領域の符号ですが、分解の正準な選択も、一つの符号が値を一つしか持たないことも述べていません。

  onC-out : ⟨ γ ⊨ Cl.onC ⟩ → (e : S) → ⟨ fst e ∈ Tv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
  onC-out h e e∈ = PT.map (λ { (c , yc , s , (ee , c∈)) → c , yc , (ee , c∈) })
    (bothEx-out i0 (var i1 ∈̇ var (sh  C)) (e ∷ γ) (h e e∈))

逆向きの読み取りは、T の各要素についてまさにこの切り詰められた分解を要求し、それを onC の二つの有界存在量化へ入れます。二方向の読み取りを合わせると、onC は「表の各要素の第一射影が C に属する」という主張に正確に対応します。全域性と組み合わせれば表の領域射影は定まりますが、表が一価の関係になるわけではありません。

  onC-in : ((e : S) → ⟨ fst e ∈ Tv ⟩ → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁)
         → ⟨ γ ⊨ Cl.onC ⟩
  onC-in g e e∈ = PT.rec (snd ((e ∷ γ) ⊨ bothEx i0 (var i1 ∈̇ var (sh  C))))
    (λ { (c , yc , (ee , c∈)) → fillBoth i0 (e ∷ γ) c yc ee (var i1 ∈̇ var (sh  C)) c∈ })
    (g e e∈)

構成子の関係を読む

構成子の読み取りは、元の m 枠の環境の前に十二の枠を加えた環境 δ 上で行われます。したがって元の枠 T と w、および十個の数項の枠 N はこの接頭部の先にあり、枠そのものでは候補値 yc が i0、構成子のペイロード r が i3 に置かれます。この位置を固定することで、どの構成子を読む場合にも同じ外側の枠を使えます。

module RelRead {m : ℕ} (T w : Fin m) (N : Fin  → Fin m) (δ : S ^ ( + m)) where
  private
    module R = Rel T w N
    yc = lookup i0 δ
    r = lookup i3 δ

残る局所名は、環境集合の枠 F とアリティの枠 ar を示します。さらに表の底集合 Tv、アリティの値 A、構成子のペイロード Rv を一度だけ射影しておくことで、後の関係の読み補題が累積階層の中で仮定を直接述べられるようにします。

    F = lookup i8 δ
    ar = lookup i9 δ
    Tv = fst (lookup (sh  T) δ)
    A = fst ar
    Rv = fst r

さらに拡張された任意の局所環境 env に対して、Ext env φ は外側の表の値 yc の正確な外延条件を述べます。要素 z が yc に属するのは、z がアリティに対応する環境集合 F に属し、かつ z を env の新しい先頭枠に置いたときに論理式 φ が成り立つ場合にちょうど限ります。そのため、env の元の枠は φ の内部では一つ後ろの位置から読まれます。

  Ext : ∀ {k} (env : S ^ k) (φ : Formula S ( + k)) → Type (ℓ-suc ℓ)
  Ext env φ = ExtFact (fst yc) (fst F) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)

二項結合子では、ペイロード r が二つの子論理式の符号 a と b に分解されなければなりません。また、鍵 c₁=(A,a) と c₂=(A,b) は、それぞれ表の値 ya と yb を持つ必要があります。これらの仮定から bin-out は、命題的切り詰めの下で五つの補助的な証人を返します。一つは r=(a,b) のコンテナで、各子論理式については T の実際の要素とその分解を示すコンテナです。数学的な結論は外側の値 yc に関する Ext であり、その本体は ya と yb への所属を結合子 op で組み合わせます。

  bin-out : (op : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.binRel op ⟩
          → (a b c₁ ya c₂ yb : S) → Rv ≡ pr (fst a) (fst b)
          → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr A (fst a)
          → ⟨ pr (fst c₂) (fst yb) ∈ Tv ⟩ → fst c₂ ≡ pr A (fst b)
          → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ e₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]

五つの証人をまとめるのは、対象言語の有界量化が各対分解を隠しているためです。ペイロードを開いた後、最初の subAt-out が左の子論理式の鍵における値を読み、二つ目が右の子論理式の鍵における値を読みます。最も内側の extB がそこで yc の正確な外延を与えますが、表がどちらかの子の値を一意に選んだとは述べていません。

              Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op) ∥₁
  bin-out op h a b c₁ ya c₂ yb er m₁ e₁ m₂ e₂ =
    ∣ container r a b er .fst , container e₁S c₁ ya refl .fst , e₁S , container e₂S c₂ yb refl .fst , e₂S ,
      subAt-out (sh  T) i16 i4 (extB i11 i19 (R.binBody op)) δ19
        (subAt-out (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op))) δ15

最初の段階では、十二枠の環境内でペイロードの等式 r=(a,b) を開きます。これにより対のコンテナが加わり、古い枠の前に b、a、そのコンテナを置いた δ15 が得られます。その後、入れ子になった二つの子の値の読み取りが左から右へ進むため、そこで隠される表の証人は外側の命題的切り詰めの内部に保たれます。

          (useBoth i3 δ a b er (subAt (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op)))) h)
          c₁ ya m₁ e₁)
        c₂ yb m₂ e₂ ∣₁
    where
    δ15 : S ^ ( + m)

(c₁,ya) の所属証明そのものは、構造 S の要素を直接与えません。down はそれを、基礎の対が (c₁,ya) である T の実際の要素 e₁S : S として実現します。環境 δ19 はさらに ya、c₁、両者の対のコンテナ、e₁S を δ15 の前に置きます。この四つの枠が、最初の subAt の読み取りが要求する枠に正確に一致します。

    δ15 = b ∷ a ∷ container r a b er .fst ∷ δ
    e₁S : S
    e₁S = down (lookup (sh  T) δ15) (pr (fst c₁) (fst ya)) m₁
    δ19 : S ^ ( + m)
    δ19 = ya ∷ c₁ ∷ container e₁S c₁ ya refl .fst ∷ e₁S ∷ δ15

同じ構成により、二つ目の所属証明は、基礎の対が (c₂,yb) である実際の表の要素 e₂S : S として実現されます。二つ目の subAt-out は δ19 を拡張するときに対応する対のコンテナも与えます。こうして binBody は二つの子の値をともに読めますが、どちらの所属証明も表からの大域的な選択には変えられていません。

    e₂S : S
    e₂S = down (lookup (sh  T) δ19) (pr (fst c₂) (fst yb)) m₂

逆向きの構成は、二項の枠のあらゆる分解に対する規則から始まります。規則は子論理式の符号と値に加えて、ペイロードのコンテナ、二つの実際の表の要素、それぞれの対のコンテナ、および鍵が (A,a) と (A,b) であることを示す等式を受け取ります。その結論は、元の十二枠の前にこれら十一の対象を加えた環境における、外側の値 yc の Ext でなければなりません。

  bin-in : (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
         → ((a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ : S) → Rv ≡ pr (fst a) (fst b)
            → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr A (fst a)
            → ⟨ fst e₂ ∈ Tv ⟩ → fst e₂ ≡ pr (fst c₂) (fst yb) → fst c₂ ≡ pr A (fst b)
            → Ext (yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ) (R.binBody op))

証明は、二つの引数の量化子と関係のコンテナを導入し、左右の表の項目のために、入れ子になった二つの subAt の条項を開いて、それぞれの符号、値、対の等式を導入します。

         → ⟨ δ ⊨ R.binRel op ⟩
  bin-in op g = bothAll-in i3 (subAt (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op)))) δ
    (λ a b s s∈ a∈ b∈ er →
      subAt-in (sh  T) i12 i1 (subAt (sh  T) i16 i4 (extB i11 i19 (R.binBody op))) (b ∷ a ∷ s ∷ δ)
        (λ c₁ ya s₁ e₁ e₁∈ ee₁ e₁' →

最も内側の水準で、ホスト側の規則が十一の対象をすべて受け取り、外延の事実を作ります。それは、最も内側の subAt の条項の中へ運ばれます。導入の入れ子は、量化された節の入れ子と鏡の関係です。

          subAt-in (sh  T) i16 i4 (extB i11 i19 (R.binBody op)) (ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b ∷ a ∷ s ∷ δ)
            (λ c₂ yb s₂ e₂ e₂∈ ee₂ e₂' →
              g a b s c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂')))

非有界量化子では、ペイロード r が子論理式の符号です。対応する子の鍵は c₁=(ar',r) という形で、ar' は外側のアリティ A の後続であり、(c₁,ya) は表に属します。このデータから qu-out は三つの隠れた証人と、外側の値 yc に関する Ext を返します。その外延条件では ya が量化された本体の読む子論理式の充足集合を与えますが、特徴付けられる集合そのものは ya ではありません。

  qu-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j) → ⟨ δ ⊨ R.quRel q ⟩
         → (c₁ ya ar' : S) → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ] Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q) ∥₁
  qu-out q h c₁ ya ar' mem e es =
    ∣ container e'S c₁ ya refl .fst , container c₁ ar' r e .fst , e'S

三つの証人にはそれぞれ異なる役割があります。e'S は対 (c₁,ya) を実現する T の実際の要素で、一方のコンテナはその対を、もう一方は c₁=(ar',r) を証明します。後続アリティに対する一般の読み取りは、これらの証人を ar'=suc A と組み合わせて、最も内側の外延条件を取り出します。

    , subSucAt-out (sh  T) i9 i3 (extB i6 i14 (R.quBody q)) δ h c₁ ya ar' mem e es ∣₁
    where
    e'S : S
    e'S = down (lookup (sh  T) δ) (pr (fst c₁) (fst ya)) mem

逆に、鍵が c₁=(ar',r) と ar'=suc A を満たす実際の表の要素 e'=(c₁,ya) が、二つの対のコンテナのどの選び方に対しても必要な Ext を与えると仮定します。この全称的な前提から quRel の有界な構造を組み直せます。これは対応するすべての項目を扱うもので、子の値 ya の一意性を仮定しません。

  qu-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → ((c₁ ya ar' s s' e' : S) → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') Rv → fst ar' ≡ sucV A
           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s ∷ e' ∷ δ) (R.quBody q))
        → ⟨ δ ⊨ R.quRel q ⟩

非有界量化子では、ペイロード r 自体が子論理式の符号なので、追加のペイロード分解は要りません。したがって、後続アリティの子の値に対する一般の逆向きの読み取りは、quRel が必要とする前提と結論をそのまま持ちます。それを一度適用すれば、対応するすべての表の項目についての全称的な読みを保ったまま、関係全体が再構成されます。

  qu-in q g = subSucAt-in (sh  T) i9 i3 (extB i6 i14 (R.quBody q)) δ g

有界量化子のペイロードには、境界を与える項の符号 t と子論理式の符号 a という二つの構文的成分があり、r=(t,a) です。子の鍵は後続アリティにおける c₁=(ar',a) で、その表の値が ya です。切り詰められた四つの証人は、ペイロードの対、子の表の要素、および関係する二つの対分解を記録します。得られる Ext は外側の値 yc を特徴付け、その本体の中で項の符号が評価され、その値が量化の範囲を制限します。

  bq-out : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
         → (c : ∀ {j} → Formula S j → Formula S j → Formula S j) → ⟨ δ ⊨ R.bqRel q c ⟩
         → (t a c₁ ya ar' : S) → Rv ≡ pr (fst t) (fst a)
         → ⟨ pr (fst c₁) (fst ya) ∈ Tv ⟩ → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A
         → ∥ Σ[ s ∈ S ] Σ[ s₁ ∈ S ] Σ[ s' ∈ S ] Σ[ e' ∈ S ]

証明がまとめる証人は正確に四つです。r=(t,a) のコンテナ、対 (c₁,ya) のコンテナと実際の表の要素、そして c₁=(ar',a) のコンテナです。useBoth がペイロードを開いた後、subSucAt-out が後続アリティにおける子の値を読みます。Ext に渡す環境は十二枠の前に九つの局所的な枠を加え、Ext 自身が候補となる符号化環境 z をさらに一つの先頭枠へ置くので、bqBody のアリティと一致します。

             Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c) ∥₁
  bq-out q c h t a c₁ ya ar' er mem e es =
    ∣ container r t a er .fst , container e'S c₁ ya refl .fst , container c₁ ar' a e .fst , e'S ,
      subSucAt-out (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c)) δ15
        (useBoth i3 δ t a er (subSucAt (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c))) h)

ペイロードを開くと、元の枠の前に三つの枠が加わります。子論理式の符号 a、境界を与える項の符号 t、および r=(t,a) を証明するコンテナです。これが環境 δ15 です。δ がすでに十二の共通枠を含むため、この記法は元の m 枠の環境の前に合計十五の枠があることを表します。

        c₁ ya ar' mem e es ∣₁
    where
    δ15 : S ^ ( + m)
    δ15 = a ∷ t ∷ container r t a er .fst ∷ δ
    e'S : S

仮定 mem は、基礎の対 (c₁,ya) が表の集合に属することを表します。移動後の表の枠で down を適用すると、この証明は必要な基礎の集合を持つ実際の表の要素 e'S : S として実現されます。この実現は証明の局所的なものであり、全域性から子の値を選ぶ操作ではありません。

    e'S = down (lookup (sh  T) δ15) (pr (fst c₁) (fst ya)) mem

逆向きの前提が九つの対象を量化するのは、ペイロードと子の表の分解のあらゆる実現を受け取る必要があるためです。ここで s₁ は表の要素の対コンテナ、s' は後続アリティの子の鍵のコンテナであり、どちらも量化された論理式が束縛する意味論的な証人ではありません。所属の証明と対の等式が与えられると、この前提は yc に関する Ext を与え、有界量化子の関係を局所的に定めます。

  bq-in : (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
        → (c : ∀ {j} → Formula S j → Formula S j → Formula S j)
        → ((t a s c₁ ya ar' s₁ s' e' : S) → Rv ≡ pr (fst t) (fst a)
           → ⟨ fst e' ∈ Tv ⟩ → fst e' ≡ pr (fst c₁) (fst ya)
           → fst c₁ ≡ pr (fst ar') (fst a) → fst ar' ≡ sucV A

bqRel を組み直すため、bothAll-in はまず構成子のペイロードの各分解 r=(t,a) を扱います。その拡張環境で subSucAt-in が子の鍵 (suc A,a) に対するすべての表の項目を扱います。与えられた規則はそこで yc の正確な外延条件を証明します。意味論的な境界値そのものは、後で bqBody の内部で量化され、tmIs によって項の符号 t と結び付けられます。

           → Ext (ar' ∷ s' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a ∷ t ∷ s ∷ δ) (R.bqBody q c))
        → ⟨ δ ⊨ R.bqRel q c ⟩
  bq-in q c g = bothAll-in i3 (subSucAt (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c))) δ
    (λ t a s s∈ t∈ a∈ er →
      subSucAt-in (sh  T) i12 i0 (extB i9 i17 (R.bqBody q c)) (a ∷ t ∷ s ∷ δ)

最も内側の段階では、構造上の義務がすべて明示されています。ペイロードは (t,a)、子の表の要素は (c₁,ya)、その鍵は (ar',a) であり、ar' は A の後続です。これらは仮定した規則 g の前提と正確に一致するため、g の与える外延条件が後続アリティの子の値の節を閉じます。この再構成では ya の一意性をまったく用いません。

        (λ c₁ ya ar' s₁ s' e' e'∈ ee e es → g t a s c₁ ya ar' s₁ s' e' er e'∈ ee e es))

原子論理式では、t と u はペイロードに格納された二つの項の符号であり、それらの意味論的な値ではありません。r=(t,u) を開くと一つの対コンテナが加わり、外側の表の値 yc に関する Ext が残ります。その環境で評価される atomBody は、二つの項の候補値を別に量化し、tmIs で検証してから、選ばれた原子関係を適用します。

  atom-out : (rel : Formula S ( + m)) → ⟨ δ ⊨ R.atomRel rel ⟩
           → (t u : S) → Rv ≡ pr (fst t) (fst u)
           → ∥ Σ[ s ∈ S ] Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel) ∥₁
  atom-out rel h t u er = ∣ container r t u er .fst , useBoth i3 δ t u er (extB i3 i11 (R.atomBody rel)) h ∣₁

逆に、ペイロードを項の符号 t と u に分解するすべての場合と、それに伴うすべての対コンテナについて、必要な外延条件を証明できると仮定します。有界全称の導入がこのペイロード分解を組み直し、原子関係を構成します。項の実際の値に対する存在的な選択は atomBody の内部に残り、atom-in の引数ではありません。

  atom-in : (rel : Formula S ( + m))
          → ((t u s : S) → Rv ≡ pr (fst t) (fst u) → Ext (u ∷ t ∷ s ∷ δ) (R.atomBody rel))
          → ⟨ δ ⊨ R.atomRel rel ⟩
  atom-in rel g = bothAll-in i3 (extB i3 i11 (R.atomBody rel)) δ (λ t u s s∈ t∈ u∈ er → g t u s er)

節から意味論的充足へ橋渡しする

関係の読み出しは完成です。それぞれの構成子の節が外延の事実へ変換され、それぞれの外延の事実が節へ変換されました。本章はここから、これらの対象言語の関係を、メタレベルの充足の意味論へ結ぶ橋に移ります。

open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat; Sat-mem; cond )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
import L.Coding.SatisfactionBridge {ℓ} lem as Semantic
open import Cubical.Data.Nat using ( znots; snotz )

橋のモジュールは、階層の集合 W をパラメータとします。その要素が内部言語の定数のアルファベットをなします。定義可能性と意味論のモジュールが W で開かれ、アルファベット Ab の上の論理式が、W が担う小さなモデルの中で解釈できるようにします。

module Bridge (W : S) where
  open Alphabet W
  private
    module DB = Semantic.DB W
    module Sem = Semantic.SemB W

小モデルの充足判断を ⊨ᴮ、項の値づけを ⟦_⟧ᴮ と改名します。これにより、橋渡しの議論では、この二つを章の前半で使った周囲の階層の充足 ⊨ と区別できます。

    open Sem.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )

論理式 ψ のメタレベルの環境 δ での意味論的な意味は、定数を付け替えた論理式が、W が担う小さなモデルの中で充足されることです。これが、橋が対象言語の表の項目を結びつける目標の意味論です。

    Meaning : ∀ {n} → Formula Ab n → DB.SM ^ n → hProp (ℓ-suc ℓ)
    Meaning ψ δ = δ ⊨ᴮ mapFo DB.ι ψ

基礎の集合 Wv は、小モデルの量化子が走る台です。これを表示 W : S と区別しておくことは、後の橋にとって重要です。対象言語の所属は集合 Wv を使い、構成可能性の証拠は W の第二成分に残ります。したがって橋が量化するのは固定されたモデルの要素であり、すべての構成可能集合ではありません。

  private
    Wv = fst W

対応 toS は、アルファベット Ab の上の論理式のすべての定数を、構造 S の対応する定数へ付け替え、周囲の充足で判定できる S の上の論理式を作ります。

  toS : ∀ {n} → Formula Ab n → Formula S n
  toS = mapFo (asConst W)

構成可能な充足集合 SatW ψ は、付け替えられた論理式を満たす符号化された環境を集めます。それは充足を定義する内部の再帰の出力なので、L の要素です。

  SatW : ∀ {n} → Formula Ab n → S
  SatW ψ = Sat W (toS ψ)

SatW ψ への所属の外向きの読み出しは、内部の充足の所属の仕様から従います。SatW ψ の要素は、正しいアリティの環境の集合に属し、付け替えられた論理式の条件を満たす、符号化された環境です。

  Sat-out : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (SatW ψ) ⟩
          → ⟨ fst z ∈ fst (envSet W n) ⟩ × ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩
  Sat-out ψ z h = subst ⟨_⟩ (Sat-mem W (toS ψ) z) h

内向きの方向は、正しい環境集合への所属と再帰条件という二つの事実から出発し、その対を Sat-mem に沿って逆向きに輸送することで SatW ψ への所属を得ます。したがって Sat-out と Sat-in は、所属の仕様が与えるパスに沿う二方向の輸送そのものであり、追加の意味論的仮定を必要としません。

  Sat-in : ∀ {n} (ψ : Formula Ab n) (z : S) → ⟨ fst z ∈ fst (envSet W n) ⟩
         → ⟨ (z ∷ []) ⊨ cond W (toS ψ) ⟩ → ⟨ fst z ∈ fst (SatW ψ) ⟩
  Sat-in ψ z hz hc = subst ⟨_⟩ (sym (Sat-mem W (toS ψ) z)) (hz , hc)

補題 extension-path は、各点における真理値のパスを SatW ψ の正確な外延定理へ変えます。符号化された各環境 z について、その前提は再帰条件 cond W (toS ψ) を目標命題 P z と同定します。Sat-mem の二方向を用いると、結論は SatW ψ の要素が、P を満たす envSet W n の要素にちょうど一致すると述べます。ここでは z を復号せず、環境ベクトルの代表も選びません。

  private
    extension-path : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
                   → ((z : S) → ((z ∷ []) ⊨ cond W (toS ψ)) ≡ P z)
                   → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)
    extension-path ψ P e =

外向きの方向は、Sat-out を通して SatW ψ への所属の二つの成分を読み、各点の等式に沿って条件を運びます。内向きの方向は、性質を運び戻して Sat-in を適用します。どちらの方向も、代表を選ぶことなく、各点の等式だけを使います。

        (λ z hz → Sat-out ψ z hz .fst , subst ⟨_⟩ (e z) (Sat-out ψ z hz .snd))
      , (λ z hz hp → Sat-in ψ z hz (subst ⟨_⟩ (sym (e z)) hp))

偽の場合、目標の性質はどの z に対しても要素を持ちません。もし z が SatW ⊥̇ に属すれば、Sat-out は不可能な偽の充足を取り出します。逆に、その不可能な性質の証明を仮定すれば、候補は直ちに除去できます。残る成分は、仮に要素があれば正しいアリティを持つことを記録するだけなので、botBridge は envSet W n の内部で空の外延を与えます。

  botBridge : (n : ℕ) {k : ℕ} (env : S ^ k)
            → ExtFact (fst (SatW (⊥̇ {n = n}))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ ⊥̇ ⟩)
  botBridge n env = (λ z hz → Sat-out ⊥̇ z hz .fst , Sat-out ⊥̇ z hz .snd) , (λ z hz b → Empty.rec* b)

env の枠 ya と yb が、それぞれ a と b の充足集合の基礎の集合を持つと仮定します。連言の橋は SatW (a ∧̇ b) を、二つの子の充足集合の両方に属する符号化環境 z として特徴付けます。本体を評価する前に z が環境の先頭へ加えられるため、元の枠は suc ya と suc yb で参照され、i0 が z を指します。この移動が、表示された論理式に記録されたホスト側の Fin 境界です。

  andBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ∧̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)) ⟩)
  andBridge a b env ya yb qa qb = extension-path (a ∧̇ b)

連言では、点ごとのパスが同じ候補環境 z の二つの記述を比較します。再帰条件は z が SatW a と SatW b の両方に属すことを述べ、二つの所属を qa と qb に沿って輸送すると、節の本体にある二つの対象言語の所属原子がちょうど得られます。この段階では子環境を復号しません。

    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∧̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊓ (fst z ∈ sym qb i))

選言の橋渡しは正確な外延記述を与えます。ある環境が SatW (a ∨̇ b) に属すのは、それが envSet W n に属し、さらに節の環境の先頭に置いたとき、a の値または b の値に属すという対象言語の選言を満たすとき、そのときに限ります。

  orBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
           → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
           → ExtFact (fst (SatW (a ∨̇ b))) (fst (envSet W n))
               (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)) ⟩)
  orBridge a b env ya yb qa qb = extension-path (a ∨̇ b)

選言の点ごとの比較は、同じ z の所属を二つのスロット等式に沿って輸送します。二つの選択肢は z の SatW a への所属と SatW b への所属であり、対象言語の選言はこの選択を正確に記録します。ここで別の環境の証人が作られることはありません。

    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ∨̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⊔ (fst z ∈ sym qb i))

含意の橋渡しも、環境集合の内部で SatW (a ⇒̇ b) を特徴づけます。候補環境 z における節の本体は、z が前件の値に属すならば、同じ z が後件の値に属すと述べます。

  impBridge : ∀ {n} (a b : Formula Ab n) {k : ℕ} (env : S ^ k) (ya yb : Fin k)
            → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
            → ExtFact (fst (SatW (a ⇒̇ b))) (fst (envSet W n))
                (λ z → ⟨ (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)) ⟩)
  impBridge a b env ya yb qa qb = extension-path (a ⇒̇ b)

ここで必要なのは点ごとのパスです。qa と qb は前件と後件の値のスロットをそれぞれ SatW a と SatW b と同定します。これらの等式に沿って輸送すると、対象言語の含意は含意の再帰条件となり、環境そのものは変わりません。

    (λ z → (z ∷ env) ⊨ (var i0 ∈̇ var (suc ya)) ⇒̇ (var i0 ∈̇ var (suc yb)))
    (λ z i → (fst z ∈ sym qa i) ⇒ (fst z ∈ sym qb i))

二つの非有界量化子の本体は、まず wi が名指す台の上で量化します。存在の本体は台のある要素 x を求め、全称の本体はそのようなすべての x を扱います。どちらの場合も内側の有界存在が子論理式の値から項目を取り、それが x を古い環境の先頭に加えて得られるグラフであることを要求します。

  quEx quAll : ∀ {k} → Fin k → Fin k → Formula S ( + k)
  quEx wi yai = ∃̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))
  quAll wi yai = ∀̇∈ (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2))

補題 direct-extension は、量化子と原子の橋渡しに共通する議論を取り出します。z がベクトル δ のグラフと同定されたなら、Meaning ψ δ と節が表す性質 P z の間の両方向の写像を仮定し、SatW ψ が envSet W n のうち P を満たす部分にちょうど等しいことを示します。δ の復元は終始切り詰めの内側に保たれます。

  private
    direct-extension : ∀ {n} (ψ : Formula Ab n) (P : S → hProp (ℓ-suc ℓ))
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ Meaning ψ δ ⟩ → ⟨ P z ⟩)
      → ((δ : DB.SM ^ n) (z : S) → fst z ≡ Semantic.graph W δ → ⟨ P z ⟩ → ⟨ Meaning ψ δ ⟩)
      → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ P z ⟩)