Gemmaの日記 このページをアンテナに追加 RSSフィード

2010-02-16

計算モデルと論理とゲーデルの不完全性定理 01:22  計算モデルと論理とゲーデルの不完全性定理 - Gemmaの日記 を含むブックマーク  計算モデルと論理とゲーデルの不完全性定理 - Gemmaの日記 のブックマークコメント

ゲーデルの不完全性定理は、数学を扱う数学、つまりメタ数学を考えるが、それだと理解が難しい。しかし、証明(数学)=プログラムという悟りを開くと、プログラムを扱うプログラム、つまりメタプログラムを考えればよくなり、それならコンパイラ等でなじみがあるので理解が優しくなる。

話の流れは以下。

1. プログラムとは何か

2. 証明とは何か

3. 証明=プログラム

                   ,
           (   {、 {   ヽ.ー、、
               \、__ぃ._ゝ⌒ヾ iヾ)}、_
              ン_ー-_二ー-, 〉 {厶 _、ヽ              _
             ヽ._>'´ / /,ィ/ / ハYヘい       ,. -- 〃⌒
 r−-、      ィ´  〃 ,イ/7'  ,イイ/ 小ヽ 丶、 ,. ‐ '´ハ i   ″`ヽ、
、ヽ、     /幺ィ  {从{小込v' jゥ仏厶川リ}  YV,   小 Vj. |丶   ヽ
 ` ー-ミー--'_,辷三彡'´ | V'芯`   芬Yjル/ハ. /   V√ヽ._! l\ \ '⌒ヽ
  ,. -‐ ` ̄    _ファィ! "´     ``ン'´イハy′    l{辷 { い. ト、ヽ._ヽ、   \
y'´   __,,_ ___,,彡'´八ム   _'__ 、_幺イ厶/     |'心`VヽヘE、ヽY い、  \
′   / |!    r==ァ'゙’_ヘ、 ´_ー,Z.彡-―-〈   ‐- 、 ド¨    {tリj ハ> i`′   ヽ
.    /   !リ    ,.幺-‐=,.イ´'´ ,. / /   ヽ    \l __ '   `゙ ん}.i_,」      `、
.    i`¨¨´   . '´ /ィ<{V/  /,イ i′ ,ハ `、   、ぃヽ「⌒`j   厶イl」     、   ぃ ―――証明と
ヽい  l     /  /レ′/〈.い、___,{.{   , -‐ \ \ーヘ` ` `ヒ´_イy , ム、 、   ヽ.   }.}、
`  \V  /,   ,{ {  '´_,ム≧ー、-ヘー}-/  ,. -‐-、ヽノ  ヽ  ハ `バ´^)\`ー-)  }ハ.  ハ{
 ,. 、   >'/   { い.ィ/ゥ ̄`ハ}ヽ\.{ /    _Vごヽ.._/   }ー}`丶乙ヽ '7ノ^ }/
ヽ'^\ー '´_,,. -‐<ゝ`ー之,_ //  }ハヘ{、i    ヽ`マTハ_ _/;  ヽ、 ハ、}ノ┐
,、-‐¬''" ,イ丁二了 {  ___彡' / ノノ  ヘ!      `∨だ¬ /  ∠_` }ヘ ン
 〉 -r‐/√    l ハ._乙 -‐'´/´/    ム      ヾ^ `i′ \ ` ー1´ヽ
-ー‐¬、Y'      |/   /了¨¨´  , '  -‐ ' ,.小、       丶 !    丶.     i
  /_,.      ,?..._ {イ{   /    / |′丶       マi 、_         ト、     ,nyぃ/
 /´ /      ∠-- .._`丶、 ィ"¨¨ ーヘ 〉|   \      ヽ     -‐   ヽl `"¨¨´ ̄|il}い} , プログラムは―――
    { ,ィ,イ厂¨\.!  `ヽ/ '´ ̄`¨マ´/ |     i>、   , - \, '"⌒丶. ハ  __,,.. 」リ近'´
   ∨い、   ` ',         _,. -≧ュ、',      |エ\       Y         |´    ,ゝだンゥー
           i      ,./'´ヽ ヾ 'r-ヘ    l-, -― 、   l.        !    ` }} `^`
          、_r{ヽ   //´  ,.ィ √ }ーヘ  -‐'´__,. 、  ヽ   |__,,.. _、  、ヽ
          ュ?ム′ , '  /。/ // ,'ム斗ヘ  /    `¨´    l     ヽ   丶
         ゞイ} ,ム./   ∧/−-/ ァZ/! i._ぃ (._,,.. ヘ下、   i l |ィT_i_、_ \.  ',
         ケ´|./ 〈  ∧/__ ,<./ / 7/、!´ 「 i.ヘ r‐ 、___`ー--‐―_、i. l i!ヘヘヽ、\ }
         °厶イ\/∨¨7`ヽ'´ ; / l i  l lヘヾヽ._`¨`ーァー ユ´l=キミ、vヘ_ぃ. Y         「「おなじだよ♪」」
           ,.ゝヘ2__,イ'‐ / / ′!j_! | !. -i¬ ヘ.く`ヽ`¨´ー'´/ィケ i. l i! l マヘ.ヘ\j
         r'´  `¨^タ_ / / i /l_j、|i_,,. l-‐!__Vドヽ`ー‐z_'.イ√丁| i! ト、i_,.Vヘヾ`ヽ、
         ヽ.___,.イ_/ `7、,' !´ i j ヘ Y'i,.ィ'"^v,.--}、`^マ´/ _/ 7√¨¨マ丁ンj_,.イ´ マベへ`ヽ、
           / //‐-/、/ヽ| / . V   !  〉¬ーi、_〉、Y´,_}厶_rt__ri.}└1厶ィつ}ヘへ>>>ぅ,
         // //..__// ヽj' !、__! { jー-'¨´/  厂ヽ.__マ^¨¨´   `1  r‐}_  `ーラ^´ r、√
         Z/V ヽ,くノ _ 廴_j、ノ  j,.、_y'    /   ム._广^i        `¨´  `辷'´厶ノ´

                 ハスケル・カリー & ウィリアム・ハワード

4. プログラムできないこと(停止性問題)

5. 証明できないこと(ゲーデルの不完全性定理)

何はともあれ、定義を見てみよう。

自然数論を含む帰納的に記述できる公理系が、ω無矛盾であれば、証明も反証もできない命題が存在する。

- ゲーデルの不完全性定理

なんのこっちゃだが、今から分かりやすく説明する。

プログラムとは何か

まだコンピュータが登場していない1930年代、「計算とは何か」を考えた人たちがいた。

現代から見れば、計算はコンピュータの仕事だから、「プログラムとは何か」となる。

最も有名な計算モデルが、チューリングチューリングマシンである。

チューリングマシン

http://eva-lu-ator.net/~gemma/geocities/godel/turing.png

以下の3つでできている。

  • 無限に長いテープ
  • テープを読み書きするヘッド
  • マシンの状態を記憶するメモリ

以下のように計算をする。

http://eva-lu-ator.net/~gemma/geocities/godel/turing321.png

チューリングマシンは単純だが、何でも計算できる。

帰納的関数

次に、クリーネ帰納的関数という計算モデルを紹介する。

http://eva-lu-ator.net/~gemma/geocities/godel/kleene.png

帰納的関数とは、プログラムでいえば、IF-THEN-ELSEとループと代入さえあれば何でも計算できるということで、BASICやC言語の考え方に近い。

以下のように計算をする。

http://eva-lu-ator.net/~gemma/geocities/godel/kleene321.png

ループに"箱"があって、その値を書きかえるのが、C言語の教科書によくある「変数とは箱のようなもの」という話のもとである。

ラムダ計算

次に、チャーチラムダ計算という計算モデルを紹介する。

http://eva-lu-ator.net/~gemma/geocities/godel/church.png

ラムダ計算は、Haskellなどの関数型言語の基礎であり、ループの代わりに再帰(入れ子)を使う。

以下のように計算をする。

http://eva-lu-ator.net/~gemma/geocities/godel/church321.png

再帰に"穴"があって、その値を書きかえないのが、Haskellの教科書によくある「変数とは穴(ラベル)のようなもので、Haskellには副作用がない」という話のもとである。

余談だが、チューリングとクリーネは、チャーチの弟子である。

     ____
   /__.))ノヽ
   .|ミ.l _  ._ i.)
  (^'ミ/.´・ .〈・ リ
  .しi   r、_) |  チューリングとクリーネはわしが育てた
    |  `ニニ' /
   ノ `ー―i´
アロンゾ・チャーチ

以上の3つの計算モデルは、後になって実は等価であるとわかった。

つまり、チューリングマシンができることは帰納的関数やラムダ計算でもできるし、その逆もできるとわかった。

証明とは何か

   / ̄ ̄\
 /   _ノ  \
 |    ( ●)(●)
. |     (__人__)  公理からはじめて
  |     ` ⌒´ノ   論理をつないだものだろ、常識的に考えて…
.  |         }
.  ヽ        }
   ヽ     ノ        \
   /    く  \        \
   |     \   \         \
    |    |ヽ、二⌒)、          \
ゲルハルト・ゲンツェン

ゲンツェンが考えた自然演繹という公理系は、常識的な感覚で証明とは何かを考えたもので、名前からして"自然"とついている。

http://eva-lu-ator.net/~gemma/geocities/godel/gentzen.png

以下のように証明をする。

http://eva-lu-ator.net/~gemma/geocities/godel/gentzen321.png

数学的帰納法は、プログラムでいう再帰と原理的に一緒である。

証明=プログラム

以上3つの計算モデルと1つの公理系をまとめると以下のようになる。

名前作者キモ具体例
チューリングマシンチューリング無限に長いテープコンピュータ
帰納的関数クリーネ無限に続くループC言語
ラムダ計算チャーチ無限に続く再帰Haskell
自然演繹ゲンツェン無限に続く数学的帰納法証明

無限に続く数学的帰納法というのは、無限にある自然数が続く限り帰納法を繰り返せるということで、つまり、ゲーデルの不完全性定理にあった"自然数論を含む帰納的"である。

証明=プログラムについては、

自然演繹と型付きラムダ計算がぴったり対応しているすげー!というカリー=ハワード対応を筆頭に、

プログラムを数学的に厳密に定義しようというプログラム意味論や、証明の正しさをコンピュータで検証しようという定理証明器の研究がある。

以上より、"無限ループを記述できるプログラム"="自然数論を含む帰納的に記述できる公理系"を認めてほしい。

プログラムできないこと(停止性問題)

どうかすると無限ループしてしまうプログラムというのは、バグっていて使い物にならない。

それでは、"プログラムが無限ループするかを判定するプログラム"を書くことはできるだろうか?というのが停止性問題である。

冒頭で述べた、プログラムを扱うプログラム、メタプログラムのおでましである。

もしできるなら、ブラウザクラッシャがポップアップを無限にだすのを未然に防げてさぞ便利だろう。

結論からいえば、停止性問題は解決不能であり、そんなプログラムは不可能である。以下で証明する。

http://eva-lu-ator.net/~gemma/geocities/godel/terminate.png

プログラムr(r)は、停止しないか、停止するか、のどちらかである。

場合1「r(r)は停止しない」とき、then loopを通ったはずである。よって、Oracle(r,r)は、「r(r)は停止する」と答えたはずである。矛盾している。

場合2「r(r)は停止する」とき、else stopを通ったはずである。よって、Oracle(r,r)は、「r(r)は停止しない」と答えたはずである。矛盾している。

どちらの場合も矛盾しているので、そもそも、Oracleの存在を仮定したのが誤りだったことになる。

よって、Oracleは存在しない。q.e.d.

メタプログラムにできないことは他にもたくさんあるが、たいていは停止性問題に帰着できる。

証明できないこと(ゲーデルの不完全性定理)

プログラムできないプログラムがあった。

そして、"無限ループを記述できるプログラム"="自然数論を含む帰納的に記述できる公理系"である。

よって、証明できない証明もあるはずだ、というのが、ゲーデルの不完全性定理である。

無矛盾かつ完全な公理系がある

停止性問題は、無限ループが原因で生まれる。よって、IF-THEN-ELSEと代入しかないような、ループを書けないプログラムには、停止性問題はない。ありとあらゆるプログラムが必ず停止する。

同様に、ゲーデルの不完全性定理は、数学的帰納法が原因で生まれる。よって、「もし〜ならば」しかないような、数学的帰納法が書けない公理系には、不完全性定理はない。ありとあらゆる命題の正しさを証明できる。

例えば、命題論理は、無矛盾かつ完全な公理系である。

(fuga様のコメントをいただき訂正 2010/2/17 20:50)

無矛盾かつ完全な公理系としては例えば実閉体の理論やPresburger算術の理論がある。

よって、よくある勘違いに「どんな公理系も不完全である」というのがあるが、誤りである。

ただ、無限ループを書けないプログラムや、自然数論を扱えない公理系なんて、つまらなくて考えるに値しないと思って、「どんな公理系も」と言いたくなる気持ちはわからないでもない。

ゲーデル数

メタプログラムなら、プログラムをデータ(テキストファイル)として扱うことを自然に考えられるが、

メタ証明だと、証明を自然数として扱うという、頭の痛くなることを考えるはめになる。それがゲーデル数の考え方である。

ゲーデルはきっと大変だったろう。

停止性問題に似た数学の問題

例1. 円周率 3.141592... に、今日の日付 20100217 は出てくるだろうか? あるいは、任意の自然数が出てくるだろうか?

出てくるまで計算を続けるしかない。もしかしたら永遠に出てこないかもしれない。

例2. コラッツの問題

数学の未解決問題である。有限回で必ず停止するか?というのが、停止性問題を連想させる。

ラッセルのパラドックス

停止性問題の結論は、プログラムが無限ループするかを判定するプログラムは無限ループする、だった。

つまり、

無限ループを判定するプログラム自身が、無限ループするプログラムの集合に含まれる。

不完全性定理の具体例としてよくあげられる、ラッセルのパラドックスの、床屋版が以下である。

ある村でたった一人の男性の床屋は、自分で髭を剃らない人全員の髭を剃り、それ以外の人の髭は剃らない。この場合、床屋自身の髭は誰が剃るのだろうか?

つまり、

自分で髭を剃らない人の髭を剃る人自身が、自分で髭を剃らない人の集合に含まれる。

停止性問題とラッセルのパラドックスは、よく似ている。

ゲーデルの不完全性定理の意義

普通にプログラムを書いていれば、メタプログラムや停止性問題には出会わない。

同様に、普通に証明を書いていれば、メタ数学や不完全性定理には出会わない。

停止性問題で困るプログラマがいないのと同様、不完全性定理で困る数学者もいない。

強いて言えば、停止性問題を知っていると、ブラウザクラッシャを未然に防ぐメタプログラムを開発しろ、と言われたとき、それは無理です、とすぐ断れる。

同様に、不完全性定理を知っていると、数学の無矛盾性を数学で証明しろ、と言われたとき、それは無理です、とすぐ断れる。

実用性はあまりない。

オブジェクト指向

今まで黙っていたが、オブジェクト指向(アクターモデル)も、立派な計算モデルである。

