Curryにへんしん！ - プログラマーになりたい。

とりあえずインストール

環境はInterl Macなのですが、
埋もれた日々の足音.tar.gz » ヘタレCurry奮闘記インストール編 115,781
に従えばいいらしいと言われた。

で、ここまでやったところで、

まずは，AquaCurryのページへ行って，Downloadから．AquaCurry-1.0.dmg.gzをパクってこよう．遠慮はいらないぜ！作者じゃないのに偉そうですね．PPCって書いてあるけど，うちのIntel Macでは動いているので平気かもしれません．そいつを解凍してインストールする前に，GMP.frameworkってのを入れておく必要があります．そのために次の2つのコマンドを実行しておく．

(こいつと)
curl -LO http://haskell.org/ghc/dist/mac_frameworks/GMP-framework.zip
(こいつ)
unzip GMP-framework.zip -d /Library/Frameworks

とか書いてあるのを発見。それにしても、さえきくんの才気走った文章には毎度、頭が沸騰させられます。
でもうまく動かない…。起動はするけど、buildとかしようとするとGMP.frameworkがどうのこうの。

(ま、とりあえず、これでインストールが完了したっぽい。)

cyiを終了する

$ cyi
    _____ __ __
   / ___/ |  / _               Muenster Curry Compiler
  / /     | / | |              Version 0.9.11, Copyright (c) 1998-2007
 / /___  / /  | |
 \____/ /_/   |_|              Type :h for help

Prelude>

から先にどうやって進むかわからない。
とりあえず「:h」と打つ。とりあえず終了は「:q」だとわかる。

プログラム例を動かしたい

プログラム例のページがあるので

rev.curry: list concatenation and naive reverse

とりあえず1つめを動かしたい。

論理型プログラミング

(調べたけどよくわからないので後回しにしました。)

論理プログラミング（Logic Programming）とは、表明とゴールからパターンによる手続き呼び出しを行うプログラミング手法

解決すべき問題とは、新たな仮説が既存の理論で説明できるかどうかを問うことと等しい。論理は問題が真か偽かを証明する方法を提供する。証明構築過程は明確であり、論理は問題に答える信頼できる方法と見なされている。

ほーう(よくわかってない)。

ホーン節（英: Horn clause）とは、数理論理学において、せいぜい1つの肯定形のリテラルを持つ節（リテラルの論理和）

リテラルって…？

論理式の正確な定義は、対象とする形式論理に依存するが、典型的な例（一階述語論理）では以下のようになる。論理式は、特定の言語として定義され、その言語は個体定項、関数記号、述語記号などの集合であり、関数および述語記号はとりうるアリティー（引数）が決まっている。
ここで、項は以下のように帰納的に定義される。
1. 変項
2. 個体定項
3. f(t1,...,tn)、ここで、f はアリティー n の関数記号で、t1,...,tn も項である。
さらに、論理式は以下のように帰納的に定義される。
1. t1=t2、ここで、t1 と t2 は項
2. R(t1,...,tn)、ここで R はアリティー n の述語記号で、t1,...,tn は項
…
これらの定義のうち、最初の2つは原子論理式と呼ばれる。また、原子論理式およびその否定をリテラルと呼ぶ。

curryはportsに入ってない

ところで、curryはports *1に入ってないの？
と、思ったので、

$ port search curry

したら…、

Djinn @2006-07-21 (devel)
    Haskell Theorem Prover

なんですか「Djinn」って。Haskell定理証明器…？(関係ないみたいね。)

*1:MacPortsについてはMacPortsでステキなUNIXツールをインストール - はこべブログ ♨を見たりしてください。もっと詳しいことは、http://macwiki.sourceforge.jp/wiki/index.php/MacPortsとか、"MacPortsのサイト"でどうぞ。