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

日々の流転


2008-08-12 [長年日記]

λ. cwaでの自然数型の解釈

(書きかけ)

この間はユニット型について考えたので、今度は自然数型を。

自然数型の規則

自然数型に関する通常の規則は以下のようなもの。

--------------
Γ ├ N : set
Γ ├ 0 : N

Γ ├ M : N
--------------
Γ ├ s(M) : N

Γ, n : N ├ C set
Γ ├ M0 : C[n:=0]
Γ, n : N, x : C ├ Ms : C[n:=s(n)]
Γ ├ M : N
--------------------------------------
Γ ├ elim([n]C,M0,Ms,M) : C[n:=M]
Γ ├ elim([n]C,M0,Ms,0) = M0 : C[n:=0]
Γ ├ elim([n]C,M0,Ms,s(M)) =
       Ms[n:=M, x:=elim([n]C,M0,Ms,M)] : C[n:=s(M)]

なんだけど、例によって以下のように変形した規則で考える。

---------
├ N set
├ 0 : N

---------------
x:N ├ s[x] : N

Γ, x:N ├ P[x] set
Γ ├ M0 : P[0]
Γ, x:N, y:P[x] ├ Ms[x,y] : P[s[x]]
------------------------------------
Γ, x:N ├ elim(P,M0,Ms)[x] : P[x]
Γ ├ elim(P,M0,Ms)[0] = M0 : P[0]
Γ, x:N ├ elim(P,M0,Ms)[s[x]]
            = Ms[x, elim(P,M0,Ms)[x]] : P[s[x]]

省略記法

cwaでの解釈をまともに書いていると大変なので、ちょっと略記法を導入する。(後で書く)

cwaでの解釈

で、cwaで解釈するとこうなる。

  • N∈Fam(1)
  • 0∈Tm(1, N)
  • s∈Tm(1・N, N+)
  • P∈Fam(Γ・N+), M0∈Tm(Γ, P[0+]), Ms∈Tm(Γ・N+・P, P[π・N+][s+][π]) が与えられたとき、h=elim(P,M0,Ms)∈Tm(Γ・N+, P) が存在し、h[0+]=M0, h[π・N+][s+]=Ms[h] が成り立つ。

\xymatrix@+20pt{ \Gamma \ar[r]^{0^{+}} \ar[d]|{h[0^{+}]=M_0} & \Gamma\cdot N^{+} \ar[d]^h \\ \Gamma\cdot P[0^{+}] \ar[r]_{0^{+}\cdot P} & \Gamma\cdot N^{+}\cdot P }

\xymatrix@+20pt{ \Gamma\cdot N^{+} \ar[rr]^{s^{+}} \ar[d]|{h[\pi\cdot N^{+}][s^{+}]=M_s[h]} & & \Gamma\cdot N^{+}\cdot N^{+} \ar[d]|{h[\pi\cdot N^{+}]} \ar[r]^{\pi\cdot N^{+}} & \Gamma\cdot N^{+} \ar[d]^{h} \\ \Gamma\cdot N^{+}\cdot P[\pi\cdot N^{+}][s^{+}] \ar[rr]_{s^{+}\cdot P[\pi\cdot N^{+}]} & & \Gamma\cdot N^{+}\cdot N^{+}\cdot P[\pi\cdot N^{+}] \ar[r]_-{\pi\cdot N^{+}\cdot P} & \Gamma\cdot N^{+}\cdot P }

\xymatrix@+20pt{ \Gamma\cdot N^{+} \ar[d]_{M_s[h]} \ar[rr]^h & & \Gamma\cdot N^{+}\cdot P \ar[d]^{M_s} \\ \Gamma\cdot N^{+}\cdot P[\pi\cdot N^{+}][s^{+}] \ar[rr]_-{h\cdot P[\pi\cdot N^{+}][s^{+}][\pi]} & & \Gamma\cdot N^{+}\cdot P\cdot P[\pi\cdot N^{+}][s^{+}][\pi] }

λ. お菓子買いだめ

今月は少なめで。
[お菓子]

Tags: