「論理学」カテゴリ内の記事 このカテゴリをはてなブックマークに追加 このカテゴリを含むはてなブックマーク (初公開日順)

2011年1月20日 (木)

時間泥棒の夕べ − 排中律と call/cc

「量子」という考え方を御存知あろう。その特徴として、複数の排他的状態が「可能性」として現実に並存し、観測によってその状態が確定する解釈が有名である。[たと]えれば、先に書いた七芒星の埋め込みの記事で、平面への展開図が発散する方向は確定していないが、空間への埋め込みにおいては、グラフの作画者はスピンの巻き方を左(InLeft)か右(InRight)に決定せざるをえないようなものだ。

七芒星のポスター

この図のグラフでは、Y = 1/X の Y 軸の発散部分を三次元の円筒上に「繰り込ん」で、そこに七芒星を描いています。それを平面に直したグラフも描いていますが、星型の辺部分は、単純に点を直線でつないでいるだけですから、無限に発散する部分は必ずしも、プラスとマイナスで逆方向に描く必要はありません。

続きを読む "時間泥棒の夕べ − 排中律と call/cc"

2011-01-20 19:41:29 (JST) in ストーリー, 情報工学・コンピュータ科学, 精神分裂病, 論理学 | | コメント (7) | トラックバック (7)

2010年11月16日 (火)

IT 革命と私――神学の忌避の向こう

私の上の世代、または、インターネット(WWW)以前の世代の人々の見解として、「神学論争」は実りのない議論の比喩であり、神学そのものが近代理性を知らないアヤしげな宗教的実践であるとみなされていたと思う。そのため、神学は、誠実でありながら、そういった常識にあえて反抗できる…というかなり人を選ぶ学問だと、例えば私は感じていた。

「近代理性」の発展は、「神」という概念を使わずに「社会」と「個人」の関りを説明し、その理性の働きはそこに権限や責任さえ見出させると信じる運動であった…と私は要約するが、その「神」学の忌避は、宗教的対立の超克や呪術的操作への拒絶といったこと以上に、あらゆる時代の若年世代に普遍的に存在した旧世代への反感を基礎にしていた…と考える。

そのような考えに私が至ったのは、私がインターネット黎明期に、コンピュータによる定理証明の研究をしていたことの影響も大きい。

続きを読む "IT 革命と私――神学の忌避の向こう"

2010-11-16 20:13:39 (JST) in 情報工学・コンピュータ科学, 自己紹介, 論理学 | | コメント (0) | トラックバック (0)

2007年9月24日 (月)

真理の前には自由者も束縛される

N を自然数の集合とする。任意の x ∈ N について x < Y なる Y ∈ N、すなわち

Y ∈ N ∧ (∀x. x ∈ N → x < Y)


なる式を満たすように自由変数 Y に代入をすることはできない。Y ∈ N だけを満たすのは 1 でも 2 でも可能である。しかし、特定の n ∈ N が任意の x について x < n とすると n + 1 ∈ N についても n + 1 < n となり矛盾する。Y に代入できるような n は存在しない。上式を仮定すると矛盾が導けるということだ。すなわち、

¬(∃Y. Y ∈ N ∧(∀x. x ∈ N → x < Y))。


最初の式において x は Y を束縛しているわけではない。あえていえば、式が真でなければならないという条件が、Y を束縛するわけだ。

続きを読む "真理の前には自由者も束縛される"

2007-09-24 18:20:06 (JST) in ストーリー, 教育, 論理学 | | コメント (1) | トラックバック (0)

2006年9月 7日 (木)

コンピュータ定理証明における弁証法 − 私が作りたいシステム

コンピュータ定理証明


コンピュータ上での定理証明は、整えられた環境でコンピュータにガイドされながら、特殊なプログラムを書く作業であると言っていい。そのプログラムが実行されると、入力物である真偽不明であった命題が、真なる定理として型付けされ出力されるのだ。

続きを読む "コンピュータ定理証明における弁証法 − 私が作りたいシステム"

2006-09-07 17:29:34 (JST) in プログラム・ウィッシュリスト, 情報工学・コンピュータ科学, 論理学 | | コメント (2) | トラックバック (2)

2006年8月24日 (木)

絶対性

絶対的な真理でないことの可能性を示すのは簡単だが、それを信じる者はそのような可能性を自動的に排除していくのがしばしばである。

続きを読む "絶対性"

2006-08-24 14:32:45 (JST) in ストーリー, 論理学 | | コメント (0) | トラックバック (1)

2006年6月 5日 (月)

参考文献:確率論

統計よりも確率、または確率モデルに興味があります。この記事の初投稿時の 2006 年に概説本を読んだ影響もあり、手近にあった教科書を書き出してみます。これらの他にも統計学やブラックショールズ方程式の本なども別にありますが、それはまた別の機会に。