http://eva-lu-ator.net/~gemma/geocities/godel/hewitt.png

オブジェクト指向は、ヒューイットアラン・ケイなどが60〜70年代に考え出した。

以下のように計算する。

http://eva-lu-ator.net/~gemma/geocities/godel/hewitt321.png

ラムダ計算とオブジェクト指向は、よく似ている。クロージャとオブジェクトの微妙な関係

http://eva-lu-ator.net/~gemma/geocities/godel/church.png(ラムダ計算)

プログラムはなぜ動くか

抽象的な計算モデルが、だんだんほぐれて、チューリングマシンに落ちる様子を描いてみた。

http://eva-lu-ator.net/~gemma/geocities/godel/pyramid.png

いろんな事情があって、Coq(定理証明器) -> OCaml(型付きラムダ計算) -> C言語(帰納的関数) -> コンピュータ(チューリングマシン) という、コンパイラのピラミッドができているのが面白い。

参考文献

fugafuga 2010/02/17 12:50 間違いがあるので指摘します。
>例えば、命題論理は、無矛盾かつ完全な公理系である。
>よって、よくある勘違いに「どんな公理系も不完全である」というのがあるが、誤りである。
論理の演繹システムについて言われる「完全」というのは、公理系の「完全」とは異なります。
なので「どんな公理系も不完全である」への反論としては不適切です。
完全な公理系としては例えば実閉体の理論やPresburger算術の理論があります。

ShoonShoon 2010/02/17 14:41 証明=プログラム ってとこ詳しく説明願いたいんだが、、、
プログラム=任意の自然数 N に対して命題p(N)が成り立つことを帰納的に証明する
って考えればOK??

GemmaGemma 2010/02/17 20:51 fuga様
おっしゃる通りです。訂正しました。
ゲーデルの不完全性定理とゲーデルの完全性定理の"完全"は全く違う意味だから注意せよというやつにまんまと引っかかりました。
有益なコメントありがとうございます。

GemmaGemma 2010/02/17 21:07 Shoon
証明=プログラムについては、参考文献に挙げたP.WadlerのProofs are Programsが面白いです。
もう少し堅い説明は↓がおすすめです(参考文献に追加しました)。
http://www.ice.nuie.nagoya-u.ac.jp/~h003149b/lang/p/frag/frag_g.html

tobarikitobariki 2010/02/18 01:20 とても面白かったので、
がんばってゲーデルの不完全定理を理解したいと再熱しました。

GemmaGemma 2010/02/18 13:44 tobariki様
ありがとうございます。

staff456staff456 2010/03/03 19:56 こんにちは。2chRSSのやつ、使わせていただいてます。
で、質問なんですが、最後のURLに //が2つついているのは仕様でしょうか?

http://2ch2rss.dip.jp/rss.xml?url=http://venus.bbspink.com/test/read.cgi/megami//1202620202

こんな感じになるのでリーダーに登録できません・・・

GemmaGemma 2010/03/17 17:49 staff456様
修正しました。ご迷惑をおかけして申し訳ありませんでした。

2009-05-05

nsIInputStreamPumpの非同期処理にジェネレータを使う 13:25  nsIInputStreamPumpの非同期処理にジェネレータを使う - Gemmaの日記 を含むブックマーク  nsIInputStreamPumpの非同期処理にジェネレータを使う - Gemmaの日記 のブックマークコメント

こいつの使いかたをググると、onDataAvailableのたびに配列(メッセージキュー)に並べておいて、上から順番に処理するコードがよく見つかる。

実はAjaxのとき話題になったんだが、ジェネレータで、こういった非同期処理を同期処理のように書ける。

この実験のために、いわゆるechoサーバをlocalhostの60000番ポートに立ててある。

"yield" == "onDataAvailableまでsleep".

let p = Application.console.log;

function nettest() {
  //ソケット(トランスポート)を作る
  let TransportService = Cc["@mozilla.org/network/socket-transport-service;1"].
                           getService(Ci.nsISocketTransportService);
  let transport = TransportService.createTransport(null, 0, "localhost", 60000, null);
  let line = {};
  //非同期処理にジェネレータを渡す。
  callWithClientSocket(transport, function(cistream, costream) {
                          //サーバに"hello\n"を送って、
                          costream.writeString("hello\n");
                          //待つ。
                          yield;
                          //サーバから返事が来たら1行読む。
                          cistream.readLine(line);
                          //コンソールにプリント。
                          p(line.value);
                          //サーバに"world\n"を送って、
                          costream.writeString("world\n");
                          //待つ。
                          yield;
                          //サーバから返事が来たら1行読む。
                          cistream.readLine(line);
                          p(line.value);
                          //サーバに"こんにちは\nせかい"を送って(UTF-8でおk)
                          costream.writeString("こんにちは\n");
                          costream.writeString("せかい");
                          //待つ.
                          yield;

                          cistream.readLine(line);
                          p(line.value);
                          cistream.readLine(line);
                          p(line.value);
                          yield;
                        });
}

