トップ «前の日記(2008-08-02) 最新 次の日記(2008-08-05)» 月表示 編集

日々の流転


2008-08-04 [長年日記]

λ. cwaでのユニット型の解釈

Categories with attributes (cwa) で cwa の簡単な説明を書いたので、今度は cwa で幾つかの基本的な型を扱ってみることに。 まずは一番簡単と思われるユニット型を。

構成規則と導入規則

通常扱う構成規則と導入規則は以下のような形になっている。

---------------
Γ ├ Unit set
Γ ├ () : Unit

これだと任意のΓについて考えなければならず面倒くさいが、実際のところはそれらの解釈はΓが空である場合からweakeningによって得たものと等しくなければならないので、Γを空の場合に限定した以下の規則を考えることにする。

--------------
├ Unit set
├ () : Unit

これはそれぞれ Unit ∈ Fam(1) と () ∈ Tm(1, Unit) で解釈される。 Γが空でない場合は、weakening -[!Γ] を使って Unit[!Γ]∈Fam(Γ) と ()[!Γ]∈Tm(Γ, Unit[!Γ]) で解釈できる。

除去規則

お次は除去規則で、通常の除去規則はこんな形をしている。

Γ, x : Unit ├ P set
Γ ├ M : P[x:=()]
Γ ├ N : Unit
--------------------------------
Γ ├ elim(P,M,N) : P[x:=N]
Γ ├ elim(P,M,())=M : P[x:=()]

ただ、これも少し扱いにくいので、少し変えて、以下のような規則を考える。

Γ, x : Unit ├ P[x] set
Γ ├ M : P[()]
---------------------------------------------
Γ, x : Unit ├ elim(P,M)[x] : P[x]
Γ ├ elim(P,M0)[()] = M : P[()]

これの解釈は、 任意の P ∈ Fam(Γ・Unit[!Γ]) と M ∈ Tm(Γ, P[()[!Γ]]) に対して、 elim(C,M) ∈ Tm(Γ・Unit[!Γ], P) が存在し、 elim(C,M)[()[!Γ]] = M ∈ Tm(Γ, P[()[!Γ]]) が成り立つということになる。 図で書くと以下のような感じになる。

\xymatrix@+15pt{ \Gamma \ar[r]^{() [!_\Gamma]} \ar@{.>}[d]|{\mathrm{elim}(C,M)[() [!_\Gamma]]=M} & \Gamma\bullet \mathrm{Unit}[!_\Gamma] \ar@{.>}[d]|{\mathrm{elim}(C,M)} \\ \Gamma\bullet P[() [!_\Gamma]] \ar[r]_{() [!_\Gamma]\bullet P} & \Gamma\bullet\mathrm{Unit}[!_\Gamma]\bullet P }