閉じた符号の定義域の健全性と完全性

module CodesSem (Wv Cv : V ℓ) where

AtomP BinP ConP QuP BqP : V ℓ → V ℓ → Type (ℓ-suc ℓ)
AtomP ar r = ∥ Σ[ t ∶ V ℓ ] Σ[ u ∶ V ℓ ] ((r ≡ pr t u) × (IsTmV Wv t ar × IsTmV Wv u ar)) ∥₁
BinP ar r = ∥ Σ[ a ∶ V ℓ ] Σ[ b ∶ V ℓ ] ((r ≡ pr a b) × (⟨ pr ar a ∈ Cv ⟩ × ⟨ pr ar b ∈ Cv ⟩)) ∥₁
ConP ar r = r ≡ # 

量化子のペイロードで一覧が完成する。非有界量化子のペイロードは、後続アリティにある下位キーである。有界量化子のペイロードは、現在のアリティで正当な項符号と、そのような下位キーとの対である。この非対称性は文法そのものに由来する。本体は後続アリティをもち、境界を表す項は量化された論理式と同じアリティをもつ。

QuP ar r = ⟨ pr (sucV ar) r ∈ Cv ⟩
BqP ar r = ∥ Σ[ t ∶ V ℓ ] Σ[ a ∶ V ℓ ] ((r ≡ pr t a) × (IsTmV Wv t ar × ⟨ pr (sucV ar) a ∈ Cv ⟩)) ∥₁

ペイロードの表はここからはじまる。タグ零と一が二つの原子の形を、タグ二と三が連言と選言の二項の形を担う。

PayN : ℕ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
PayN  = AtomP
PayN  = AtomP
PayN  = BinP
PayN  = BinP

表は続き、タグ四が含意、タグ五が定数の偽、タグ六と七が二つの非有界量化子、タグ八が有界の全称を担う。

PayN  = BinP
PayN  = ConP
PayN  = QuP
PayN  = QuP
PayN  = BqP

タグ九は有界存在量化子のペイロードを担う。補助族 PayN は十以上の自然数では空型であるが、正当な Key のタグは Fin 10 から選ばれる。したがって、キーに現れうるのは零から九までの十種類だけである。

PayN  = BqP
PayN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) _ _ = ⊥*

アリティ ar でのキーとは、単に、十のタグの一つと、それに合った形のペイロードのことである。キーが何でないかに注意してほしい。キーは帰納的な構文木ではなく、その分解が一意なデータだとも主張していない。キーとは、集合として符号化された対が、既知の十の形のどれかに分解されるという、切り詰められた証拠なのである。