function socketInputStream(aTransport) {
  //ソケットの入力ストリームをとる
  let istream = aTransport.openInputStream(0, 0, 0);

  //ソケットの入力ストリームの文字コードをUTF-8にする
  let cistream = Cc["@mozilla.org/intl/converter-input-stream;1"].
                   createInstance(Ci.nsIConverterInputStream);
  cistream.init(istream, "UTF-8", 0, Ci.nsIConverterInputStream.DEFAULT_REPLACEMENT_CHARACTER);
  //ソケットの入力ストリームを行単位で読むようにする
  cistream.QueryInterface(Ci.nsIUnicharLineInputStream);

  //ソケットの入力ストリームの非同期ポンプをとる
  let pump = Cc["@mozilla.org/network/input-stream-pump;1"].
               createInstance(Ci.nsIInputStreamPump);
  pump.init(istream, -1, -1, 0, 0, false);

  return [pump, cistream];
}

function socketOutputStream(aTransport) {
  //ソケットの出力ストリームをとる
  let ostream = aTransport.openOutputStream(0, 0, 0);
  //ソケットの入力ストリームの文字コードをUTF-8にする
  let costream = Cc["@mozilla.org/intl/converter-output-stream;1"].
                   createInstance(Ci.nsIConverterOutputStream);
  costream.init(ostream, "UTF-8", 0, Ci.nsIConverterInputStream.DEFAULT_REPLACEMENT_CHARACTER);

  return costream;
}

function callWithClientSocket(aTransport, aProc) {
  //ソケットの入出力ストリームと、非同期ポンプをとる。
  let [pump, cistream] = socketInputStream(aTransport);
  let costream         = socketOutputStream(aTransport);

  // Javascript 1.7 の新機能、ジェネレータを作る。
  let generator = aProc(cistream, costream);

  //非同期ポンプのリスナ
  let listener = {
    generator: generator,  //onDataAvailableでの"環境"はちょっと特殊。
    transport: aTransport, //onDataAvailableでの"環境"はちょっと特殊。
    onStartRequest: function onStartRequest(channel, context) {
    },
    onStopRequest: function onStopRequest(channel, context, status, errorMsg) {
      this.generator.close();
      this.transport.close(null);
    },
    onDataAvailable: function onDataAvailable(channel, socketContext, inputStream, sourceOffset, count) {
      //非同期ポンプにデータが来るたびに、ジェネレータを進める。
      this.generator.next();
    }
  };
  generator.next(); //こいつをonStartRequestに書くと動かないのは、なんで?
  pump.asyncRead(listener, null);
}

小ネタ

  • Firefox3拡張を書くなら、もうvarは捨ててletでいいとのこと(id:nanto_viさんに教えてもらった。thx.)。C言語構文の皮をかぶったSchemeの世界征服計画が進んでいるぜ。ふっふっふ。
  • echoサーバはGaucheユーザリファレンス: gauche.selector - 簡単なディスパッチャからパクった。
  • 最近は、XPCOMのIOやソケットの、Gauche風のラッパーを書きためている。callWithClientSocketという関数名もGaucheからパクった。
  • Ajaxにジェネレータを使うのは有名だけど、"nsIInputStreamPump yield"でググっても出てこない。既出だったら教えてください。

2009-03-14

Gemma2009-03-14

SchemeのOpenGLで流体力学なデモを書いてみた 22:48  SchemeのOpenGLで流体力学なデモを書いてみた - Gemmaの日記 を含むブックマーク  SchemeのOpenGLで流体力学なデモを書いてみた - Gemmaの日記 のブックマークコメント

  • 双方とも 1〜2 fpsだった。元のC言語のは 70 fpsだった。
  • OpenGLの関数名が、YpsilonだとglBegin, glVertex2fと元に忠実なのに対して、Gaucheだとgl-begin、gl-vertexと、Scheme風になっているところに、思想の違いがあるかもしれない。

2008-07-21

Python勉強中 04:32  Python勉強中 - Gemmaの日記 を含むブックマーク  Python勉強中 - Gemmaの日記 のブックマークコメント

Google App EngineのためにPythonを勉強中。

自分はScheme使いなので、

Lisp プログラマのための Python 入門がとても役にたっている。

そういえば、学部3年で、「C言語の次に学ぶべきは、LispかPythonか」で迷ったときにも、この文書を読んだ覚えがある。

読んだけど内容が理解できなくて、結局、なんとなく、題名で先に来ているからというので、Lispを学ぶことにした。

おかげで、SICPや、関数型言語の世界に巡りあえたように思う。

もし題名が「Python プログラマのための Lisp 入門」だったらPythonに進んだかもしれない。

