線形論理
linear logic
古典線形論理 CLL
始式 :$ \frac{}{D\vdash D}(I),$ \frac{}{\Gamma,0\vdash\Delta}(0),$ \frac{}{\Gamma\vdash\top,\Sigma}(\top),$ \frac{}{\bot\vdash\quad}(\bot),$ \frac{}{\quad\vdash 1}(1)
換 (permutation) :$ \frac{\Gamma,A,B,\Pi\vdash\Delta}{\Gamma,B,A,\Pi\vdash\Delta}(PL),$ \frac{\Gamma\vdash\Delta,A,B,\Lambda}{\Gamma\vdash\Delta,B,A,\Lambda}(PR)
Cut :$ \frac{\Gamma\vdash\Delta,D\quad D,\Pi\vdash\Lambda}{\Gamma,\Pi\vdash\Delta,\Lambda}(Cut)
雙對 (否定)$ ^\bot:$ \frac{\Gamma\vdash\Delta,D}{D^\bot,\Gamma\vdash\Delta}(^\bot L),$ \frac{D,\Gamma\vdash\Delta}{\Gamma\vdash\Delta,D^\bot}(^\bot R)
$ 1^{\bot}=\bot,$ \bot^{\bot}=1,$ 0^{\bot}=\top,$ \top^{\bot}=0
(別な導入法$ A\vdash B\iff B^\bot\vdash A^\bot(對偶)。$ \frac{A^\bot}{A\multimap C})?
$ A\vdash B\iff B^\bot\vdash A^\botを更に、不可能性$ A\vdash\neg B\iff B\vdash\neg Aと非必然性$ -A\vdash B\iff B\vdash-Aとに分けたら何が起こるだらう? 必然性$ \neg-、可能性$ -\neg
乘法的 (multiplicative)。同時 (simultaneous) 存在
$ \otimes(tensor 積、乘法的連言。融合積 (fusion)) :$ \frac{A,B,\Gamma\vdash\Delta}{A\otimes B,\Gamma\vdash\Delta}(\otimes L),$ \frac{\Gamma\vdash\Delta,A\quad\Pi\vdash\Lambda,B}{\Gamma,\Pi\vdash\Delta,\Lambda,A\otimes B}(\otimes R) $ Aと$ Bの兩方を得られる$ A\otimes B\vdash C\iff A,B\vdash C
單位元は$ 1。$ A\otimes 1=1\otimes A=A
分配律$ A\otimes(B\oplus C)=(A\oplus B)\otimes(A\otimes C) $ ⅋(par、乘法的選言。分裂和 (fission)) :$ \frac{A,\Gamma\vdash\Delta\quad B,\Pi\vdash\Delta}{A⅋B,\Gamma,\Pi\vdash\Delta,\Lambda}(⅋L),$ \frac{\Gamma\vdash\Delta,A,B}{\Gamma\vdash\Delta,A⅋B}(⅋R)
$ Aも$ Bも得られないとするとおかしい$ C\vdash A,B\iff C\vdash A⅋B
單位元は$ \bot。$ A⅋\bot=\bot⅋A=A
分配律$ A⅋(B\&C)=(A\&B)⅋(A\&C) 加法的 (additive)。擇一 (alternative) 存在
$ \&(with、加法的連言) :$ \frac{A,\Gamma\vdash\Delta}{A\&B,\Gamma\vdash\Delta}(\&L_1),$ \frac{B,\Gamma\vdash\Delta}{A\&B,\Gamma\vdash\Delta}(\&L_2),$ \frac{\Gamma\vdash\Delta,A\quad\Gamma\vdash\Lambda,B}{\Gamma\vdash\Delta,A\&B}(\&R)
$ Aか$ Bかどちらかをこちらが選べる$ A\&B\vdash A,$ A\&B\vdash B,$ \frac{C\vdash A\quad C\vdash B}{C\vdash A\&B}
單位元は$ \top。$ A\&\top=\top\&A=A
$ \oplus(plus、加法的選言) :$ \frac{A,\Gamma\vdash\Delta\quad B,\Gamma\vdash\Delta}{A\oplus B,\Gamma,\Delta}(\oplus L),$ \frac{\Gamma\vdash\Delta,A}{\Gamma\vdash\Delta,A\oplus B}(\oplus R_1),$ \frac{\Gamma\vdash\Delta,B}{\Gamma\vdash\Delta,A\oplus B}(\oplus R_2)
$ Aか$ Bかどちらかを相手が選んでこちらに與へられる$ A\vdash A\oplus B,$ B\vdash A\oplus B,$ \frac{A\vdash C\quad B\vdash C}{A\oplus B\vdash C}
單位元は$ 0。$ A\oplus 0=0\oplus A=A
$ \multimap(lolli、線形含意) :$ \frac{B,\Gamma\vdash\Delta\quad\Pi\vdash\Lambda,A}{A\multimap B,\Gamma,\Pi\vdash\Delta,\Lambda}(\multimap L),$ \frac{A,\Gamma\vdash\Delta,B}{\Gamma\vdash\Delta,A\multimap B}(\multimap R) $ A\multimap B\iff A^\bot⅋B.
$ A^\bot\oplus Bは???
別な導入法$ A,B\vdash C\iff A\vdash B\multimap C.
指數的結合子
$ !(of course、必然性$ \square) :$ \frac{\Gamma\vdash\Delta}{!A,\Gamma\vdash\Delta}(!W),$ \frac{!A,!A,\Gamma\vdash\Delta}{!A,\Gamma\vdash\Delta}(!C),$ \frac{A,\Gamma\vdash\Delta}{!A,\Gamma\vdash\Delta}(!L),$ \frac{!\Gamma\vdash?\Sigma,A}{!\Gamma\vdash?\Sigma,!A}(!R)
$ !X\otimes!Y=!(X\&Y),$ 1=!\top。指數法則$ e^xe^y=e^{(x+y)}の類似
(正の樣相$ \frac{A\vdash B}{!A\vdash!B}。必然性$ !A\&!B\vdash!(A\&B)。$ \frac{!A}{C\multimap A})?
實質含意は嚴密含意の如く$ A\to B\iff!(A\multimap B)と分析できる
$ ?(why not、可能性$ \lozenge) :$ \frac{\Gamma\vdash\Delta}{\Gamma\vdash\Delta,?A}(?W),$ \frac{\Gamma\vdash\Delta,?A,?A}{\Gamma\vdash\Delta,?A}(?C),$ \frac{A,!\Gamma\vdash?\Sigma}{?A,!\Gamma\vdash?\Sigma}(?L),$ \frac{\Gamma\vdash\Delta,A}{\Gamma\vdash\Delta,?A}(?R)
$ ?X⅋?Y=?(X\oplus Y),$ \bot=?0
(正の樣相$ \frac{A\vdash B}{?A\vdash?B}。可能性$ ?A\oplus?B\vdash?(A\oplus B)。$ \frac{?A}{A\otimes C})?
$ 1:$ \frac{\Gamma\vdash\Delta}{1,\Gamma\vdash\Delta}(1L)
$ \bot :$ \frac{\Gamma\vdash\Delta}{\Gamma\vdash\Delta,\bot}(\bot R)
量化
※$ tは任意の變項を表し、$ aは下式に現れない變項を表す事にする
全稱量化$ \forall:$ \frac{F\lbrack t/x\rbrack,\Gamma\vdash\Delta}{\forall xF,\Gamma\vdash\Delta}(\forall L),$ \frac{\Gamma\vdash\Delta,F\lbrack a/x\rbrack}{\Gamma\vdash\Delta,\forall xF}(\forall R)
存在量化$ \exist:$ \frac{F\lbrack a/x\rbrack,\Gamma\vdash\Delta}{\exist xF,\Gamma\vdash\Delta}(\exist L),$ \frac{\Gamma\vdash\Delta,F\lbrack t/x\rbrack}{\Gamma\vdash\Delta,\exist xF}(\exist R)
light liner logic (LLL)
指數的結合子$ !,$ ?を廢し、代はりに$ \sharp,$ \natural,$ \flatを持つ
始式$ \frac{}{\sharp\top\vdash 1}(\sharp L),$ \frac{}{1\vdash\sharp\top}(\sharp R),$ \frac{}{\bot\vdash\flat 0}(\flat R),$ \frac{}{\flat 0\vdash\bot}(\flat L)
$ \sharp:$ \frac{}{}(\sharp W),$ \frac{}{}(\sharp C),$ \frac{}{}(\sharp-\&),$ \frac{}{}(\sharp-\sharp),$ \frac{}{}(\sharp-\natural)
$ \flat:$ \frac{}{}(\flat W),$ \frac{}{}(\flat C),$ \frac{}{}(\flat-\oplus),$ \frac{}{}(\flat-\flat),$ \frac{}{}(\natural-\flat)
$ \natural:$ \frac{}{}(\natural-\otimes),$ \frac{}{}(\natural-⅋),$ \frac{}{}(\natural-\natural),$ \frac{}{}(\natural R),$ \frac{}{}(\natural L)
直觀主義線形論理 (ILL)
整合空閒 (coherent space) 意味論
整合空閒は無向 graph
clique (部分整合空閒)
整合空閒に於ける安定寫像 (stable map) は有限呼び出し (finite call property) であり直觀主義論理に對應する。これを函數だけでなく引數も直和を保存する樣に制限した線形寫像 (linear map) は單一呼び出し (unique call property) であり線形論理に對應する $ \top\coloneqq(\varnothing,\varnothing)は空整合空閒。$ \bot\coloneqq(\{*\},\{(*,*)\})は單位整合空閒
$ 0\coloneqq(\varnothing,\varnothing)。$ 1\coloneqq(\{*\},\{(*,*)\})
整合空閒$ X=(|X|,\sim)の雙對空閒$ X^\bot=(|X|,\sim^\bot)を$ x\sim^\bot y\coloneqq x\cancel\sim y\lor x=yで定義すると、$ X^\bot\cong X\multimap\botであり$ (X^\bot)^\bot=X。これは線形代數に於ける雙對空閒の類似
證明網 (proof nets)
sequent 化された證明網としての證明圖 (proof diagram)
相互作用の幾何 (geometry of interaction)
引數と返り値
data と計算
型と値