Key : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Key ar p = ∥ Σ[ k ∶ Fin  ] Σ[ r ∶ V ℓ ] ((p ≡ pr (# (toℕ k)) r) × PayN (toℕ k) ar r) ∥₁

module _ {k : ℕ} (t ar w N0 N1 : Fin k) (δ : Vec S k)
  (q0 : (lookup N0 δ) .fst ≡ # ) (q1 : (lookup N1 δ) .fst ≡ # ) where

private
  Wv = (lookup w δ) .fst

外向きの読み出しは、対象言語の論理式の切り詰められた選言を消去する。定数の分岐では、存在量化が対の第二成分を取り出し、数項の等式がタグを揃え、所属が IsTmV へ入る。結果は、切り詰められた定義の左の分岐である。

isTm-out : ⟨ δ ⊨ isTm t ar w N0 N1 ⟩ → IsTmV Wv ((lookup t δ) .fst) ((lookup ar δ) .fst)
isTm-out = rec₁ squash₁
  (λ { (inl h) → map₁
         (λ { (v , s , (e , v∈)) → inl (v .fst , (e ∙ cong (λ a → pr a (v .fst)) q0 , v∈)) })
         (sndEx-out t N0 (var i0 ∈̇ var (sh  w)) δ h)

変数の分岐は、数項一とアリティの集合で同じ三歩を繰り返し、右の分岐を作る。二つの分岐合わせて、対象言語の認識と、集合レベルの IsTmV がまさに同値であることが言える。

     ; (inr h) → map₁
         (λ { (v , s , (e , v∈)) → inr (v .fst , (e ∙ cong (λ a → pr a (v .fst)) q1 , v∈)) })
         (sndEx-out t N1 (var i0 ∈̇ var (sh  ar)) δ h) })

内向きの読み出しは、同じ変換を逆向きに行う。定数の分岐では、充填の補題が証人 x を枠零の存在量化子の下に置き、対の等式が逆向きの数項の等式に沿って運ばれて、充足が対象言語の論理式の形と一致するようにする。

isTm-in : IsTmV Wv ((lookup t δ) .fst) ((lookup ar δ) .fst) → ⟨ δ ⊨ isTm t ar w N0 N1 ⟩
isTm-in = rec₁ ((δ ⊨ isTm t ar w N0 N1) .snd)
  (λ { (inl (x , (e , x∈))) →
         ∣ inl (fillSnd t δ (lookup N0 δ) (down (lookup w δ) x x∈)
                  (e ∙ cong (λ a → pr a x) (sym q0)) (var i0 ∈̇ var (sh  w)) x∈ N0 refl) ∣₁

変数の分岐は、数項一の枠の存在量化子の下に証人 i を満たし、対応する逆向きの等式に沿って運ぶ。二つの分岐が、この同値を両方向で閉じる。

     ; (inr (i , (e , i∈))) →
         ∣ inr (fillSnd t δ (lookup N1 δ) (down (lookup ar δ) i i∈)
                  (e ∙ cong (λ a → pr a i) (sym q1)) (var i0 ∈̇ var (sh  ar)) i∈ N1 refl) ∣₁ })

module _ {k : ℕ} (C ar r : Fin k) (δ : Vec S k) where

keyUp-out : ⟨ δ ⊨ keyUp C ar r ⟩ → ⟨ pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst) ∈ (lookup C δ) .fst ⟩
keyUp-out = rec₁ ((pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst) ∈ (lookup C δ) .fst) .snd)
  (λ { (c' , (c'∈ , h)) → rec₁ ((pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst) ∈ (lookup C δ) .fst) .snd)
    (λ { (s , (s∈ , h')) → rec₁ ((pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst) ∈ (lookup C δ) .fst) .snd)

外向きには、対の論理式が選ばれた C の要素を (ar',r) と同一視し、後続の論理式が ar' を suc ar と同一視する。この二つの等式に沿って所属を移すと、(suc ar,r) ∈ C が得られる。切り詰められた証人はすべて、この所属命題へのみ消去される。

      (λ { (ar' , (ar'∈ , (e , hs))) →
        subst (λ u → ⟨ u ∈ (lookup C δ) .fst ⟩)
          (pr-out i2 i0 (sh  r) (ar' ∷ s ∷ c' ∷ δ) e
           ∙ cong (λ a → pr a ((lookup r δ) .fst)) (suc-out (sh  ar) i0 (ar' ∷ s ∷ c' ∷ δ) hs))
          c'∈ })

したがって、三層の有界な証人は、表示された対象が C の要素であることを確かめるためだけに使われる。その切り詰めを消去した結果、keyUp-out は外部の所属 (suc ar,r) ∈ C をちょうど与える。

      h' })
    h })

内向きには、(suc ar,r) ∈ C から始める。後続アリティを構成可能集合として提示し、それと r の順序対をまとめ、これらを三つの有界な証人として使う。すると、対と後続の論理式から keyUp C ar r の充足が再構成される。

keyUp-in : ⟨ pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst) ∈ (lookup C δ) .fst ⟩ → ⟨ δ ⊨ keyUp C ar r ⟩
keyUp-in h = ∣ c' , (h , ∣ c .fst , (c .snd .fst , ∣ ar' , (c .snd .snd .fst
  , ( pr-in i2 i0 (sh  r) (ar' ∷ c .fst ∷ c' ∷ δ) (sym (cong (λ a → pr a ((lookup r δ) .fst)) (sucʟ-fst (lookup ar δ))))
    , suc-in (sh  ar) i0 (ar' ∷ c .fst ∷ c' ∷ δ) (sucʟ-fst (lookup ar δ)) )) ∣₁) ∣₁) ∣₁
  where

具体的には、ar' が suc ar を表し、c' が C の要素 (suc ar,r) を表す。さらに c' とともに与えられる包含集合が、論理式で使う有界所属の鎖を証する。それぞれの基礎集合の等式により、内部の証人が意図した外部の対を表すことが保証される。

  ar' : S
  ar' = sucʟ (lookup ar δ)
  c' : S
  c' = down (lookup C δ) (pr (sucV ((lookup ar δ) .fst)) ((lookup r δ) .fst)) h
  c = container c' ar' (lookup r δ) (cong (λ a → pr a ((lookup r δ) .fst)) (sym (sucʟ-fst (lookup ar δ))))

module _ {k : ℕ} (C ar N a : Fin k) (δ : Vec S k) where

private
  Cv = (lookup C δ) .fst
  A = (lookup ar δ) .fst
  Nv = (lookup N δ) .fst

unKey の外向きの読みは、入れ子のキー (A,(N,a)) が C に属することを正確に述べる。順序対の式の妥当性により、対象言語の所属は、ホスト側のこの集合所属へ変換される。

unKey-out : ⟨ δ ⊨ unKey C ar N a ⟩ → ⟨ pr A (pr Nv ((lookup a δ) .fst)) ∈ Cv ⟩
unKey-out = E.member-out (keyExpr ar N (E.slot a)) (var C) δ

妥当性は逆向きにも使える。所属 (A,(N,a)) ∈ C から、対象言語の述語 unKey の充足が得られる。したがって、キーの条項とホスト側での読みは、双方向に一致する。

unKey-in : ⟨ pr A (pr Nv ((lookup a δ) .fst)) ∈ Cv ⟩ → ⟨ δ ⊨ unKey C ar N a ⟩
unKey-in = E.member-in (keyExpr ar N (E.slot a)) (var C) δ

module _ {k : ℕ} (C ar N a b : Fin k) (δ : Vec S k) where

private
  Cv = (lookup C δ) .fst
  A = (lookup ar δ) .fst
  Nv = (lookup N δ) .fst

二つの引数の値から順序対 P = (a,b) を作る。この対が、入れ子の二項キー (A,(N,P)) のペイロードである。

  P = pr ((lookup a δ) .fst) ((lookup b δ) .fst)

binKey の外向きの読みは、所属 (A,(N,(a,b))) ∈ C にほかならない。この形は、アリティ、構成子タグ、対にした引数という符号化の三つの論理的な層を保つ。

binKey-out : ⟨ δ ⊨ binKey C ar N a b ⟩ → ⟨ pr A (pr Nv P) ∈ Cv ⟩
binKey-out = E.member-out (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

内向きの読み出しはその逆向きであり、他のキーの条項と同じく、二者は論理式の主張と集合の所属を同一視する。

binKey-in : ⟨ pr A (pr Nv P) ∈ Cv ⟩ → ⟨ δ ⊨ binKey C ar N a b ⟩
binKey-in = E.member-in (keyExpr ar N (E.pair (E.slot a) (E.slot b))) (var C) δ

module _ {k : ℕ} (C ar N Nx x Ny y : Fin k) (δ : Vec S k) where

private
  Cv = (lookup C δ) .fst
  A = (lookup ar δ) .fst
  Nv = (lookup N δ) .fst

二つの項符号を T=(Nx,x)、U=(Ny,y) と書く。この段階では Nx と Ny は環境から得た任意のタグ値であり、それらが零または一であるという条件は、原子の閉性の場合を具体化するときに課される。

  T = pr ((lookup Nx δ) .fst) ((lookup x δ) .fst)
  U = pr ((lookup Ny δ) .fst) ((lookup y δ) .fst)

原子の条件を外向きに読むと、(A,(N,(T,U))) ∈ C となる。ここで T と U は二つの項符号である。最も外側の対がアリティを、その次が原子タグを、最も内側の対が二つの項を記録する。

atomKey-out : ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩ → ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩
atomKey-out = E.member-out (atomKeyExpr ar N Nx x Ny y) (var C) δ

内向きの読み出しはその逆向きで、これまでのどのキーの条項と同じく、原子の場合を両方向で閉じる。

atomKey-in : ⟨ pr A (pr Nv (pr T U)) ∈ Cv ⟩ → ⟨ δ ⊨ atomKey C ar N Nx x Ny y ⟩
atomKey-in = E.member-in (atomKeyExpr ar N Nx x Ny y) (var C) δ

module _ {k : ℕ} (C ar N Nx x a : Fin k) (δ : Vec S k) where

private
  Cv = (lookup C δ) .fst
  A = (lookup ar δ) .fst
  Nv = (lookup N δ) .fst

境界項の符号を T=(Nx,x)、本体の符号を Av と書く。項は現在のアリティで検査され、本体のキーは後続アリティで検査される。両者を別々のペイロード成分として保つことで、この文法上の非対称が記録される。

  T = pr ((lookup Nx δ) .fst) ((lookup x δ) .fst)
  Av = (lookup a δ) .fst

有界キーの条件を外向きに読むと、(A,(N,(T,Av))) ∈ C となる。最も内側の対には、境界項の符号と本体の符号がこの順で入る。この所属だけでは、どちらの成分が正当であることもまだ主張しない。

bndKey-out : ⟨ δ ⊨ bndKey C ar N Nx x a ⟩ → ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩
bndKey-out = E.member-out (bndKeyExpr ar N Nx x a) (var C) δ

逆に、(A,(N,(T,Av))) が C に属することから bndKey の充足が得られる。二方向の読みが確立するのは構造的な所属の同値だけである。T の正当性と、後続アリティにおける Av の所属は、周囲のペイロード述語が別に与える。

bndKey-in : ⟨ pr A (pr Nv (pr T Av)) ∈ Cv ⟩ → ⟨ δ ⊨ bndKey C ar N Nx x a ⟩
bndKey-in = E.member-in (bndKeyExpr ar N Nx x a) (var C) δ

module PayRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : Vec S ( + m))
  (tg : Tags δ (shN  N)) where

private
  Cv = (lookup (sh  C) δ) .fst
  Wv = (lookup (sh  w) δ) .fst

各ペイロードの読みでは、A が記録されたアリティを、R が生のペイロードを表す。タグ零と一の等式を取り出しておくのは、原子と有界量化子のペイロードがともに項符号を認識する必要があり、項の二つの正当な形がちょうどこの二タグを使うからである。

  A = (lookup i5 δ) .fst
  R = (lookup i0 δ) .fst
  q0 = tg f0
  q1 = tg f1
  rS = lookup i0 δ

比較の両側では、同じ基礎集合 Wv と Cv を使う。したがって、構文的なペイロード論理式が述べる Wv への項の所属と Cv への部分キーの所属は、五つの外部ペイロード述語のパラメータと正確に一致する。

  module Sh = Shape C w N
open CodesSem Wv Cv

原子の本体は、ペイロードの二成分がともに、記録されたアリティで項符号の述語を満たすことを要求する。これに対して二項の本体は、両成分が同じアリティのキーとして候補領域に現れることを要求する。どちらのペイロードも対として符号化されるが、二つの条件は異なる。

private
  tmBody : Formula S ( + m)
  tmBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ isTm i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1))
  binBody : Formula S ( + m)
  binBody = appAt (sh  C) i8 i1 ∧̇ appAt (sh  C) i8 i0

最後のペイロード形は二つの有界量化子を扱う。その本体は、境界を表す項が現在のアリティで合法であることと、本体のキーが後続アリティで符号集合に属することを要求する。

  bqBody : Formula S ( + m)
  bqBody = isTm i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) ∧̇ keyUp (sh  C) i8 i0