今では、私がScheme使い。孫にあげるのはもちろん(ry

mzpmzp 2008/07/22 11:35 そういえばThe Art of Unix Programmingの参考文献にも無門関がありました。 > 禅

GemmaGemma 2008/07/22 16:49 面白いな。坐禅をプログラミングに変えるだけでいろいろ見えてくるw
俺が何か本を書いたら、参考文献に「のだめカンタービレ」とか書いてみたい。

GemmaGemma 2008/07/22 17:35 何か学習者を、3年くらいうんうん唸らせて、この道に集中させられるような課題が、他にないかな? 自分は「継続」や「クロージャ=オブジェクト」のおかげでSICPに興味を持って読めたわけだ。
昔の人はよく考えてるなw

2008-06-07

ちょっと面白い予見として、電子書籍ではテキスト検索ができないと思う。 07:59  ちょっと面白い予見として、電子書籍ではテキスト検索ができないと思う。 - Gemmaの日記 を含むブックマーク  ちょっと面白い予見として、電子書籍ではテキスト検索ができないと思う。 - Gemmaの日記 のブックマークコメント

それは、電子書籍のデータ形式は、画像ファイルになると思うから。

テキストデータじゃない。PDFでもない。

それじゃテキスト検索ができなくて、当然みんなブツブツ言うんだけど、それが未来だと思う。

そんな馬鹿なことってあるだろうか?

いまや本の編集作業はデジタル化されて、

原稿のテキストデータがあって、

DTPソフトは当然のごとくPDFを吐けるのに?

これは、デザインの「悪い方がよい」原則による。

  • 画像ファイルはとにかくシンプルだ。出版社はスキャナにかけるだけ、ブックリーダはそれを表示するだけ。原則から、実装の単純さはすべてに勝る。
  • 画像ファイルは一貫している。テキストデータもPDFも、全部画像ファイルに統一できる。
  • 画像ファイルはすべてを飲み込める。レイアウトも、挿絵も、フォントも、文章も、なにもかも。

なんてズボラなんだろう。

でも、これがWorse is betterだ。

歴史が、この原則の正しさを証明している。

それはUnix、C言語、Perlだ。

2008-01-29 関数型言語って何がすごいんですか このエントリーを含むブックマーク このエントリーのブックマークコメント

C使いの人に、

関数型言語って何がすごいんですか

と聞かれて、

じゃあC言語で accumulator すなわち、数nをとり、「数iを取ってnをiだけ増加させ、その増加した値を返す関数」を返すような関数を書いてみろよ

って言ったら、

値を返す関数を返すような関数・・・? オンドゥルルラギッタンディスカー

で、会話が続かない。

さらに、C使いのターン。

関数に関数を渡せる? Cだって関数ポインタ渡せますよ。

チューリング完全なんだから、どんなプログラムだって書けますよ。

と仕掛けてきた。そこで、

じゃあ、3回呼ぶと動作が変わる関数を書いてみて。

f();

f();

f();

f();

と呼ぶと、

3

2

1

liftoff

って出力されるやつ。ロケットみたいな。

できました。

#include <stdio.h>

void f() {
  static int count = 3;
  if (count) {
    printf("%d\n",count);
    count--;
  } else printf("liftoff\n");
}

int main(void) {
  f();
  f();
  f();
  f();
  return 0;
}

OK. じゃあさ・・・。実はロケットは2機あったんだよ。ロケットg。カウントダウン別々で。

f();

f();

f();

f();

g();

g();

と呼ぶと、

3

2

1

liftoff

3

2

ってなるようにしてくれ。

と問題をだしたら、白旗をあげて、

安西先生・・・関数をコピーしたいです・・・

となった。関数がファーストクラスなのが関数型言語の特徴さ。

おっと、関数型言語に触れてしまったか。甘い痺れがいつまでもとれないだろう?

javascript ならこうなります。

function rocket(n) {
  return function () {
    if (n) {
      console.log(n);
      n--;
    } else console.log('liftoff');
  }
}

var f = rocket(3);
var g = rocket(3);
f();
f();
f();
f();
g();
g();

通りすがり通りすがり 2008/02/11 05:26 これは関数型言語というより,クロージャのオブジェクト指向的使い方.
C++等なら同じことはオブジェクトでできる(例:Boostやデリゲート).

Lisp/Schemeが有名だった昔はこれが大きな特徴だったのだけど,
今はこういうことを関数型言語の特徴というのはあまり良くない気が……
副作用のない純粋な関数型言語ではできないことだし.
現にHaskellはできない,Ocamlは参照型を使う必要あり.

GemmaGemma 2008/02/12 07:47 鋭いですね!その通りです。自分の勉強が足りませんでした。
Objects are a poorman’s closures. 逆も然り。
うーん。この日記でやりたかったのは、手続き型言語しか知らない人に、関数をコピーしたいな、つまり、関数がファーストクラスだったらな、という切り口を見せたい、ということなんです。
副作用のない純粋な関数型言語ではできないこと という点は耳が痛いです。
もしその点をも満たしていて、しかも、関数型言語の特徴がよくわかる例があれば、ぜひ教えてください!
このスレッドを自分はまだ読んでいません。
http://groups.google.com/group/fa.haskell/browse_thread/thread/40221a24b1f31422

コメントお待ちしています。

関数言語勉強中関数言語勉強中 2012/01/30 22:11 お題の件。C言語書きならば、迷わずロケット状態の構造でメモリ確保してポインタを関数に渡すと答えると思いますよ。

2008-01-03

有名なOCamlプログラムTop10 15:27  [http://ocamlnews.blogspot.com/2007/12/top-10-most-popular-ocaml-programs.html:title=有名なOCamlプログラムTop10] - Gemmaの日記 を含むブックマーク  [http://ocamlnews.blogspot.com/2007/12/top-10-most-popular-ocaml-programs.html:title=有名なOCamlプログラムTop10] - Gemmaの日記 のブックマークコメント

1.FFTW

FFTWはまぎれもなく世界最速なフーリエ変換の実装である。

MATLABなど多くの商用アプリケーションで使われている。無料で利用でき、ほとんどすべてのLinuxディストリに同梱されている。FFTWライブラリを構成するFFTルーチンは、OCamlが生成したC言語のコードからできている。(このOCamlプログラムはgenfftという。)

2.Unison

Unisonファイル同期ツールである。Unix用とWindows用がある。

ファイルやディレクトリ群の複製が、別のホスト(あるいは同じホストの別のディスク)に置いてあるとする。各々に変更をする。すると、それぞれの変更を複製同士で伝えあってくれて、最新にすることができる。

3.MLDonkey

MLDonkeyは、オープンソースなeDonkey2000クライアントである。

P2Pのファイル共有ができる。Linux, Unix, Solaris, MacOSX, MorphOS, Windowsで動く。

4.Planets

Planetsは、惑星系をシミュレートして遊べる、簡単で対話的なプログラムである。

GPLで配布されている。LinuxとWindowsで動く。

5.Hevea

Heveaは、高性能なLaTeX→HTML変換器である。

6.FreeTennis

FreeTennisは、テニスシミュレータである。高度なAIとリアルな3Dグラフィックが特徴。

7.LEdit

LEditは、bashやtcshなどのシェルで動くプログラムに、行編集機能を加える

(訳者註: ledit ocaml、ledit gosh -i などが便利です。)

8.Polygen

Polygenは、自然な文章を生成する高度なプログラムである。文法定義および構文&字句ルールをユーザが与える。

9.MTASC

MTASCは、世界初のオープンソースActionScript2コンパイラである。

10.ADVI

ADVIは、DVIファイルのビューワ、プレゼンタである。

DVIに視覚エフェクトを記述できるようになっていて、手の込んだプレゼンがノートPCでできる。

mzpmzp 2008/01/03 22:27 leditはよく使ってます。世界最速なフーリエ変換って格好いいですね。

GemmaGemma 2008/01/03 23:30 実はOCamlプログラムで最も有名だっていうFFTWを知らなくてさ、なんてこったいと思って、えいやっと訳してみた。
今年はAdobe AIRでも覚えようかな。GaucheでXML吐けるし。

2007-12-21

Javascript使いもSICPを読むべき 11:09  Javascript使いもSICPを読むべき - Gemmaの日記 を含むブックマーク  Javascript使いもSICPを読むべき - Gemmaの日記 のブックマークコメント

Javascriptで名前空間を汚染しないようにクロージャを使うイディオム、例えばA JavaScript Module Patternって、

SICP第3章のコレじゃん。

3.1.1 Local State Variables

(define (make-account balance)
  (define (withdraw amount)
    (if (>= balance amount)
        (begin (set! balance (- balance amount))
               balance)
        "Insufficient funds"))
  (define (deposit amount)
    (set! balance (+ balance amount))
    balance)
  (define (dispatch m)
    (cond ((eq? m 'withdraw) withdraw)
          ((eq? m 'deposit) deposit)
          (else (error "Unknown request -- MAKE-ACCOUNT"
                       m))))
  dispatch)

(define acc (make-account 100))
((acc 'withdraw) 50)
50
((acc 'withdraw) 60)
"Insufficient funds"
((acc 'deposit) 40)
90
((acc 'withdraw) 60)
30

このSchemeをJavascriptで書くとこうなる。

function make_account(balance) {
  function withdraw(amount) {
     if (balance >= amount) {
         balance -= amount;
         return balance;
     } else  return "Insufficient funds";
  }
  function deposit(amount) {
    balance += amount;
    return balance;
  }
  return {
     withdraw: withdraw,
     deposit: deposit
  }
}; 
var acc = make_account(100);
acc.withdraw(50);
50
acc.withdraw(60);
"Insufficient funds"
acc.deposit(40);
90
acc.withdraw(60);
30

Javascriptは C言語構文の皮をかぶったSchemeなので、ぜひSICPを読むべきだと思う。読めばクロージャを完璧に理解できる。

Javascript1.7で let文やyieldや分割代入が入るので、これからますますSchemeっぽくなる。

Javascriptで学ぶSICPって書いたら面白そう。

          l      /    ヽ    /   ヽ \                         
          /     / l    ヽ /      |  \                       
   し な 間 〉 //  l_ , ‐、   ∨ i l  | |    \      継               
| ら っ に |/ l ,-、,/レ‐r、ヽ  |   /`K ,-、 <   よ                  
| ん て あ   / | l``i { ヽヽ l | / , '/',` //`|_/       続               
| ぞ も わ    |> ヽl´、i '_   。`、llィ'。´ _/ /,) /\    こ                  
| |   な   |`/\ヽ'_i ,.,.,.⌒´)_ `_⌒  /__/l  \       を               
っ   |    く    |/ / l´,.-― 、l`ー一'_冫 /l l |   /   せ                  
!!!! |        \ ', /  /`7-、二´、,.| /// |   /                       
           lT´ {  /  /  ト、 |::| /// /  /    !!!!!                  
          l´ ヽ、 > ー    ,/ |ニ.ノ-' / / _                      
              i``` 、/ }    ',,,..'  |-'´,- '´     ̄/ ヽ∧  ____ (こいつはyieldだ!
           \/ ' \_  `´ノ7l´      /    // ヽ l ヽ   クソッタレー!)
         / ̄ |      ̄ ̄/ ノ L___/      ★  U  |             
        /   ヽ      /`ー´     /l                 |            
          

2007-10-04

Gaucheで数式処理を書いてみたい 05:37  Gaucheで数式処理を書いてみたい - Gemmaの日記 を含むブックマーク  Gaucheで数式処理を書いてみたい - Gemmaの日記 のブックマークコメント

数学科でD加群のゼミをとった。計算機科学との相性が良さそうだから。

で、国産の数式処理ソフトの名前がちらほら (Risa/Asirやkan/sm1) 耳に入る。

これらはC言語で書いてあるようだ。さらにBoehm GCを使い、Bignumや、exact number(有理数表現)を自前でやっているようだ。

Lisp/Schemeの再発明をしているようにも思える。

こういった数学用のソフトウェアには昔はLispがよく使われていたそうな。

ためしにGaucheで階段行列を計算するプログラムを書いたら、gauche.arrayが大変役に立った。

Gaucheで数式処理ソフトを書くというのも面白そうだ。それでグレブナ基底を計算できるようにしたい。

2007-07-26 コルーチンとギャラクシアン このエントリーを含むブックマーク このエントリーのブックマークコメント

SICP読書会で、26日に継続について話してほしいとのこと。

前回、id:zyxwvさんがC言語で書いたS式計算機を披露したとき、彼は、パーサ、というかミニ正規表現、の有限状態遷移を書くために、switch文があふれかえってしまい、困っているとのことだった。

これは、C言語で有限状態マシンを書くにはどうしたらよいか、ということだ。

つ"

の「解読の輪」とか「cdecl」あたり"

本質的に書きたいのは相互再帰なんだけど、C言語で再帰を書くとスタックを消費してしまうことに抵抗があって、この本の実装に落ち着いたんじゃないかなと思われる。

つ"タスクシステム"

昔懐かしのギャラクシアンで、タスクシステムが使われたらしい。シューティングゲーム開発に便利。ただ、C言語にはクロージャがないので、関数ポインタ+データを使わなきゃならない、ついでに無名関数がないので、いちいち関数を宣言しなきゃならない。switch文よりはマシ。

で、C言語のタスクシステムは、Schemeでいうコルーチンだ。コルーチンには継続だ。

コルーチンは、ノンプリエンプティブだ。で、格闘ゲームでは、波動拳のモーションの途中で攻撃をくらったらヤラレモーションにはいる。これってプリエンプティブじゃない?知らないけど。

だからSchemeでいうエンジンが役に立つかもしれない。知らないけど。

エンジンについては独習3週間と本格的にはKent本をどうぞ。

エンジンを使うと並列論理和ができる(ってKent本に書いてあった。)。

mzpmzp 2007/07/13 23:57 ゲームで使うタスクシステムやらコルーチンの話は、やねう本2で読みました。
全体的に説明不足な感のある本でしたが。

syd_sydsyd_syd 2007/07/14 02:00 懐かしいね。Logician’s Lordかな?
http://web.archive.org/web/20041009222313/www.hh.iij4u.or.jp/~peto/Games/games_top.html

GemmaGemma 2007/07/14 04:21 >mzp
おっ、やねう本2ですか。実はゲーム開発に興味あり?
Game Programming Gems 2 のマイクロスレッドで補えるかも。

>syd_syd
それそれ!タスクシステムの説明で一番いいサイトだったのに無くなってしまったんですよね。web.archiveにかろうじて残っていたとは知らなかったです。

shiroshiro 2007/07/26 06:31 ゲームのタスクシステムのタスクは1フレーム内で実行が済むような細粒度のものなので、モーションの途中で攻撃を喰らっても実行中のタスクが割り込まれるわけじゃないです。継続が変化するだけ。
Schemeなどで抽象化する場合の問題はメモリ管理でしょうか。昔のタスクシステムはデータエリアの大きさの上限を決めておけば、タスク用メモリの配列を静的に確保して、実行中はアロケーションフリーでいけたんですよね。CPUも速くなったしincremental GCなどを使えば昔ほどGCを気にする必要はないのかもしれませんが、やっぱりシューティングやアクションゲームだとGCが入るのはきついんじゃないでしょうか。

GemmaGemma 2007/07/26 21:20 全く同意見です。格闘ゲームにプリエンプション云々は間違いでした。
実時間処理でGCをググッたら”Timed-GCを備えた実時間型Schemeシステム”http://ci.nii.ac.jp/naid/110003179934/en/ というのを見つけました。
ソフトリアルタイムのErlangのGCはどうなってるのかと思ったら、独立した小さなスレッドの小さなヒープだし、メッセージパッシングのデータはコピーしてるしで、条件を満足できるらしいです。
http://lists.tunes.org/archives/gclist/2001-January/001975.html