型付きラムダ計算とCCCと直観主義論理
型付きラムダ計算$ \lambdaとプログラムから、CCC$ \mathscr{C}_\lambdaを構成する この圏$ \mathscr{C}_\lambdaに一般的な名称ってないんかな #?? 特にラムダ計算の項ではなく、型に着目することに注意
つまり「CCCの圏」みたいなのを考えると$ \mathscr{C}_\lambdaは始対象になるってことか #?? データだけでなく関数も対象として扱う、ということをする
CCCの条件を強めたり弱めたりすることで様々な計算モデルを表現できるらしい 圏の構成
対象
$ \lambdaの型の有限列
対象は型mrsekut.icon
射
βη同値類の列$ [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はβη同値類なので、β簡約すれば同じもの同士になるラムダ抽象 「βη同値類」という単語は『圏論の歩き方』.icon固有 #?? 型の導出$ \Gamma\vdash A
https://gyazo.com/01ad48d2ab0d30cc6b5aa8a8f00022b8
恒等射
$ [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
https://gyazo.com/f7aff80ba2541f12401021a663d7641e
合成
以下の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)
https://gyazo.com/89a100f6c666b5c8faba6b363f93fd83
定理 ref『圏論の歩き方』.icon p.66
$ Xを基底型の集合とすると、$ \mathscr{C}_\lambdaは集合$ Xから自由生成されたカルテジアン閉圏と同値である
意味がわからんmrsekut.icon
具体例
型なども一つ2つに定めてものすごく具体的な例を見たいmrsekut.icon
ラムダ計算とCCCの対応
まだmrsekut.iconの中で独立した概念になってしまっている
https://gyazo.com/71378f19be64abe2d29a4c9fbf4b9703
$ \mathscr{C}_\lambdaから任意のCCCに対して関手が存在する
関手が存在するということは、そのCCC上には型付きラムダ計算の意味論が存在するということを表す
例えば集合の圏SetはCCCの一つであり、$ \mathscr{C}_\lambdaからSetへの関手があるので、Setにおける型付きラムダ計算の意味論(集合論的モデル)が存在する 参考