原子ペイロードを外向きに読むと、二つの存在束縛が除かれ、項 t と u、等式 R ≡ pr t u、および両方の項がアリティ A で合法であることの証明が得られる。項の読みは 0 と 1 のタグ等式を用いて、二つの充足証明を対応する切り詰められた項の形へ変換する。

atom-out : ⟨ δ ⊨ Sh.atomPay ⟩ → AtomP A R
atom-out h = map₁
  (λ { (t , u , s , (e , (ht , hu))) → t .fst , u .fst
     , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 ht
             , isTm-out i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (u ∷ t ∷ s ∷ δ) q0 q1 hu ) ) })

この消費は、二重の存在消去の一つの適用にすぎない。証人 t、u と容器を取り出し、残りの連言をペイロードのデータへ処理する。

  (bothEx-out i0 tmBody δ h)

内向きの読みは、データから充足を組み立て直す。切り詰められた合法性の証明は、目標もまた切り詰められた充足であるため消去でき、二つの項はそれぞれずらした文脈を通して合法性の原子に入る。

atom-in : AtomP A R → ⟨ δ ⊨ Sh.atomPay ⟩
atom-in = rec₁ ((δ ⊨ Sh.atomPay) .snd)
  (λ { (t , u , (e , (ht , hu))) →
    fillBoth i0 δ (fstS rS t u e) (sndS rS t u e) e tmBody
      ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 ht

二つ目の合法性の証明も同じ方法で入れる。補助環境 δ12 は、R ≡ pr t u によって選ばれた二つの成分、その対を証明するコンテナ、元の環境からなり、二つの項の原子式はまさにこの環境で解釈される。

      , isTm-in i0 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t u e) q0 q1 hu ) })
  where
  δ12 : (t u : V ℓ) (e : R ≡ pr t u) → Vec S ( + m)
  δ12 t u e = sndS rS t u e ∷ fstS rS t u e ∷ container rS (fstS rS t u e) (sndS rS t u e) e .fst ∷ δ