続きを読む "参考文献:確率論"

2006-06-05 23:01:51 (JST) in 参考文献・リンク集, 確率論, 論理学 | | コメント (3) | トラックバック (3)

2006年4月30日 (日)

セキュアジャパン 2006 の Winny 対策としての VM は釣り?

本丸はこちらのように思います。

共謀罪は、今の日本の体制であればあとから包括的に政府による情報利用を規制する法律を作れば何とでもなるような気がしてスルーしていたのですが、ボット対策とプロバイダ規制の法律が含まれていたんですね。

恥ずかしながら、この記事の公開日の前日(4/29)にはじめて気づきました。

ボットに関して私の意見は下記「参考」の日弁連の見解とだいたい同じです。挙証責任をボット作成者側に課してもよいので主観目的を入れて欲しいです。

さらなるプロバイダ規制をしたいならば、本当は令状の保全・公開システムを作れといいたいのですが、少なくとも、プロバイダへの命令を行ったときに、令状なしであれば、それが保全され自動的に公開されるシステムと、できればプロバイダ側からユーザーへのデータ提供範囲の通知義務が欲しいです。

情報コントロール権やプライバシーを守ることはもちろん、警察などへのなりすましを防ぐことが目的です。タテマエ上はプロバイダ業には自由に参入できるはずですから、セキュリティレベルの低いプロバイダでもダマされにくいよう対策をこうじておこうということです。


セキュアジャパンの VM (Virtual Machine) 構想とは違いますが、VM っつーかエミュレータの技術は、複数の第三者がそれぞれプログラムの仕様を理論的に枝切りしながら総当り的に検証し、その証明過程のソースを公開した上で対象プログラムを電子認証し、そのような認証済プログラムのみリモート実行できるようにする……とかいう技術として、私がずっとやりたかったものなんです。

デバッガの代わりに理論的な極限状況を再現できるものとしてのエミュレータって感じかな。他の方からすれば、エミュレータというよりもインタプリタ + 定理証明システムってことになるのかもしれませんが。

そういった研究は私にとっては困難で諦めていましたから、その分野に研究費がまわるのは研究を離れた今も正直うれしいです。でも、それは今のところ「空中要塞」を造りたいってぐらいのアイデアですからね。

そういう私からすると、Winny 対策に VM ってのは、ボットとかの空中戦がメインになってるのに、ウィルスの射程距離から絶対届かないことを追及するって感じで「大艦巨砲主義」を思い出させるんですよ……


最初、武田様のところにコメントをしたのですが、コメントを許可制になさっていたのか、うまく書き込めなかったのでブログに書き、トラックバックしました。二重になってしまったら、お手数をかけて申し訳ありませんが、コメントを消去していただければと思います。

そのコメントを基にしていますが、かなり書き足しています。


匿名 P2P を認めた上で、著作権法をどう考えるかという私の意見については、あくまで方向性でしかないですが、下記をご参照ください。

更新: 2006-04-30, 2006-05-01
初公開: 2006年04月30日 00:21:58
最新版: 2006年05月01日 02:09:46

2006-04-30 00:21:56 (JST) in 情報工学・コンピュータ科学, 時事, 論理学 | | コメント (4) | トラックバック (4)

2006年2月13日 (月)

不完全性定理: 「真」「偽」「わからない」

記号論理学入門の講座をある程度長く習うと、最後のほうでゲーデルの不完全性定理について学ぶことがあると思う。

欧米流の「真」「偽」ですべてを結着するような考え方は間違いで、論理では「真」「偽」「わからない」の三値を考えるべきだなどという意見を見ることもあるが、不完全性定理とは、これを支持するように見えて、実はこれを否定するような定理なのである。

続きを読む "不完全性定理: 「真」「偽」「わからない」"

2006-02-13 23:07:59 (JST) in ストーリー, 論理学 | | コメント (1) | トラックバック (0)

2006年1月31日 (火)

メタ論理: 演驛と帰納

「演驛」とは論理的に命題を導くことである。

「帰納法」は演驛の一つである。しかし、帰納法を学ぶことで、人は帰納のなんたるかを知る。それが「帰納」である。

続きを読む "メタ論理: 演驛と帰納"

2006-01-31 15:46:30 (JST) in ストーリー, 論理学 | | コメント (0) | トラックバック (0)

2006年1月29日 (日)

なぜ記号論理学から社会科学を目指すようになったのか

学生当時、私は、流行していたオブジェクト指向プログラミングの考えを記号論理学に持ち込むことをまず目標とした。

続きを読む "なぜ記号論理学から社会科学を目指すようになったのか"

2006-01-29 20:18:37 (JST) in 自己紹介, 論理学 | | コメント (0) | トラックバック (2)