callccによる排中律の証明 - sumiiのブログ
Wadlerのパクリ。というか劣化コピー。 悪魔：「あなたが私と契約してくれたら、(A)『私があなたに一億円をあげる』、(B)『あなたが私に一億円をくれたら、どんな願いでもかなえてあげる』のどちらかをして差し上げます。(A)と(B)のどちらにするかは、私が決めます。」 人間：「どちらにせよ害はなさそうなので、じゃあ契約します。」 悪魔：「はい、では私は(B)を選びます。」 人間：「やっぱりそう来るか。でも一億円なんて持ってないし、まあいいや。」 （十年後） 人間：「気になってしょうがないので、悪いことをして一億円を集めました。だから願いをかなえてください。」 悪魔：「そりゃどうも（と一億円を受け取る）。では私は(A)を選びます。はいどうぞ（と一億円を返す）。」 ICFP 2003の会場ではWadlerとShiversが壇上で寸劇をやりました（本当）。λ式で書くと callcc(λk:¬(T
「ラムダ計算」を独学で学習するための，講義ノートやPDFのリンク集 （復習用の問題付き） - 主に言語とシステム開発に関して
講義ノートの目次へ ラムダ計算は，コンピュータ・サイエンスの重要な１分野。 「λ」を使って各種の関数を記述し，λどうしの計算方法を習得すれば・・・ HaskellやF#などの関数型言語を習得するために役立つ。 プログラミングにおいて，関数についての理解を深めることができる。 複雑なアルゴリズムを簡易に記述して，挙動や性質を予測することができる。 計算機科学の，より深い専門的な話題を理解するための足がかりを得られる。 などのメリットがある。 下記に，独学でλ計算を勉強するための， 入門レベルの講義ノートやWebページを掲載する。 読みやすい便利なもの・わかりやすいものから，応用的なものへと並べてある。 質の高いものだけを精選し，わかりづらい資料は除外してある。 ラムダ計算の概要 ラムダ計算の基礎 ラムダ計算の応用 復習のための問題（入門レベル） ※λ計算を利用した計算量・計算複雑性・計算可能
A Reading List for Postgraduates
計算可能性、計算量、アルゴリズム Highly Recommended N.D. Jones, Computability and Complexity: From a Programming Perspective. MIT Press, 1997. ● 計算可能性と計算量について、プログラミング言語を基礎に置いて 平易かつ統一的に説明するのに成功している良書。 もちろん、部分計算など、Jonesならではの話題も充実。 （ただし誤植がかなり多いので注意 － 再版でかなり修正されるそうです） [ 所蔵図書館 ] （研究室にもあります） J.E. Hopcroft, R. Motwani and J.D. Ullman, Introduction to Automata Theory, Languages, and Computation, Second Edition. Addison-W
miniKanren.org
Twitter: @miniKanren Github: @miniKanren Google Group: miniKanren IRC: irc://irc.libera.chat/minikanren Follow @miniKanren Workshop | Book | Online Course | Implementations | Projects | Upcoming Talks | Talks | Interviews | Tutorials | Theses | Papers | Screencasts | Weekly Hangouts | Podcasts | Blogs | Contact What is miniKanren? miniKanren is a family of Domain Specific Languages for lo
Linear Logic (Stanford Encyclopedia of Philosophy)
First published Wed Sep 6, 2006; substantive revision Sat Sep 16, 2023 Linear logic is a refinement of classical and intuitionistic logic. Instead of emphasizing truth, as in classical logic, or proof, as in intuitionistic logic, linear logic emphasizes the role of formulas as resources. To achieve this focus, linear logic does not allow the usual structural rules of contraction and weakening to a
GC撲滅への道 - GC Advent Calendar - miura1729の日記
Garbage Collection Advent Calendarの5日目の記事です。 私はGCが嫌いです。GCは幼稚で礼儀知らずで気分屋で 甘やかすといつまでも動き、ほったらかすとセグフォする。 そんなGCのために、私達人間は何もする必要はありませんよ ♪ ということで、GC撲滅の1方法としてLinear Lispなるものを紹介します。Linear Lispは線形論理という論理に基づいたLisp処理系です。 元論文はこれです。 Lively Linear Lisp -- 'Look Ma, No Garbage!' http://home.pipeline.com/~hbaker1/LinearLisp.html 線形論理については、ここのページが感動的なほどわかりやすいです。 線形論理って何？ (情報科学演習 III 課題紹介（小林研究室）) http://web.yl.is.s.u
ACM Sigplan Notices 27, 8 (Aug. 1992), 89-98.
Introduction Neither a borrower nor a lender be; For loan oft loses both itself and friend ... [Shakespeare, Hamlet, I. iii 75] The sharing of data structures can be efficient, because sharing can substitute for copying, but it creates ambiguity as to who is responsible for their management. This ambiguity is difficult to statically remove [Barth77] [Bloss89] [Chase87] [Hederman88] [Inoue88] [Jone
「数理論理学」（鹿島亮） - あいまいな本日の私 blog
ごく一部で話題になっていた新刊本です。本日買ってきました。210ページのソフトカバー本なんですが、古典論理の自然演繹と列計算（LK）、完全性定理と不完全性定理、さらにはLKのカット除去、また直観主義およびクリプキモデル、さらには中間論理の話題まで扱っており、お得です（コンパクトすぎるため、学生の自習用には難しいかもしれませんが）。 数理論理学 (現代基礎数学) 作者: 鹿島亮出版社/メーカー: 朝倉書店発売日: 2009/10/01メディア: 単行本購入: 11人 クリック: 367回この商品を含むブログ (5件) を見るネット上でまったく内容に関する情報を見つけられなかったので、目次を下に紹介します。 証明を対象にするとは 証明の実例 証明における言葉遣い 証明の前提と結論 証明の本質の抽出 第2章以降へ向けて 自然演繹 項と論理式 導出図 公理からの証明 論理式の真理値 命題論理の論理
直観主義論理の「自然さ」(1) 自然演繹 - 再帰の反復blog
直観主義や直観主義論理そのものには特に思い入れはない。ブラウワーの文章を読んだ覚えはないし、ダメットの文章もほとんど読んでいない。ポアンカレの文章も。でも、もう少し日の目を浴びても良いと思う(それとも知らないだけで、けっこう浴びているのだろうか)。 直観主義論理と自然演繹 自然演繹による証明では、何かある論理式を仮定するところから証明が始まる。仮定された論理式から別の論理式を導き、新しく導かれた論理式からまた別の論理式を導いていく。証明で立てられる仮定は一つとは限らない(複数の仮定を立てないといけない場合の方がたぶん多い)。また証明の途中で、立てていた仮定が取り除かれる場合もある(そのような証明規則が用意されている)。 直観主義論理に対する自然演繹では、論理積・論理和・含意・否定・矛盾の各論理記号について、導入則と除去則と呼ばれる演繹規則を持っている(否定と矛盾についてはちょっと特殊な面が
Ryo Kashima
鹿島 亮 （かしま りょう） 東京工業大学 情報理工学院 数理・計算科学系 准教授 kashima@is.titech.ac.jp 研究テーマ 数理論理学．特に非古典論理やラムダ計算． 主要論文 鹿島 亮: 様相ミュー計算のタブロー法の完全性と無限ゲームの決定性について, 京都大学数理解析研究所 講究録 2233, pp.65-81 (2022). Ryo Kashima, Naosuke Matsuda, and Takao Yuyama: Term-Space Semantics of Typed Lambda Calculus, Notre Dame Journal of Formal Logic 61[4], pp.591-600 (2020). Kento Takagi and Ryo Kashima: On the completeness and the decidabili
15-819K Logic Programming
Logic programming is a paradigm where computation arises from proof search in a logic according to a fixed, predictable strategy. It thereby unifies logical specification and implementation in a way that is quite different from functional or imperative programming. This course provides a thorough, modern introduction to logic programming. It consists of a traditional lecture component and a projec
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Reddit - Dive into anything
講義一覧 | 現代論理学の諸問題 | 慶應OCW|
数理論理学入門(Introduction to Mathematical Logic) 高崎金久（京都大学） 〜京都大学での全学共通科目講義に基づく〜
セキュアコーディング(法政大学 理工学部 応用情報工学科 2年次後期 (2011年度))
researchmap
ERROR Detected
東京工業大学 情報理工学院 数理・計算科学系
15-819K Logic Programming / Schedule
Logic Programming