二項ペイロードを外向きに読むと、ペイロード a と b、等式 R ≡ pr a b、および pr A a と pr A b がともに符号集合に属することが得られる。二つの適用原子式の妥当性が、拡張環境におけるこれらの所属を同定する。

bin-out : ⟨ δ ⊨ Sh.binPay ⟩ → BinP A R
bin-out h = map₁
  (λ { (a , b , s , (e , (ha , hb))) → a .fst , b .fst
     , ( e , ( subst ⟨_⟩ (appAt-adequate (sh  C) i8 i1 (b ∷ a ∷ s ∷ δ)) ha
             , subst ⟨_⟩ (appAt-adequate (sh  C) i8 i0 (b ∷ a ∷ s ∷ δ)) hb ) ) })

原子の場合と同じく、二項の条件の二重の存在量化は一度の消去で処理される。

  (bothEx-out i0 binBody δ h)

内向きの読みは、名指された下位コードで二つの存在量化子を満たす。二つの適用の原子は、妥当性を逆向きに辿ってずらした文脈の中で充足される。

bin-in : BinP A R → ⟨ δ ⊨ Sh.binPay ⟩
bin-in = rec₁ ((δ ⊨ Sh.binPay) .snd)
  (λ { (a , b , (e , (ha , hb))) →
    fillBoth i0 δ (fstS rS a b e) (sndS rS a b e) e binBody
      ( subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i1 (δ12 a b e))) ha

二項の場合の補助定義も同じずらした文脈の形を記録する。今度は周囲の値 a と b から組み立てられる。

      , subst ⟨_⟩ (sym (appAt-adequate (sh  C) i8 i0 (δ12 a b e))) hb ) })
  where
  δ12 : (a b : V ℓ) (e : R ≡ pr a b) → Vec S ( + m)
  δ12 a b e = sndS rS a b e ∷ fstS rS a b e ∷ container rS (fstS rS a b e) (sndS rS a b e) e .fst ∷ δ

