Ads by Google
新しい記事を書く事で広告が消せます。
ET Q&A
問い詰める会 wiki の方で質問されて （私の不勉強により） うまく答えられなかったことを，研究室の M 先輩を問い詰めて （笑） いろいろ教えていただいたので，ちょっとまとめてみます．
たぶん Web 上での議論には限界があるので （また収集がつかなくなる），さらなる疑問点などは，問い詰める会などでよろしくお願いします．コメント欄などに質問をオープンな形でメモするぶんには大歓迎です （レスはあまり期待しないでください）
(免責 : これは私の理解，解釈であり，間違いは全て私の責任です)
# というか，問い詰める会は，理論的なことをちゃんとやってる M 先輩とかが行った方が （笑）
Q. 正しさの根拠の違い
命令型 : アルゴリズムの一実装 （コーディング）．正しさの議論が困難．仕様 (what) の概念無し．how そのもの
関数型 : how を書くことには変わりないんだけど，プログラムを数学的にすることにより，プログラムが特定の性質を持つことの検証をしやすくする （数学的に検証できるからより確からしいよ派）
論理型 : プログラム = 論理式の集合は問題の定義そのもの (公理)．公理から演繹できるものは全て正しいよ派
ET : 上の全部ができない，プログラムの仕様に対する正当性がちゃんと議論できる理論になっている．
Q. Prolog と ET ってどう違うの ?
Prolog は，仕様 = プログラムなので，プログラムを改善しようと思ったら，仕様自体を変えないといけない．次々と公理を変更したり，増やし続けないといけない．だけど，そうなると，D 自体が変わるのに，D に対する正しさ，正しさの根拠をどうやって議論するの ? (できない)
ET は，仕様とプログラムの空間がわかれているので，プログラムを，新しいルールの探索により，段階的に改善していくことができる．
具体例
論理式の集合 D が与えられたとする．ここは Prolog と同じ．
(append () Y Y) <-.
(append (X | Xs) Y Z) <- (= Z (X | Z1)), (append Xs Y Z1).
どうやってこれを動かすか ?
Prolog は，SLD 導出という，正しさが保障される推論方法 （アルゴリズム） によって実行する．
ET は，仕様から，搾り出し方やメタ計算と呼ばれる，必ず仕様に対して正当な ET ルールを生成する（半）自動アルゴリズムによって，ルールを生成して実行する．
実行とは，質問を展開（書き換え）ていくこと．質問の集合 Q の最大の集合は，D に依存して決まる．D で定義されてない質問には回答できない．
でも，別に，常に想定される最大の Q に対してのアルゴリズムを生成する必要は無い．Q をもっと限定すると，可能な最適化がいろいろと出てくる．
例えば，必ず第一リストはグラウンド（変数じゃない）などの制約．(append (12) Y Z) とか，(append () (1 2) (1 2) とか (append (1 2) (3 4) Z) とか，そういう限定された加算無限集合が Q．
そうすれば，X が変数の場合をケアするアルゴリズムが不要になる．
ET の世界では，D と Q の組 <D, Q> を仕様 (specification) と呼ぶ．
ここらへんから，だんだんと Prolog と離れていく．Prolog の世界は，常に最大の Q を想定するから，D と独立した最適化には限界がでてくる．
ET では，最適化のために，Q を限定するだけで良いのに，Prolog では D を直接変更しないといけない．
Q を非常に限定していくと，プログラムに非決定性は不要になります．特定の入力に対して，一つの出力を出す関数になる．そうすると，より効率的な，決定的なルール (D ルール) でプログラムを表現できます．Prolog の場合は，cut とか使って，直接 D を書き換えないと，手続き （決定的なアルゴリズム） は表現できない．
Q が固定 (常に最大） の世界では，ET と Prolog では，与えられた確定節の集合 D に対する意味はほぼ同じ．
確定節の意味とは，Prolog では任意有限回の推論で得られるアトムの集合．
ET は，データ構造をパラメータ化してる（特殊化システム） ので，それのより一般的な定義になっている （推論とかいう，Logic Programming に依存する概念は入ってない）．
ここから，完全に ET と Prolog の世界は変わる．ここから先の世界が，Prolog では到達不可能な世界．
Prolog の世界では，D からは一つの正当なアルゴリズムしか得られない．アルゴリズムを変えようと思ったら D を直接変えないといけない．これが本質的な問題点．一つの D に対して，一つの手続きしか得ることができないので，それ以上の改善ができない．
ET の世界では，ET ルールを D から出した後，D とルールの世界 (Prog とする) が明確に分かれているから，D を変更することなく，D に対する正当性を厳密に議論できる世界で Prog を改善することができる．
具体的には （トリビアルな例だけど） 結合法則
(append *A *B *C), (append *X *C *Z) ==> (append *X *A *D), (append *D *B *Z)
みたいな手続きは，Prolog では絶対に探索できない，その正しさも証明できない．
ET の理論では，D から直接得られる，正しさが証明されたET ルールを，いわば公理のルールとして,
上のルールも ET ルールであることが証明できる．右辺と左辺を，最初に得られた ET ルールで展開していって，同じ単位節が得られれば，これもまた ET ルール．そして上のルールを ET ルールとして Prog に追加することができる．D は無変更なので，相変わらず D に対する正当性は完璧に保存されているし，議論できる．このようにして，Prog を膨らませていくことにより，より良い手続きを探索することができる．
そもそも Prolog はホーン節の世界だから，ヘッドは一個だけしか許されないんだけど．
そういう狭さは，まぁ本質ではない．CHR とか，Prolog の後継のような言語は，ヘッド*部* に複数の制約の記述を許しているんだけど．CHR も，結局は Prolog と同じ，D と Prog が分かれてないという問題点は解決できていない．
要するに，Prolog も CHR も，ET の世界のごく一部しか表現できない狭い理論ということ （よくある，言語間の優位性戦争なんかとは本質的に異なる．科学的に構造の優位性が証明されている）
Q. 北大の TA ではどんなことを教えているのですか ?
忘れなければ，問題とテキストを印刷して持って行きます．
テキストの一部はここらへんから （ちょっと古い ?）
ETプログラミング入門テキスト(Dルール編)
ETプログラミング入門テキスト(Nルール編) (現在トップからリンク張って無いので，見てよいものなのかは謎だけど)
(ET SITE)
ちょっと今時間無いので，推敲せずにアップ．
たぶん Web 上での議論には限界があるので （また収集がつかなくなる），さらなる疑問点などは，問い詰める会などでよろしくお願いします．コメント欄などに質問をオープンな形でメモするぶんには大歓迎です （レスはあまり期待しないでください）
(免責 : これは私の理解，解釈であり，間違いは全て私の責任です)
# というか，問い詰める会は，理論的なことをちゃんとやってる M 先輩とかが行った方が （笑）
Q. 正しさの根拠の違い
命令型 : アルゴリズムの一実装 （コーディング）．正しさの議論が困難．仕様 (what) の概念無し．how そのもの
関数型 : how を書くことには変わりないんだけど，プログラムを数学的にすることにより，プログラムが特定の性質を持つことの検証をしやすくする （数学的に検証できるからより確からしいよ派）
論理型 : プログラム = 論理式の集合は問題の定義そのもの (公理)．公理から演繹できるものは全て正しいよ派
ET : 上の全部ができない，プログラムの仕様に対する正当性がちゃんと議論できる理論になっている．
Q. Prolog と ET ってどう違うの ?
Prolog は，仕様 = プログラムなので，プログラムを改善しようと思ったら，仕様自体を変えないといけない．次々と公理を変更したり，増やし続けないといけない．だけど，そうなると，D 自体が変わるのに，D に対する正しさ，正しさの根拠をどうやって議論するの ? (できない)
ET は，仕様とプログラムの空間がわかれているので，プログラムを，新しいルールの探索により，段階的に改善していくことができる．
具体例
論理式の集合 D が与えられたとする．ここは Prolog と同じ．
(append () Y Y) <-.
(append (X | Xs) Y Z) <- (= Z (X | Z1)), (append Xs Y Z1).
どうやってこれを動かすか ?
Prolog は，SLD 導出という，正しさが保障される推論方法 （アルゴリズム） によって実行する．
ET は，仕様から，搾り出し方やメタ計算と呼ばれる，必ず仕様に対して正当な ET ルールを生成する（半）自動アルゴリズムによって，ルールを生成して実行する．
実行とは，質問を展開（書き換え）ていくこと．質問の集合 Q の最大の集合は，D に依存して決まる．D で定義されてない質問には回答できない．
でも，別に，常に想定される最大の Q に対してのアルゴリズムを生成する必要は無い．Q をもっと限定すると，可能な最適化がいろいろと出てくる．
例えば，必ず第一リストはグラウンド（変数じゃない）などの制約．(append (12) Y Z) とか，(append () (1 2) (1 2) とか (append (1 2) (3 4) Z) とか，そういう限定された加算無限集合が Q．
そうすれば，X が変数の場合をケアするアルゴリズムが不要になる．
ET の世界では，D と Q の組 <D, Q> を仕様 (specification) と呼ぶ．
ここらへんから，だんだんと Prolog と離れていく．Prolog の世界は，常に最大の Q を想定するから，D と独立した最適化には限界がでてくる．
ET では，最適化のために，Q を限定するだけで良いのに，Prolog では D を直接変更しないといけない．
Q を非常に限定していくと，プログラムに非決定性は不要になります．特定の入力に対して，一つの出力を出す関数になる．そうすると，より効率的な，決定的なルール (D ルール) でプログラムを表現できます．Prolog の場合は，cut とか使って，直接 D を書き換えないと，手続き （決定的なアルゴリズム） は表現できない．
Q が固定 (常に最大） の世界では，ET と Prolog では，与えられた確定節の集合 D に対する意味はほぼ同じ．
確定節の意味とは，Prolog では任意有限回の推論で得られるアトムの集合．
ET は，データ構造をパラメータ化してる（特殊化システム） ので，それのより一般的な定義になっている （推論とかいう，Logic Programming に依存する概念は入ってない）．
ここから，完全に ET と Prolog の世界は変わる．ここから先の世界が，Prolog では到達不可能な世界．
Prolog の世界では，D からは一つの正当なアルゴリズムしか得られない．アルゴリズムを変えようと思ったら D を直接変えないといけない．これが本質的な問題点．一つの D に対して，一つの手続きしか得ることができないので，それ以上の改善ができない．
ET の世界では，ET ルールを D から出した後，D とルールの世界 (Prog とする) が明確に分かれているから，D を変更することなく，D に対する正当性を厳密に議論できる世界で Prog を改善することができる．
具体的には （トリビアルな例だけど） 結合法則
(append *A *B *C), (append *X *C *Z) ==> (append *X *A *D), (append *D *B *Z)
みたいな手続きは，Prolog では絶対に探索できない，その正しさも証明できない．
ET の理論では，D から直接得られる，正しさが証明されたET ルールを，いわば公理のルールとして,
上のルールも ET ルールであることが証明できる．右辺と左辺を，最初に得られた ET ルールで展開していって，同じ単位節が得られれば，これもまた ET ルール．そして上のルールを ET ルールとして Prog に追加することができる．D は無変更なので，相変わらず D に対する正当性は完璧に保存されているし，議論できる．このようにして，Prog を膨らませていくことにより，より良い手続きを探索することができる．
そもそも Prolog はホーン節の世界だから，ヘッドは一個だけしか許されないんだけど．
そういう狭さは，まぁ本質ではない．CHR とか，Prolog の後継のような言語は，ヘッド*部* に複数の制約の記述を許しているんだけど．CHR も，結局は Prolog と同じ，D と Prog が分かれてないという問題点は解決できていない．
要するに，Prolog も CHR も，ET の世界のごく一部しか表現できない狭い理論ということ （よくある，言語間の優位性戦争なんかとは本質的に異なる．科学的に構造の優位性が証明されている）
Q. 北大の TA ではどんなことを教えているのですか ?
忘れなければ，問題とテキストを印刷して持って行きます．
テキストの一部はここらへんから （ちょっと古い ?）
ETプログラミング入門テキスト(Dルール編)
ETプログラミング入門テキスト(Nルール編) (現在トップからリンク張って無いので，見てよいものなのかは謎だけど)
(ET SITE)
ちょっと今時間無いので，推敲せずにアップ．
簡単 ET 講座 生産者と消費者問題
なんか twitter の方で，並列プログラミングがどうとか，ET 言語に興味があるから教えてとか言われたので，ちょっと書いてみる．
実は北大では ET 言語で「問題解決プログラミング」とか「人工知能プログラミング」（おおげさなタイトルですが，ようするにちょっと複雑な探索アルゴリズムなど）とかいう講義を教えています（僕も TA として，プログラミングとか全く知らない新入生に ET 言語教えてます．下手に他の言語を知らない子達のほうが，素直で吸収が早いと感じます）．
いちおう全学共通科目で，工学部とかに限らず，誰でも受講できます（といっても，やっぱり工学系の子たち = 男子が大半ですが） 普通の，よくあるプログラミング言語の演習というよりも，「問題解決のための一般的な考え方，方法論，要するにアルゴリズムの作り方」を ET 言語を使って教える （アルゴリズムを表現するのに一番適した言語（と少なくとも我々は信じている）だから） ということを目指した講義です．
# 等価変換の理論は，プログラミングという行為を科学的に体系化することを目指しているので，それはつまり原理や方法論が明確で，教育に適したものにもならないといけないという狙いもあります．現在のプログラミング教育ってのは，所詮は「こうやれば，こういうことができます」という膨大な how を詰め込んでるだけで，何の体系化もされてないと思います （結局最後は，個人で本読んで，たくさんコード書いて，読んで，がんばって勉強してね，の世界．属人性が高すぎて，ぜんぜん科学的じゃない職人芸の世界）
うちの研究室は，情報システムの体系的な構築方法について研究してるところなので，いちおう現在のブームのウェブアプリケーションのほうもやっていて，そっちの方の研究している人が作った e-lerning システム(問題投稿とか，自動採点システムとか）を使って運用してます．
ET 言語には，おおざっぱに N ルールと D ルールという二つの記述（プログラムの集合のクラス）があって，そっちのほうでは D プログラムを教えています．これは，おおざっぱに言えば，項書き換え系（パターンマッチが使える関数型言語）なので，それほど面白いものではありません．
# ロードされてるプログラム（ルール集合）を丸ごと取り出したり，ルールを追加削除したりみたいな，自己書き換え（リフレクション)機能や，逐次世界から，並列計算の世界を作って結果を取得するワールド機能とか，いろいろ面白い機能もあるのですが．
なので N プログラムをちょっと書きます．N プログラムは非決定的的計算という計算のクラスを表現するもので，アクターとか並列計算とか定理証明（バックトラッキング）とか，そういうもろもろのモデルを全部含む広大なプログラム空間を扱うことになります．
生産者と消費者問題ってのは，並列計算の世界ではわりとポピュラーな例題で．
データの生産者と消費者というそれぞれのプロセスが，勝手にそれぞれ動くわけですが，Java とかみたいに，スレッドとかコルーチンとかのライブラリ使って，明示的にセマフォとかで共有資源をロックしたり，準備ができるまで待ったり，準備ができたらシグナルとか発行してプロセス起こして… とかやるのは大変なわけです．
消費者が要求したら生産者が動く，生産者が作り終わったら消費者が動くという感じで，勝手に協調動作してくれるとうれしいわけです．
N プログラムでは，ガード部で自動的に同期が取られる （条件を満たすまで待機する） ので，こういう問題が非常に素直に書けます．明示的な同期処理とかは一切要りません．単に，計算を進めるにあたり，必要な条件を記述するだけ．
メッセージのやり取りには，論理変数が使われます（GHC/KL1 からの伝統）論理変数が具体化されるまで，自動的に同期が取られます．論理変数にメッセージを含む未完成データ構造を具体化し続けることで，自動的な同期と要求駆動計算が実現されます．
未完成データ構造ってのは，*msg = (need | *X) みたいな感じで，リストをインクリメンタルに作っていくという，Prolog の伝統芸ですね （差分リストとかのテクニックでも使われまくります）
具体的なプログラムは，こんな感じです．実行には ETI というインタプリタが必要です．Windows 版だったら，ダウンロードしてインストーラを起動すれば簡単にインストールできますし，日本語もちゃんと通ります (講義で使ってる e-lerning system は，全部これで動いているので，それなりに実績もあります)．Linux 版とかは，中に DSO ライブラリが入ってるので LD_LIBRARYPATH が通った場所にライブラリをインストールして，展開するだけで動くはず．
ただリスト作るだけだとつまらないので，一応 fizzbuzz にしてみました．
Scheme とかでも同じようなプログラムは書けますけど，このプログラムは生産者/消費者の形に書いてあるので，全てのリストが作られる前に，並列で加工者 (filter) や表示者 (printer) まで動くところが，ちょっと面白いところです．
上のプログラムは GHC/KL1 ライクな感じですが，N プログラムの場合はマルチヘッドの書き換えルールが使えるので，論理変数を使わないで，こんな感じにも書けます．メッセージ通信で協調動作させる代わりに，マルチヘッドルールでいきなりまとめて書き換えます．
今回は使ってませんが，それぞれのルールごとに優先度を付けることができるので，柔軟に計算パスを制御することができます （複数のボディに展開されるルールなどは，同じ優先度で適用されると大量の空間を消費するので，優先度を下げるのが普通）
実行過程は，こんな感じで，全てのルールが同じ優先度で，動ける人から動く感じの並列プログラム（今回は単一 CPU マシンで逐次実行のインタプリタで動かしたので，スレッドですが）になってます．ET の実行モデルでは，問題を確定節という，計算を行うのに適した性質を持つ論理式の一種で記述して，それを ET ルールで書き換えることによって計算が進みます．
ルールのヘッド部にパターンが入ってるので，変数だとリストパターンを満たせないので，どっか他のプロセスに変数が具体化されるまで，勝手に待機して同期を取ります．GHC/KL1 よりも，より徹底したルール型の言語の ET は，並列計算が簡単に書けるというか，最初から全てが並列であり非決定的計算という世界です．N プログラムだと，ヘッドがアトム集合になるので，確定節中のヘッドの選び方 (Prolog とかの SLDR と違って，アトムの選択順序が固定されてない．言語によって計算順序が規定されるのではなく，処理内容によって柔軟に変化する，コンテンツドリブン型計算) と，ルールの選択順序において非決定性が生まれます （計算パスが分岐しまくる）．
# ただし，ETI の上で実行する際には，それだといくらなんでも処理効率が悪すぎるので，デフォルトでは理論よりも多少狭いクラスのプログラムに限定されています．一応，全通り計算が可能なモードもありますが．これだと，ワンステップ書き換えごとに大量に計算世界（ワールド）が分岐することになるので，激しく効率は悪いです．そのぶん，非常に強力なプログラムが書けるわけですが．
この動ける人から動くという制約が，関数型の方とかだとモナドとかで定式化されるのかな，という気もします （プロセスが全部並列に非決定的に動いても，一定の制約があるので，正しい順番で出力される）ET の理論では，全てが確定節の書き換えモデル（等価変換）で定式化されてます．
# 個人的には，圏論とか大げさな道具を持ってこなくても，単純な原理だけで説明できるのならばそっちのほうがエレガントだと思ってます．ここら辺の感覚は個人のバックグランドに依存するので，人それぞれだと思いますが （圏論は，現代の，少なくとも情報系のカリキュラムでは，まだそれほどポピュラーではないと思います．50 年後はどうだかわかりませんが）
実は北大では ET 言語で「問題解決プログラミング」とか「人工知能プログラミング」（おおげさなタイトルですが，ようするにちょっと複雑な探索アルゴリズムなど）とかいう講義を教えています（僕も TA として，プログラミングとか全く知らない新入生に ET 言語教えてます．下手に他の言語を知らない子達のほうが，素直で吸収が早いと感じます）．
いちおう全学共通科目で，工学部とかに限らず，誰でも受講できます（といっても，やっぱり工学系の子たち = 男子が大半ですが） 普通の，よくあるプログラミング言語の演習というよりも，「問題解決のための一般的な考え方，方法論，要するにアルゴリズムの作り方」を ET 言語を使って教える （アルゴリズムを表現するのに一番適した言語（と少なくとも我々は信じている）だから） ということを目指した講義です．
# 等価変換の理論は，プログラミングという行為を科学的に体系化することを目指しているので，それはつまり原理や方法論が明確で，教育に適したものにもならないといけないという狙いもあります．現在のプログラミング教育ってのは，所詮は「こうやれば，こういうことができます」という膨大な how を詰め込んでるだけで，何の体系化もされてないと思います （結局最後は，個人で本読んで，たくさんコード書いて，読んで，がんばって勉強してね，の世界．属人性が高すぎて，ぜんぜん科学的じゃない職人芸の世界）
うちの研究室は，情報システムの体系的な構築方法について研究してるところなので，いちおう現在のブームのウェブアプリケーションのほうもやっていて，そっちの方の研究している人が作った e-lerning システム(問題投稿とか，自動採点システムとか）を使って運用してます．
ET 言語には，おおざっぱに N ルールと D ルールという二つの記述（プログラムの集合のクラス）があって，そっちのほうでは D プログラムを教えています．これは，おおざっぱに言えば，項書き換え系（パターンマッチが使える関数型言語）なので，それほど面白いものではありません．
# ロードされてるプログラム（ルール集合）を丸ごと取り出したり，ルールを追加削除したりみたいな，自己書き換え（リフレクション)機能や，逐次世界から，並列計算の世界を作って結果を取得するワールド機能とか，いろいろ面白い機能もあるのですが．
なので N プログラムをちょっと書きます．N プログラムは非決定的的計算という計算のクラスを表現するもので，アクターとか並列計算とか定理証明（バックトラッキング）とか，そういうもろもろのモデルを全部含む広大なプログラム空間を扱うことになります．
生産者と消費者問題ってのは，並列計算の世界ではわりとポピュラーな例題で．
データの生産者と消費者というそれぞれのプロセスが，勝手にそれぞれ動くわけですが，Java とかみたいに，スレッドとかコルーチンとかのライブラリ使って，明示的にセマフォとかで共有資源をロックしたり，準備ができるまで待ったり，準備ができたらシグナルとか発行してプロセス起こして… とかやるのは大変なわけです．
消費者が要求したら生産者が動く，生産者が作り終わったら消費者が動くという感じで，勝手に協調動作してくれるとうれしいわけです．
N プログラムでは，ガード部で自動的に同期が取られる （条件を満たすまで待機する） ので，こういう問題が非常に素直に書けます．明示的な同期処理とかは一切要りません．単に，計算を進めるにあたり，必要な条件を記述するだけ．
メッセージのやり取りには，論理変数が使われます（GHC/KL1 からの伝統）論理変数が具体化されるまで，自動的に同期が取られます．論理変数にメッセージを含む未完成データ構造を具体化し続けることで，自動的な同期と要求駆動計算が実現されます．
未完成データ構造ってのは，*msg = (need | *X) みたいな感じで，リストをインクリメンタルに作っていくという，Prolog の伝統芸ですね （差分リストとかのテクニックでも使われまくります）
具体的なプログラムは，こんな感じです．実行には ETI というインタプリタが必要です．Windows 版だったら，ダウンロードしてインストーラを起動すれば簡単にインストールできますし，日本語もちゃんと通ります (講義で使ってる e-lerning system は，全部これで動いているので，それなりに実績もあります)．Linux 版とかは，中に DSO ライブラリが入ってるので LD_LIBRARYPATH が通った場所にライブラリをインストールして，展開するだけで動くはず．
(fizzbuzz) ==> (generator *msgQ), // 生産者
(take 100 *msgQ *x), // 消費者
(fizzbuzz *x *fizzbuzz), // 加工者
(printList *fizzbuzz). // 表示者
// 1 から数を生産開始
(generator *msg)
==> {(= *msg (1 | *msg1))}, (generator 1 *msg1).
// 要求メッセージがきたら生産
(generator *n (need | *msg))
==> {(add *n 1 *n1), (= *msg (*n1 | *msg1))}, (generator *n1 *msg1).
// 停止メッセージがきたら生産終了
(generator *n (halt | ?)) ==>.
// 生産済みだったら取るだけ
(take *n (*m | *msg) *x)
==> {(= *x (*m | *x1)),(sub *n 1 *n1)}, (take *n1 *msg *x1).
// 取り終わったら終了メッセージを送る
(take 0 *msg *x),{(pvar *msg)}
==> {(= *msg (halt)), (= *x ())}.
// メッセージを送って生産してもらう
(take *n *msg *x), {(> *n 0), (pvar *msg), (= *msg (need | *msg1))}
==> (take *n *msg1 *x).
// できたそばから表示
(printList (*x | *xs))
==> {(format "/a " (*x))}, (printList *xs).
(printList ()) ==> {(format "/n" ())}.
// fizzbuzz filter
(fizzbuzz (*x | *xs) *fizzbuzz), {(:= 0 (mod *x 3)), (:= 0 (mod *x 5))}
==> {(= *fizzbuzz (FizzBuzz | *fizzbuzz1))}, (fizzbuzz *xs *fizzbuzz1).
(fizzbuzz (*x | *xs) *fizzbuzz), {(:= 0 (mod *x 3)), (not (:= 0 (mod *x 5)))}
==> {(= *fizzbuzz (Fizz | *fizzbuzz1))}, (fizzbuzz *xs *fizzbuzz1).
(fizzbuzz (*x | *xs) *fizzbuzz), {(not (:= 0 (mod *x 3))), (:= 0 (mod *x 5))}
==> {(= *fizzbuzz (Buzz | *fizzbuzz1))}, (fizzbuzz *xs *fizzbuzz1).
(fizzbuzz (*x | *xs) *fizzbuzz), {(not (:= 0 (mod *x 3))), (not (:= 0 (mod *x 5)))}
==> {(= *fizzbuzz (*x | *fizzbuzz1))}, (fizzbuzz *xs *fizzbuzz1).
(fizzbuzz () *fizzbuzz) ==> {(= *fizzbuzz ())}.
ただリスト作るだけだとつまらないので，一応 fizzbuzz にしてみました．
Scheme とかでも同じようなプログラムは書けますけど，このプログラムは生産者/消費者の形に書いてあるので，全てのリストが作られる前に，並列で加工者 (filter) や表示者 (printer) まで動くところが，ちょっと面白いところです．
上のプログラムは GHC/KL1 ライクな感じですが，N プログラムの場合はマルチヘッドの書き換えルールが使えるので，論理変数を使わないで，こんな感じにも書けます．メッセージ通信で協調動作させる代わりに，マルチヘッドルールでいきなりまとめて書き換えます．
(fizzbuzz *n) ==> (gen 1 *x), (take *n), (filter *x *l), (printer *l).
(gen *i *x), (take *n)
==> {(> *n 0), (= *x (*i | *x1)), (add *i 1 *i1), (sub *n 1 *n1)},(gen *i1 *x1), (take *n1).
(gen *i *x), (take 0) ==> {(= *x ())}.
// 以下，同じ
(filter (*x | *xs) *filter), {(:= 0 (mod *x 3)), (:= 0 (mod *x 5))}
==> {(= *filter (filter | *filter1))}, (filter *xs *filter1).
(filter (*x | *xs) *filter), {(:= 0 (mod *x 3)), (not (:= 0 (mod *x 5)))}
==> {(= *filter (Fizz | *filter1))}, (filter *xs *filter1).
(filter (*x | *xs) *filter), {(not (:= 0 (mod *x 3))), (:= 0 (mod *x 5))}
==> {(= *filter (Buzz | *filter1))}, (filter *xs *filter1).
(filter (*x | *xs) *filter), {(not (:= 0 (mod *x 3))), (not (:= 0 (mod *x 5)))}
==> {(= *filter (*x | *filter1))}, (filter *xs *filter1).
(filter () *filter) ==> {(= *filter ())}.
(printer (*x | *xs))
==> {(format "/a " (*x))}, (printer *xs).
(printer ()) ==> {(format "/n" ())}.
今回は使ってませんが，それぞれのルールごとに優先度を付けることができるので，柔軟に計算パスを制御することができます （複数のボディに展開されるルールなどは，同じ優先度で適用されると大量の空間を消費するので，優先度を下げるのが普通）
実行過程は，こんな感じで，全てのルールが同じ優先度で，動ける人から動く感じの並列プログラム（今回は単一 CPU マシンで逐次実行のインタプリタで動かしたので，スレッドですが）になってます．ET の実行モデルでは，問題を確定節という，計算を行うのに適した性質を持つ論理式の一種で記述して，それを ET ルールで書き換えることによって計算が進みます．
[D]>include "C:\\Documents and Settings\\aloha.IIC\\デスクトップ\\fizzbuzz2.eti"
[D]>n
Execution mode "N"
[N]>dn
[N:N]>(fizzbuzz 4)
-------------------------N execution ---------------------
============================
(ans (fizzbuzz 4))<-(gen 1 *A), (take 4), (filter *A *B), (printer *B).
============================
(ans (fizzbuzz 4))<-(filter (1 | *A) *B), (printer *B), (gen 2 *A), (take 3).
============================
(ans (fizzbuzz 4))<-(printer (1 | *A)), (gen 2 *B), (take 3), (filter *B *A).
1 ============================
(ans (fizzbuzz 4))<-(gen 2 *A), (take 3), (filter *A *B), (printer *B).
============================
(ans (fizzbuzz 4))<-(filter (2 | *A) *B), (printer *B), (gen 3 *A), (take 2).
============================
(ans (fizzbuzz 4))<-(printer (2 | *A)), (gen 3 *B), (take 2), (filter *B *A).
2 ============================
(ans (fizzbuzz 4))<-(gen 3 *A), (take 2), (filter *A *B), (printer *B).
============================
(ans (fizzbuzz 4))<-(filter (3 | *A) *B), (printer *B), (gen 4 *A), (take 1).
============================
(ans (fizzbuzz 4))<-(printer (Fizz | *A)), (gen 4 *B), (take 1), (filter *B *A).
Fizz ============================
(ans (fizzbuzz 4))<-(gen 4 *A), (take 1), (filter *A *B), (printer *B).
============================
(ans (fizzbuzz 4))<-(filter (4 | *A) *B), (printer *B), (gen 5 *A), (take 0).
============================
(ans (fizzbuzz 4))<-(printer (4 | *A)), (gen 5 *B), (take 0), (filter *B *A).
4 ============================
(ans (fizzbuzz 4))<-(gen 5 *A), (take 0), (filter *A *B), (printer *B).
============================
----------------------------------------------------------
execution time: 31 [msec]
ルールのヘッド部にパターンが入ってるので，変数だとリストパターンを満たせないので，どっか他のプロセスに変数が具体化されるまで，勝手に待機して同期を取ります．GHC/KL1 よりも，より徹底したルール型の言語の ET は，並列計算が簡単に書けるというか，最初から全てが並列であり非決定的計算という世界です．N プログラムだと，ヘッドがアトム集合になるので，確定節中のヘッドの選び方 (Prolog とかの SLDR と違って，アトムの選択順序が固定されてない．言語によって計算順序が規定されるのではなく，処理内容によって柔軟に変化する，コンテンツドリブン型計算) と，ルールの選択順序において非決定性が生まれます （計算パスが分岐しまくる）．
# ただし，ETI の上で実行する際には，それだといくらなんでも処理効率が悪すぎるので，デフォルトでは理論よりも多少狭いクラスのプログラムに限定されています．一応，全通り計算が可能なモードもありますが．これだと，ワンステップ書き換えごとに大量に計算世界（ワールド）が分岐することになるので，激しく効率は悪いです．そのぶん，非常に強力なプログラムが書けるわけですが．
この動ける人から動くという制約が，関数型の方とかだとモナドとかで定式化されるのかな，という気もします （プロセスが全部並列に非決定的に動いても，一定の制約があるので，正しい順番で出力される）ET の理論では，全てが確定節の書き換えモデル（等価変換）で定式化されてます．
# 個人的には，圏論とか大げさな道具を持ってこなくても，単純な原理だけで説明できるのならばそっちのほうがエレガントだと思ってます．ここら辺の感覚は個人のバックグランドに依存するので，人それぞれだと思いますが （圏論は，現代の，少なくとも情報系のカリキュラムでは，まだそれほどポピュラーではないと思います．50 年後はどうだかわかりませんが）
ET 用の vim syntax ファイル
limbo の vim 用 syntax file を眺めていたら思っていたよりも簡単そうだったので，試しに ET 用のキーワードファイルを書いてみた．単に強調表示されるだけで，オートインデントとかは何もしてない．整数･浮動小数点数とかのマッチングもテキトーで (真面目に書こうとすると，けっこう大変)，とりあえず書いてみた感漂う作品となっております．
あと，S 式単位の移動とか操作とかは，テキストオブジェクトとかいう vim の機能を使うと普通にできるらしいんだけど，まだ良くわかって無い．
昔，lisp モードを改造しようと思ったんだけど，でかすぎて断念したんだよなぁ．
というわけで，S 式のサポートも，set sm (() {} などの show match) とかを微妙にしているだけ．
参考 : Vim documentation: syntax
使い方は，Windows だったら C:\Program Files\vim-6.4.006-w32j\runtime\syntax とかに以下を et.vim とかで保存して，runtime\filetype.vim の augroup filetypedetect というところの下あたりに au BufNewFile,BufRead *.eti,*.etc setf et とか書けば OK です．
あと，S 式単位の移動とか操作とかは，テキストオブジェクトとかいう vim の機能を使うと普通にできるらしいんだけど，まだ良くわかって無い．
wiliki?leque Editing with Emacs
ときどき UTF-8 なテキストを編集しなくてはいけないことがあって nvi だといろいろ不便なのでこれを機に Emacs に乗り換えた（vim も候補にあがったけれど、vim script があまり好きになれそうにないのと、:set lisp しても ( や ) が S式単位でうごいてくれなかったので×）。
昔，lisp モードを改造しようと思ったんだけど，でかすぎて断念したんだよなぁ．
というわけで，S 式のサポートも，set sm (() {} などの show match) とかを微妙にしているだけ．
参考 : Vim documentation: syntax
使い方は，Windows だったら C:\Program Files\vim-6.4.006-w32j\runtime\syntax とかに以下を et.vim とかで保存して，runtime\filetype.vim の augroup filetypedetect というところの下あたりに au BufNewFile,BufRead *.eti,*.etc setf et とか書けば OK です．
はじめてのかたちぇっか
Prolog なら簡単に型チェッカが書ける，とか言ったが，すまん．ありゃ嘘だった．
まぁ，Prolog だと，プログラムを項として扱うと分解 (マッチング) が面倒だし，リストとして扱うとカンマで区切らないといけないから，どっちにしろ TAPL とかで扱っている形とかけ離れてしまうという．
そんなこんなで，いわば S 式で書く Prolog，ET 言語の出番ですな．一番使い慣れてるし．
例題プログラムは，TAPL の let-polymorphism のやつ．
というやつ．
しっかし，パーサを書くのは面倒なので，手抜きさせてください．問題を S 式で与えます．あと，ET では，*var みたいにアスタリスクを付けると変数になるので，識別子に制限はありません (個人的には，乗算やポインタのイメージが付きまとうので，?var とかの方が良かったのではないかと思う．ちなみに ? は，他の全ての変数にマッチしないことが保障される無名変数 (ワイルドカード) として扱われます)
あと，推論規則は，テキトーに必要最小限のを，パターンマッチ使いまくりで，IF-THEN ルールをひたすら書いて行きます．
んでまぁ，あとは
とか書きたくなるところですが，これだと *a と *b で型変数が共有されてしまうので，let-polymorphism にならない ！！
# *a で *F_a が (Num -> Num) になると，*b での *F_b の型は (Bool -> Bool) だから，*F_a と *F_b が同じ *F として共有されてしまうと全体としては不整合が起きる．
というわけで，変数をコピーして，フレッシュな変数を用意しましょうという話．
ちなみに，定義されてない述語，number/1 と print/1 と =/2 (unification) と copy/2 は組み込みルールです．
実行してみると，こんな感じ．
まぁ，S 式とパターンマッチによるルール記述とユニフィケーションと論理変数があると，定理証明器とか型チェッカはすごく簡単に (いや，もちろん，複雑な型体系になったら，それなりに大変だけど，他の言語とかに比べたら相対的に) 書けますよと．
パターンマッチは劇的にプログラムを宣言的にします．
あと，型推論の本質は記号によって組み立てられた構造のユニフィケーションなので．
今回使ったのは，ET の D (eterministic) ルールというサブセットのみで，他にもまぁいろいろ機能はあります．面倒だから説明しないけど(駄目)
たとえば論理変数だけだと表現力に乏しいので，情報 (制約) 付き変数とか．
D ルールのみだと，基本的に Erlang とほとんど同じだと思います．構文とかもかなり似ているような．ただ，値への簡約ではなく，論理変数経由で計算結果を伝えていく点は違いますけど．
まぁ，Prolog だと，プログラムを項として扱うと分解 (マッチング) が面倒だし，リストとして扱うとカンマで区切らないといけないから，どっちにしろ TAPL とかで扱っている形とかけ離れてしまうという．
そんなこんなで，いわば S 式で書く Prolog，ET 言語の出番ですな．一番使い慣れてるし．
例題プログラムは，TAPL の let-polymorphism のやつ．
let double = λ f:X -> X . λ a . f(f(a)) in
let a = double succ 1 in
let b = double not true in
...
というやつ．
しっかし，パーサを書くのは面倒なので，手抜きさせてください．問題を S 式で与えます．あと，ET では，*var みたいにアスタリスクを付けると変数になるので，識別子に制限はありません (個人的には，乗算やポインタのイメージが付きまとうので，?var とかの方が良かったのではないかと思う．ちなみに ? は，他の全ての変数にマッチしないことが保障される無名変数 (ワイルドカード) として扱われます)
(test) --> (= *F (*X -> *X)), // f:X -> X のつもり．下の式にインラインで書いても良いけど
(= *double (lambda (*F *A) (*F (*F *A)))),
(= *a (*double succ 1)),
(= *b (*double not true)),
(typeInf *a),
(typeInf *b).
あと，推論規則は，テキトーに必要最小限のを，パターンマッチ使いまくりで，IF-THEN ルールをひたすら書いて行きます．
(typeInf1 () ()) -->.
(typeInf1 (*F | *rest) (succ | *rest1))
-->
(= *F (Num -> Num)),
(typeInf1 *rest *rest1).
(typeInf1 (*F | *rest) (not | *rest1))
-->
(= *F (Bool -> Bool)),
(typeInf1 *rest *rest1).
(typeInf1 (*A | *rest) (true | *rest1))
-->
(= *A Bool),
(typeInf1 *rest *rest1).
(typeInf1 (*A | *rest) (*n | *rest1)),
{(number *n)}
-->
(= *A Num),
(typeInf1 *rest *rest1).
(typeInf2 ((Num -> Num) *X) *R)
-->
(typeInf2 *X Num),
(= *R Num).
(typeInf2 ((Bool -> Bool) *X) *R)
-->
(typeInf2 *X Bool),
(= *R Bool).
(typeInf2 Bool *R)
-->
(= *R Bool).
(typeInf2 Num *R)
-->
(= *R Num).
んでまぁ，あとは
// 間違い ！！
(typeInf ((lambda *parm *body) | *args))
-->
(typeInf1 *parm *args),
(print (lambda *parm *body)).
とか書きたくなるところですが，これだと *a と *b で型変数が共有されてしまうので，let-polymorphism にならない ！！
# *a で *F_a が (Num -> Num) になると，*b での *F_b の型は (Bool -> Bool) だから，*F_a と *F_b が同じ *F として共有されてしまうと全体としては不整合が起きる．
というわけで，変数をコピーして，フレッシュな変数を用意しましょうという話．
(typeInf ((lambda *parm *body) | *args))
-->
// コピーしてフレッシュな変数を使う
(copy (*parm *body) (*parm1 *body1)),
(typeInf1 *parm1 *args),
(print (lambda *parm1 *body1)),
(typeInf2 *body1 *result),
(print (*parm1 => *result)).
ちなみに，定義されてない述語，number/1 と print/1 と =/2 (unification) と copy/2 は組み込みルールです．
実行してみると，こんな感じ．
[D]>load "C:\\Documents and Settings\\aloha\\デスクトップ\\typeInf.eti"
[D]>(test)
-------------------------D execution ---------------------
(lambda ((Num -> Num) Num) ((Num -> Num) ((Num -> Num) Num)))
(((Num -> Num) Num) => Num)
(lambda ((Bool -> Bool) Bool) ((Bool -> Bool) ((Bool -> Bool) Bool)))
(((Bool -> Bool) Bool) => Bool)
----------------------------------------------------------
succeeded.
(test)
まぁ，S 式とパターンマッチによるルール記述とユニフィケーションと論理変数があると，定理証明器とか型チェッカはすごく簡単に (いや，もちろん，複雑な型体系になったら，それなりに大変だけど，他の言語とかに比べたら相対的に) 書けますよと．
パターンマッチは劇的にプログラムを宣言的にします．
あと，型推論の本質は記号によって組み立てられた構造のユニフィケーションなので．
今回使ったのは，ET の D (eterministic) ルールというサブセットのみで，他にもまぁいろいろ機能はあります．面倒だから説明しないけど(駄目)
たとえば論理変数だけだと表現力に乏しいので，情報 (制約) 付き変数とか．
D ルールのみだと，基本的に Erlang とほとんど同じだと思います．構文とかもかなり似ているような．ただ，値への簡約ではなく，論理変数経由で計算結果を伝えていく点は違いますけど．
lambda 式の Just-In-Time コンパイラコンパイラ libjit 版
コンパイラコンパイラ (ラムダ式をコンパイルする関数を生成する) のターゲットを libjit に変更してみた．
まぁ，実際に吐かれたコードがコンパイル通るかどうかは確かめてないけど (テキトー) GNU lightning と違って，レジスタアロケーションまではやる必要が無いので非常に楽ですな．
いやぁ，JIT ライブラリは素晴らしいですね．クロージャ変換とかまで真面目に実装する気はあんまり無いのですが，簡単なクロージャならば返せる程度まではやってみても良いかも．
(lambda (*a) (lambda (*x) (+ *a *x)))
とか程度を想定．上のラムダ式をコンパイルすると，shinh 先生が BINARY HACKS 「C でポータブルなカリー化」で例題にしていたようなコードが吐かれると，けっこう面白いなと．
ようするに，関数を作る関数を作る関数をラムダ式をコンパイルして吐けば良いわけで．技術的には (libjit を使えば) そんなに難しいことじゃない．
しかし，ま，ちょっと今はあんまり時間無いので，今日はこの辺で．
それにしても，BINARY HACKS は素晴らしく面白いですね．これを読んでると，何でもできそうな気がしてきて，夜眠れなくなるぐらい興奮します ｗ
(半分本当．実際今日寝不足で… いや，BH のせいだけではなく，たまたまなんですが．あまりにも研究をやる気がでなかったので，だらだらコンパイラ書いて現実逃避してた (クズ院生))
とりあえず，objcpy は素晴らしすぎるということがよくわかりました．リソースやソースコードって，バイナリに直接埋め込めたんだなぁ… なんて便利．
まぁ，あたりまえの話なんですけど，VM とか OS とか libc を捨てた古き良き世界では，プログラマはまさしく全能なんですよね．障害は自分の能力の限界だけ．この自由にプログラムを書いてる感覚こそが，BIN HACK の最大の醍醐味のわけで．今時の箱庭の中で普通に暮らしていると，なかなか味わえないと思いますが，それはけっこうもったいないというか．
プログラミング言語 C や SICP や Lions 本が名著と呼ばれるのは，そこらへんの Good-Old-Fashioned な精神，プログラマが魔術師の尊称だった時代の価値観が，世間の価値観に流され，プログラマが単なるコーダの別称となってしまった現在においてもなお垣間見れるからだと思います．
プログラミング言語もスタイルも，ハードウェアもソフトウェアも，形があるものはいつか必ず滅び，やがては消えて行ってしまいます．しかし，現在という時代を作り上げてきた，未来を創った人々の黄金のような精神は永遠です．どれだけ内容が古びようとも，世間の価値観が移り変わろうとも，けして失われない何かがある．そのような本が名著と呼ばれるのではないでしょうか．
ようこそ… バイナリの世界へ…
[D]>(compile (lambda (*x *y *z) (set! *a (+ *z (+ *x *y)))))
-------------------------D execution ---------------------
/* 変換過程
(lambda (*A *B *C) (set! *D (+ *C (+ *A *B))))
=>
(lambda (*A *B *C) (set! *E (+ *A *B)) (set! *F (+ *C *E)) (set! *D *F) *D)
=>
(lambda ("v0" "v1" "v2") (set! "v3" (+ "v0" "v1")) (set! "v4" (+ "v2" "v3")) (set! "v5" "v4") "v5")
*/
#include <stdio.h>
#include <jit/jit.h>
int main(int argc, char **argv) {
jit_context_t context = jit_context_create();
jit_type_t params[3];
jit_type_t signature;
jit_function_t function;
jit_value_t v0, v1, v2, v3, v4, v5;
jit_int arg0, arg1, arg2;
void *args[3];
jit_int result;
jit_context_build_start(context);
params[0] = jit_type_int;
params[1] = jit_type_int;
params[2] = jit_type_int;
signature = jit_type_create_signature(jit_abi_cdecl, jit_type_int, params, 3, 1);
signature = jit_type_create_signature(jit_abi_cdecl, jit_type_int, params, 3, 1);
function = jit_function_create(context, signature);
v3 = jit_insn_add(function, v0, v1);
v4 = jit_insn_add(function, v2, v3);
jit_insn_store(function, v5, v4);
jit_insn_return(function, v5);
jit_function_compile(function);
jit_context_build_end(context);
arg0 = 2;
args[0] = &arg0;
arg1 = 3;
args[1] = &arg1;
arg2 = 4;
args[2] = &arg2;
jit_function_apply(function, args, &result);
puts("/* (lambda (*A *B *C) (set! *D (+ *C (+ *A *B)))) */");
printf("(lambda (1 2 3)) => %d\n", (int)result);
jit_context_destroy(context);
return 0;
}
----------------------------------------------------------
succeeded.
まぁ，実際に吐かれたコードがコンパイル通るかどうかは確かめてないけど (テキトー) GNU lightning と違って，レジスタアロケーションまではやる必要が無いので非常に楽ですな．
いやぁ，JIT ライブラリは素晴らしいですね．クロージャ変換とかまで真面目に実装する気はあんまり無いのですが，簡単なクロージャならば返せる程度まではやってみても良いかも．
(lambda (*a) (lambda (*x) (+ *a *x)))
とか程度を想定．上のラムダ式をコンパイルすると，shinh 先生が BINARY HACKS 「C でポータブルなカリー化」で例題にしていたようなコードが吐かれると，けっこう面白いなと．
ようするに，関数を作る関数を作る関数をラムダ式をコンパイルして吐けば良いわけで．技術的には (libjit を使えば) そんなに難しいことじゃない．
しかし，ま，ちょっと今はあんまり時間無いので，今日はこの辺で．
それにしても，BINARY HACKS は素晴らしく面白いですね．これを読んでると，何でもできそうな気がしてきて，夜眠れなくなるぐらい興奮します ｗ
(半分本当．実際今日寝不足で… いや，BH のせいだけではなく，たまたまなんですが．あまりにも研究をやる気がでなかったので，だらだらコンパイラ書いて現実逃避してた (クズ院生))
とりあえず，objcpy は素晴らしすぎるということがよくわかりました．リソースやソースコードって，バイナリに直接埋め込めたんだなぁ… なんて便利．
まぁ，あたりまえの話なんですけど，VM とか OS とか libc を捨てた古き良き世界では，プログラマはまさしく全能なんですよね．障害は自分の能力の限界だけ．この自由にプログラムを書いてる感覚こそが，BIN HACK の最大の醍醐味のわけで．今時の箱庭の中で普通に暮らしていると，なかなか味わえないと思いますが，それはけっこうもったいないというか．
プログラミング言語 C や SICP や Lions 本が名著と呼ばれるのは，そこらへんの Good-Old-Fashioned な精神，プログラマが魔術師の尊称だった時代の価値観が，世間の価値観に流され，プログラマが単なるコーダの別称となってしまった現在においてもなお垣間見れるからだと思います．
プログラミング言語もスタイルも，ハードウェアもソフトウェアも，形があるものはいつか必ず滅び，やがては消えて行ってしまいます．しかし，現在という時代を作り上げてきた，未来を創った人々の黄金のような精神は永遠です．どれだけ内容が古びようとも，世間の価値観が移り変わろうとも，けして失われない何かがある．そのような本が名著と呼ばれるのではないでしょうか．
ようこそ… バイナリの世界へ…
