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

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

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

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

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

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

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

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

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

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

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 を束縛するわけだ。

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

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

■	コンピュータ定理証明

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

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

絶対性

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

続きを読む "絶対性"

参考文献：確率論

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

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

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

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

● 《H17-163閣法22 共謀罪＆サイバー刑法／「組織犯罪処罰法改正法案」犯罪の国際化及び組織化並びに情報処理の高度化に対処するための刑法等の一部を改正する法律案》

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

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

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

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

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

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

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

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

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

■	参考 ● 《「セキュア・ジャパン２００６」（案）に関する意見の募集》 ● 《日弁連：国際刑事立法対策委員会 サイバー犯罪条約とその国内法化に関するＱ＆Ａ》 ● 《武田圭史：政府、安全にウィニーを使用するためのソフトを開発？》 ● 《とりあえず月配列とかのブログ：Winny対策に税金でVirtual PCくれる、だなんてシャレがきついっすよ》 ● 《アンカテ：Winny規制はもしやるなら責任者を明確にして実施すべき》 ● 《Tomo’s HotLine：プロバイダがWinnyを規制する本当の思惑とは？》

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

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

■	私の P2P ファイル共有に関する記事 ● 《ISP による Winny 規制が良くない理由》 ● 《Winny 媒介流出事件 ― 新たなプロバイダ規制 vs P2Pファイル共有の信頼モデル》 ● 《P2P を用いた作業履歴流通の可能性》 ● 《JRF の公開ブックマーク：Winny事件》 ● 《JRF の公開ブックマーク：ネット法学》

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

● 《はてなブックマーク「投げ銭予約」のアイデアまとめ − 金本位制のメタファより》 ● 《フィギュアの写真の著作権に対する見解》 ● 《GPL のここが嫌い》

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

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

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

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

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

メタ論理: 演驛と帰納

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

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

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

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

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

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