偽のペイロードには下位データがない。その論理式は R が 0 タグのスロットに格納された値に等しいことを述べ、ConP A R は R ≡ # 0 を述べる。0 タグの等式と合成することで外向きの方向が得られる。

con-out : ⟨ δ ⊨ Sh.conPay ⟩ → ConP A R
con-out h = h ∙ q0

逆に、等式 R ≡ # 0 を 0 タグの等式の逆向きと合成すると、R が 0 タグのスロットの値に等しいことが示される。これは偽のペイロードの充足そのものである。

con-in : ConP A R → ⟨ δ ⊨ Sh.conPay ⟩
con-in h = h ∙ sym q0

どちらの非有界量化子でも、ペイロードは後続アリティにおける本体のキーである。後続キーの読みは、このペイロード論理式の充足を pr (sucV A) R が符号集合に属することへ変換する。

qu-out : ⟨ δ ⊨ Sh.quPay ⟩ → QuP A R
qu-out = keyUp-out (sh  C) i5 i0 δ

逆向きには、pr (sucV A) R が符号集合に属することから後続キーの論理式に必要な証人が得られ、量化子ペイロードが証明される。

qu-in : QuP A R → ⟨ δ ⊨ Sh.quPay ⟩
qu-in = keyUp-in (sh  C) i5 i0 δ

