続きといえば↓これの続き。
cut-elimination.hatenablog.com
豊岡さんが型なし証明論と並べてもうひとつ挙げていた論文がAndreoli "Logic Programming with Focusing Proofs in Linear Logic"という論文。線形論理の世界では超有名な論文だが初めてちゃんと読んだ。
これはタイトルのとおり線形論理を論理プログラミングに応用することを狙ったもので哲学論文ではない*1。なのだけれども、ここで導入された焦点化(focusing)の概念は証明の分析として斬新なもので、証明論的意味論への応用も期待できる。
線形論理には乗法的演算子と加法的演算子の区別があるがこの論文では「同期(synchronous)」と「非同期(asynchronous)」の区別が導入される。これは線形論理においては非常に自然に区別できる。この区別を導入することで線形論理の証明探索が効率的になる。この探索が論理プログラムの計算と解釈できるのである。
これらの区別はジラール先生の"Locus Solum"という論文で「正(positive)」と「負(negative)」の極性(polarity)と言い換えられる。"Locus Solum"は超有名論文で、以降ではこちらの呼び方のほうが主流になった。前に書いた↓の6節を参照。
cut-elimination.hatenablog.com
正と負の区別はその後、線形論理以外の論理体系でも考察されている。線形論理由来の概念のおかげで証明の内部にある構造がよりよくわかるようになった例だろう。
この正と負なる言葉はジラール先生のもっと前の"A new constructive logic: classical logic"や"On the unity of logic"という論文にも出てくる。こちらの正負概念は、Andreoli先生の同期・非同期とは、関連はありそうではあるものの違う。しかし"Locus Solum"以降ジラール先生は同期・非同期を正・負と言うようになってしまったので、話がややこしくなっている。ジラール先生の言い換えの意図は何か、Andreoli先生はそれでいいのか、とか気になる。
（追記：後に詳しい方に話を聴いた。"A new constructive logic: classical logic"の極性とAndreoliの同期・非同期は、どちらもインバージョン（推論規則を下から上に遡れること）できるかどうかで定義していて、同じことだと聴いた。なので正・負の極性という用語で統一されたのもべつに変ではないらしい。）
*1:参考文献に日本人が書いた論文がたくさんある。それくらい当時の日本で論理プログラミングは流行っていたのだ。
