型付きラムダ計算\lambdaとプログラムから、CCC\mathscr{C}_\lambdaを構成する

この圏\mathscr{C}_\lambdaに一般的な名称ってないんかな #??

特にラムダ計算の項ではなく、型に着目することに注意

これは最も普遍的なCCCになる

つまり「CCCの圏」みたいなのを考えると\mathscr{C}_\lambdaは始対象になるってことか #??

データだけでなく関数も対象として扱う、ということをする

CCCの条件を強めたり弱めたりすることで様々な計算モデルを表現できるらしい

具体例を知りたい #??

圏の構成

対象

\lambdaの型の有限列

対象は型

射

βη同値類の列[M_1],\cdots,[M_n]

対象A_1,\cdots,A_mから、対象B_1,\cdots,B_nへの射

このラムダ抽象M_iの型は、A_1\to(\dots\to(A_m\to B_i)\dots)

それぞれのM_iはβη同値類なので、β簡約すれば同じもの同士になるラムダ抽象

「βη同値類」という単語は固有 #??

射はラムダ抽象

型の導出\Gamma\vdash A

恒等射

[p_1], \cdots, [p_m]

対象A_1,\cdots,A_mの恒等射

ただしp_i=\lambda x^{A_1}_1.\dots\lambda x^{A_m}_m.x_i

合成

以下の2つの射

[M_1],\cdots, [M_n]:(A_1,\cdots,A_m)\to(B_1,\cdots,B_n)

[N_1],\cdots, [N_n]:(A_1,\cdots,A_n)\to(B_1,\cdots,B_k)

の合成は[L_1],\cdots,[L_k]

ただしL_i=\lambda x^{A_1}_1.\dots\lambda x^{A_m}_m.N_i(M_1(\vec{x}))\dots(M_n(\vec{x}))

ただし(M_j(\vec{x}))= (\dots(M_j(x_1))\dots)(x_m))

直積

直積は有限列の連結になる

(A_1,A_2)\times(B_1,B_2,B_3) = (A_1,A_2,B_1,B_2,B_3)

終対象は空列()

冪

(B_1,\cdots,B_n)^{(A_1,\cdots,A_m)}=(\vec{A}\to B_1,\dots,\vec{A}\to B_n)

ただし\vec{A}\to B_iはA_1\to(\dots\to(A_m\to B_i)\dots)

定理 ref p.66

Xを基底型の集合とすると、\mathscr{C}_\lambdaは集合Xから自由生成されたカルテジアン閉圏と同値である

意味がわからん

具体例

型なども一つ2つに定めてものすごく具体的な例を見たい

ラムダ計算とCCCの対応

まだの中で独立した概念になってしまっている

\mathscr{C}_\lambdaから任意のCCCに対して関手が存在する

関手が存在するということは、そのCCC上には型付きラムダ計算の意味論が存在するということを表す

例えば集合の圏SetはCCCの一つであり、\mathscr{C}_\lambdaからSetへの関手があるので、Setにおける型付きラムダ計算の意味論(集合論的モデル)が存在する

参考

『圏論の歩き方』 p.66-

横内『プログラム意味論』にも書いてある