有界量化子のペイロードを外向きに読むと、項 t、本体のペイロード a、等式 R ≡ pr t a が得られる。さらに、t がアリティ A で合法であることと、本体のキー pr (sucV A) a が符号集合に属することも得られる。

bq-out : ⟨ δ ⊨ Sh.bqPay ⟩ → BqP A R
bq-out h = map₁
  (λ { (t , a , s , (e , (ht , ha))) → t .fst , a .fst
     , ( e , ( isTm-out i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (a ∷ t ∷ s ∷ δ) q0 q1 ht
             , keyUp-out (sh  C) i8 i0 (a ∷ t ∷ s ∷ δ) ha ) ) })

有界の本体の二重の存在量化は、他の場所と同じく二重の消去で処理される。

  (bothEx-out i0 bqBody δ h)

内向きの読みでは、境界の項がずらした文脈を通して合法性の原子に入る。

bq-in : BqP A R → ⟨ δ ⊨ Sh.bqPay ⟩
bq-in = rec₁ ((δ ⊨ Sh.bqPay) .snd)
  (λ { (t , a , (e , (ht , ha))) →
    fillBoth i0 δ (fstS rS t a e) (sndS rS t a e) e bqBody
      ( isTm-in i1 i8 (sh  w) (sh  (N f0)) (sh  (N f1)) (δ12 t a e) q0 q1 ht

本体の鍵は後続の鍵の補題を通して入り、補助定義は境界の値とその容器から作られるずらした文脈の形を記録する。

      , keyUp-in (sh  C) i8 i0 (δ12 t a e) ha ) })
  where
  δ12 : (t a : V ℓ) (e : R ≡ pr t a) → Vec S ( + m)
  δ12 t a e = sndS rS t a e ∷ fstS rS t a e ∷ container rS (fstS rS t a e) (sndS rS t a e) e .fst ∷ δ

タグの読みはタグの上の再帰で選ばれる。タグ 0 と 1 が二つの原子式、タグ 2、3、4 が三つの二項結合子である。

payN-out : (k : ℕ) → ⟨ δ ⊨ Sh.payN k ⟩ → PayN k A R
payN-out  = atom-out
payN-out  = atom-out
payN-out  = bin-out
payN-out  = bin-out

タグ 5、6、7 は偽と二つの非有界の量化子を、タグ 8 は有界の全称を担う。

payN-out  = bin-out
payN-out  = con-out
payN-out  = qu-out
payN-out  = qu-out
payN-out  = bq-out

タグ 9 が有界の存在である。タグ 10 以上は構成子を名指さないためペイロードは空であり、読みはその空のデータの上の恒等写像である。

