曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

線形論理(ジラール)

ネッカーキューブ錯視と線形論理の連言

ちょっとした思い付きです。 ネッカー・キューブというのは誰しも一度は見たことがあるであろう錯視図である。 ja.wikipedia.org 表示されてるかな? これは一つの平面図形が二通りの見え方をする、二通りの立方体に見える、という錯視である。一つの感覚入…

シーケント計算の完全性定理(線形論理)

前回こんなことを書いたけれど更に完全性定理について cut-elimination.hatenablog.com Troelstra先生の本を読んで線形論理の代数的意味論の完全性定理を勉強しているところなのだけれど、 Lectures on Linear Logic (Lecture Notes Book 29) (English Editi…

線形論理の代数的意味論のメモ

Troelstra先生の"Lectures on Linear Logic"を読んで線形論理の代数的意味論を勉強している。 Lectures on Linear Logic (Lecture Notes Book 29) (English Edition) 作者:Troelstra, A. S. Center for the Study of Language and Inf Amazon いま本では大幅…

【しゃあっコヒーレンス・スペース!】整合空間(coherence space)をじっくりとその2 安定関数(stable function)

↓これの続きです。 cut-elimination.hatenablog.com 今回は安定関数が出てくるはずです。 用語の整理 いろいろ用語、記法が出てきている。 用語・記法:整合空間 の要素を の点(point)という。 のクリークを整合部分集合(coherence subset)とも言う。点とは…

【しゃあっコヒーレンス・スペース!】整合空間(coherence space)をじっくりとその1

↓これの続きっちゃあ続きである。 cut-elimination.hatenablog.com "Proofs and Types"を読んでいくシリーズだったが、第7章のSystem Tの導入をちょっと飛ばして第8章の整合空間(coherence space)を詳細に読みたいのよ。 整合空間から線形論理を解説している…

ジラール先生の"Proofs and Types"の5,6章を(ちょっと真剣に)読む(シーケント計算、強正規化定理)

↓これの続きでこざる。 cut-elimination.hatenablog.com シーケント計算 シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなん…

ジラール先生の"Proofs and Types"の3,4章を(ちょっと真剣に)読む(カリー=ハワード同型、正規化定理)

↓これの続きでっせ。 cut-elimination.hatenablog.com 3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。 Chapter 3 カリー=ハワード同型 命題を型と対応させる。型付項のシステムにおいても sense と den…

フル線形論理のカット除去定理を証明する際のポイント(あんまり親切でない記事です)

この本で線形論理の勉強をしているよ。 Lectures on Linear Logic (Lecture Notes Book 29) (English Edition) 作者:Troelstra, A. S. Center for the Study of Language and Inf Amazon 加法も乗法も量化子も指数も全部入れたフル線形論理のカット除去定理…

ジラール先生の"Proofs and Types"の1,2章を(ちょっと真剣に)読む

私は現代最高のロジシャンはJean-Yves Girardだとガチで思っている。 ジラール先生の論文や本は、理論的なものであっても個人の論理に対する考えが混入していることがよくあるように思う。時には本線のテクニカルな議論からやや離れたお話のようなことが書か…

ジラール先生の映画批評を読む「千と千尋の神隠し」編

ジャン=イヴ・ジラール先生は大量の映画短評を書いておられる。ジラール先生のサイトの"alter ego"というところから読める。 girard.perso.math.cnrs.fr オルター・エゴというだけあって、Yann-Joachim Ringardという変名で書いている。おもしろい。 フラン…

ルディクス(遊技)についてメモ(順次改訂)

ルディクスに興味があるのだけれどあんまりよくわからない*1。わかったことをメモしておく。 ジラール先生が最初に提案したのは1999年の論文らしいのだが、本格的に論じられているのは2001年の"Locus Solum"という長い論文である。こちらのほうが基本文献と…

線形論理超入門!!

デカく構えたタイトル!! 後期に専門が違う人向けに研究の説明をする演習があるようなので、ロジックが専門でない人向けの線形論理の解説を考えたい。 自然演繹からシーケント計算へ 論理学の入門講義をとったことがある人は多そうなので、自然演繹から入っ…