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 }](tex/3f9b7cee876ecac53c8b09df323baa05.png "\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 }](tex/8babf88d37750599ce5d3ae3009d101c.png "\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] }](tex/49e9f9dc8ea37c97bde41a957570c4e3.png "\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] }")
λ. お菓子買いだめ
今月は少なめで。
![[お菓子]](./images/20080812_0.jpg)
[ツッコミを入れる]