payN-out  = bq-out
payN-out (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

内向きの読みも同じ再帰で選ばれ、タグごとに一つの節をもつ。

payN-in : (k : ℕ) → PayN k A R → ⟨ δ ⊨ Sh.payN k ⟩
payN-in  = atom-in
payN-in  = atom-in
payN-in  = bin-in
payN-in  = bin-in

タグ 4 から 7 までが一覧を続ける。最後の二項結合子、偽、そして二つの非有界の量化子である。

payN-in  = bin-in
payN-in  = con-in
payN-in  = qu-in
payN-in  = qu-in
payN-in  = bq-in

タグ 9 が一覧を完成させる。10 以上を読むべきものはない。そのようなタグをもつ合法な鍵はないからである。

payN-in  = bq-in
payN-in (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) h = h

module TenRead {m : ℕ} (C w : Fin m) (N : Fin  → Fin m) (δ : Vec S ( + m))
  (tg : Tags δ (shN  N)) where

private
  Cv = (lookup (sh  C) δ) .fst
  Wv = (lookup (sh  w) δ) .fst

新たに束縛された項目のうち、A はアリティであり、P はキーとして認識すべきタグ付きペイロードである。P の集合レベルの表示を保つことで、タグとそのペイロード r を選んだときに等式 P ≡ pr (# (toℕ j)) r を実現できる。

  A = (lookup i3 δ) .fst
  P = (lookup i0 δ) .fst
  pS = lookup i0 δ
  module Sh = Shape C w N
open CodesSem Wv Cv

タグの読みは、j 番目のタグの原子の充足を鍵へ変換する。切り詰められた証人は添字 r と容器の対であり、符号化の等式は、j 番目のタグのスロットが j の数項を名指すというタグの等式に沿って輸送され、ペイロードはタグ j での読みによって読まれる。

at-out : (j : Fin ) → ⟨ δ ⊨ Sh.at j ⟩ → Key A P
at-out j h = map₁
  (λ { (r , s , (e , hp)) → j , r .fst
     , ( e ∙ cong (λ a → pr a (r .fst)) (tg j)
       , PayRead.payN-out C w N (r ∷ s ∷ δ) tg (toℕ j) hp ) })

タグの原子の二重の存在量化はみずからの消去で処理されるため、読みが添字を選ぶことはない。充足が与える一つを展開するだけである。

  (sndEx-out i0 (sh  (N j)) (Sh.pay j) δ h)

内向きの方向は、鍵から充足を組み立てる。証人の項目はずらした値で満たされ、ペイロードは拡張された文脈の上で内向きに読まれ、タグの等式が名指しのスロットを j の数項と同一視する。

at-in : (j : Fin ) (r : V ℓ) (e : P ≡ pr (# (toℕ j)) r) → PayN (toℕ j) A r → ⟨ δ ⊨ Sh.at j ⟩
at-in j r e pay =
  fillSnd i0 δ (lookup (sh  (N j)) δ) rS e' (Sh.pay j)
    (PayRead.payN-in C w N (rS ∷ container pS (lookup (sh  (N j)) δ) rS e' .fst ∷ δ) tg (toℕ j) pay)
    (sh  (N j)) refl

改名された値は j の数項と選ばれた項目を対にし、符号化の等式はタグの等式と逆向きに合成されて、拡張された名指しが正しいスロットに触れるようにする。

  where
  rS : S
  rS = sndS pS (# (toℕ j)) r e
  e' : P ≡ pr ((lookup (sh  (N j)) δ) .fst) (rS .fst)
  e' = e ∙ cong (λ a → pr a r) (sym (tg j))

十通りの外向きの読みは選言を消費し、証人が名指すタグのところでタグの読みを引用する。

ten-out : ⟨ δ ⊨ Sh.ten ⟩ → Key A P
ten-out h = rec₁ squash₁ (λ { (j , hj) → at-out j hj }) (bigOr-out δ  Sh.at h)

内向きの読みは、証人の現れたタグで選言に入り、ペイロードもそのタグで内向きに読まれる。二つの方向合わせて、十通りの選言の充足と、合法な鍵をもつことは同じことだと述べている。

ten-in : Key A P → ⟨ δ ⊨ Sh.ten ⟩
ten-in = rec₁ ((δ ⊨ Sh.ten) .snd)
  (λ { (j , r , (e , pay)) → bigOr-in δ  Sh.at j (at-in j r e pay) })

module ShapeRead {m : ℕ} (C w E : Fin m) (N : Fin  → Fin m) (γ : Vec S m) (tg : Tags γ N) where

private
  Cv = (lookup C γ) .fst
  Wv = (lookup w γ) .fst
  Ev = (lookup E γ) .fst

選ばれた要素 c と塔の証人 (ar,F) に対し、残りの論理式はペイロード p を選び、c ≡ pr ar p を要求し、十通りのタグ形に照らして p を検査する。このように、入れ子になった証人は外側のアリティと内側のタグ付きペイロードを別々に明らかにする。

  module Sh = Shape C w N
  inner : Formula S ( + m)
  inner = sndEx i4 i1 Sh.ten
open CodesSem Wv Cv

Shaped c は形の節から取り出されるデータをそのまま記録する。pr ar F が E に属し、c ≡ pr ar p が成り立ち、p がアリティ ar における合法なタグ付きペイロードとなる ar、F、p が存在する。この存在データはすべて命題的に切り詰められており、分解の一意性は主張しない。

Shaped : V ℓ → Type (ℓ-suc ℓ)
Shaped c = ∥ Σ[ ar ∶ V ℓ ] Σ[ F ∶ V ℓ ] Σ[ p ∶ V ℓ ]
             (⟨ pr ar F ∈ Ev ⟩ × ((c ≡ pr ar p) × Key ar p)) ∥₁

符号集合の各 c について、外向きの読みはまず E の要素 q を得る。q を分解すると ar と F および等式 q ≡ pr ar F が得られ、内側の存在量化からは p、等式 c ≡ pr ar p、十通りのペイロード論理式の充足が得られる。

shape-out : ⟨ γ ⊨ shapeAt C w E N ⟩ → (c : S) → ⟨ c .fst ∈ Cv ⟩ → Shaped (c .fst)
shape-out h c c∈ = rec₁ squash₁
  (λ { (q , (q∈ , hb)) → rec₁ squash₁
    (λ { (ar , F , s , (eq , hs)) → map₁
      (λ { (p , s' , (ec , ht)) →

等式 q ≡ pr ar F は、既知の q の E への所属を pr ar F の所属へ輸送する。c に関する等式は保持され、十通りの読みが残りの充足証明を Key ar p へ変換する。

        ar .fst , F .fst , p .fst
        , ( subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈
          , ( ec , TenRead.ten-out C w N (p ∷ s' ∷ F ∷ ar ∷ s ∷ q ∷ c ∷ γ) tg ht ) ) })
      (sndEx-out i4 i1 Sh.ten (F ∷ ar ∷ s ∷ q ∷ c ∷ γ) hs) })
    (bothEx-out i0 inner (q ∷ c ∷ γ) hb) })

元の形の充足は符号集合の要素について全称量化されている。これを c とその所属証明に適用すると、上で除去した存在データが得られ、Shaped (c .fst) の構成が完了する。

  (h c c∈)

内向きの方向では、符号集合の各要素 c が切り詰められた形のデータをもつと仮定する。その切り詰めを除去すると、ar、F、p とともに、pr ar F の E への所属、c に関する等式、Key ar p が得られる。目標自体が命題なので、この除去は正当である。

shape-in : ((c : S) → ⟨ c .fst ∈ Cv ⟩ → Shaped (c .fst)) → ⟨ γ ⊨ shapeAt C w E N ⟩
shape-in k c c∈ = rec₁ (((c ∷ γ) ⊨ ∃̇∈ (var (sh  E)) (bothEx i0 inner)) .snd)
  (λ { (ar , F , p , (q∈ , (ec , key))) →
    let qS = down (lookup E γ) (pr ar F) q∈
        arS = fstS qS ar F refl

pr ar F が E に属することから集合レベルの表示 qS が得られ、その二成分がそれぞれ ar と F を表す。これとは別に、等式 c ≡ pr ar p は c の内部でペイロードの表示 pS を選ぶ。二つの対コンテナが、入れ子の存在論理式に必要な環境を与える。

        FS = sndS qS ar F refl
        δ2 = qS ∷ c ∷ γ
        cq = container qS arS FS refl
        δ5 = FS ∷ arS ∷ cq .fst ∷ δ2
        pS = sndS c ar p ec

内側の論理式はアリティと表のデータで満たされ、十通りの選言は鍵で満たされる。こうして形の充足の全体が、実際のデータから組み上がる。

        cp = container c arS pS ec
        δ7 = pS ∷ cp .fst ∷ δ5
    in ∣ qS , ( q∈ , fillBoth i0 δ2 arS FS refl inner
          (fillSnd i4 δ5 arS pS ec Sh.ten
            (TenRead.ten-in C w N δ7 tg key) i1 refl) ) ∣₁ })

仮定した形の割り当てを c とその所属に適用すると、内向きの構成で用いる切り詰められた証人がちょうど得られる。外向きの方向と合わせると、符号集合の各要素について、形の論理式の充足が命題 Shaped と一致することが分かる。

  (k c c∈)