あいさつ
こんにちは.
皆さん如何お過ごしでしょうか.
本日の日付を確認致しましたらもう2014年も残り一月半と改めて認識させられ驚いています.
こうも時間の流れが早いと死ぬのもすぐですね.
懸命に生きようと思います.
さて今回はHilbertという論理型プログラミング言語を作りました.
（カジュアルに作ってるように見えますが、割と本気です.）
まだまだやるべき事は本当に多くて、飴ちゃんあげるのでコミッター大募集です.
（今ならカントリーマームもつけるのでお願いします.）
HP: http://hilbert-lang.org/ja/
Github: https://github.com/gogotanaka/Hilbert
前座
世界で一番ピュアで豊かなプログラミング言語
この言語で仮定されているのは恒真（トートロジー）のみです.
（厳密に言うと自然演繹も仮定されていますが.）
当初、自然演繹すら仮定しないのが最もピュアと思い試みましたが、帰って来れなくなりそうだったので思考を止めました.（卒論にでも書きます）しかしそれでも現存するものではこれが最もピュアだと思います.
（Prologとの違いはあちらは論理包含が真である事をベースにプログラムを構築しますがHilbertは公理の仮定によってのみプログラムを構築します. 評価も仮定との論理包含の仮定によって行なうため、至って公理の仮定の範疇となります.）
恒真（トートロジー）とは「Aが真またAが偽」のように各命題の真偽値に依らず常に真である論理式の事で、論理包含の左辺にとっても（仮定としてとっても）右辺の真偽値にしか全体はよらないのでそいう意味で非常にピュア
これは「貧しい」とも取れますが、公理主義的な文脈で言えば
この貧しさこそ豊かさなんですよね.
（貧しく見せる事が大事で内部実装は選言標準化とDPLLアルゴリズムで泥臭くやってる）
恒真（トートロジー）と恒偽（パラドックス）は副作用をもたない.
まず一番心に留めておいて頂きたいのは、
Hilbertに与えられる文字列は全て, 仮定の宣言です.
これ非常に大事なのですが、基本的にHilbertでは仮定の宣言しか許されないのです、
そして仮定の宣言はプログラム空間に副作用をもたらします.
しかし宣言する論理式が恒真（トートロジー）と恒偽（パラドックス）の場合は仮定の宣言ではなく（トートロジーを仮定する意味はないし、パラドックスを仮定するとどんな命題も真になってしまう）その旨をアウトプットするだけという意味で副作用がありません.
（ここでいう副作用というのはプログラム空間上の状態に変化をもたらさないだけでIOはあります）
この機構により仮定から導き出される命題の真偽の確認なども行なえます.
つまり仮定との論理包含をとって副作用があったかないかで命題の真偽値を確認する事が出来ます.
A # 命題Aが真である事の宣言
A -> B # 命題A->Bが真である事の宣言
B? # Aが真かつA-BならばBは真
#=> TRUE
B?というのは((A & (A -> B)) -> B) の糖衣構文にあたります.
論理式に?をつけると宣言した仮定が真である事との論理包含の論理式がトートロジーならTRUEをパラドックスならFALSEをどちらでもなければUNDEFINEDを返します.
Hilbert(ヒルベルト)という名前について
HaskellやErlangと同じノリです.
僕が天才と愛して止まないダフィット・ヒルベルトという演繹主義者の当時、今ほど数学が整理されてなく記号や言葉が恣意的で直感的に用いられていた中行なった偉大な仕事が今に至る、後の100年の著しい発展における基礎付けとなった事への敬意と憧れがこめられています.
彼やヒルベルト学派の姿勢に習いこのプログラミング言語では一切の直感性や恣意さを取り除く用に努めました.
現存するプログラミング言語は直感的で恣意的なのかと言われれば、大きく首を縦にふる事は出来ませんが、言語仕様の末端まで一貫した思想で演繹的に満たされているモノて多くはないですし不十分だと思います. (そいう意味でHaskellやProlog、Rubyは好きです）
有限の立場
やりたい事がありすぎて思想のテンコ盛りなんですが、
軸はPrologと同じく論理型プログラミング言語として設計されておりますが、
普遍妥当な論理式を機械的に導出可能とする公理系と推論法則を言語内部に構築し、実数学の諸概念を離散世界の抽象物に飛ばす機構を目指した言語です.
（これもめっちゃ気に入ってるので大きくしてみた）
日々の計算業務から高度な自動定理証明までお任せという感じです.
実解析に関する公理系は標準ライブラリとして添付してあります.
連言標準形とDPLLアルゴリズム
まあどうやってこの機構を担保しているかと少しお話ししますと、
与えられた論理式はもれなく連言標準形（重否定則とドモルガン則、分配則）に変換され論理包含をとった時に限り、
DPLLアルゴリズムで充足可能性を確認するという事を行なっています.
美しさが大事
処理速度とか並列性とか保守性とか生産性とか気にするあまり美しさを失ってる気がしてならないんですよね、
（そもそもプログラミング言語とはそいうモノだし、これら（処理速度...etc）の要素は重んじられて当然だとは思いますが.）
Hilbertでは美を先鋭し、入力値と返値を楽しむ事に重きを置いています.
しかし「だから何？暇なの？」と一蹴されてしまいますが、
まあ、グウの根も出ません.
Hello world! なんて陽気な事は出来ません
ゴチャゴチャうっさいのでとりあえず雰囲気を見てみましょう.
多くの言語は「Hello world!」という陽気な例から始まりますが、
Hilbertでは三段論法がそれにあたります.
文字列を扱えない事に不十分さを感じるのは僕たちがまだまだ未熟だからなんだと思います.
（適当）
# 三段ロンポー
P -> Q
Q -> R
P -> R ?
=> TRUE
P | Q # PまたはQ
~P # Pではない
Q? # ではQである
=> TRUE
A?
=> UNDEFINED
~A
A?
=>FALSE
A -> B # AならばBである
B -> A ? # BならばAとは限らない
=> UNDEFINED
B -> A # BならばAである
A <-> B ? # AとBは同値である
# 標準の公理系をインポートすれば実数解析なども扱える
postulate zfc_analysis
d/dx x^2
=> 2x
d/dx e^x
=> e^x
S(sin(x)dx)[0..pi]
=> 2
lim[x->oo] 1/x
=> 0
∑[i=1, 10] i
=> 55
与太話
一階述語論理
現在の所、命題論理のみの対応となりますが、
その内一階述語論理またはそのサブセットを導入して
IsHuman(gogotanaka) # gogotanakaは人間である
A[x] IsHuman(x) -> WillDie(x) # 全ての人間は死ぬ
WillDie(gogotanaka)? # gogotanakaは死ぬのか？
#=>true
タノシー
二階述語論理
また二階述語論理も実装出来れば（これは多くの先人達が苦労していますが）
gogotanaka <- HUMAN # gogotanakaは人間である.
A[h<-HUMAN] WillDie(h) # 全ての人間は死ぬ
WillDie(gogotanaka)? # gogotanakaは死ぬのか？
#=>true
ウヒョー
仮定のモジュール化（公理系）
Rubyのクラスシンタックスを真似ます.
Axiom tanaka
A
A->B
end
postulate tanaka #公理系の仮定(事実モジュールのインポート)
ワー
ドキュメント
事実の宣言と事実の評価
?の糖衣構文を用いればHilbertは事実の宣言と事実の確認によって構成されているともみなせます.
事実は論理式という形でHilbertでは抽象化を行ないます.
論理式とは
- Sを除く（積分記号として用いてしまっている）1文字からなる大文字アルファベットは命題変数を表す.
- 命題変数は論理式である.
- 論理式と論理演算子(~, |, &, ->)からなる式は論理式である.
- 論理式を丸括弧
()で括ったものは論理式である.
つまり、
A, Bは論理式である.
A, Bが論理式であるので、~A, A|B, A&B, A->B, (A), (A&B) も論理式である.
論理式の真偽値の宣言と確認
論理式と改行はその論理式が真である事の宣言となる.
論理式の後ろに?を付けるとその論理式の真偽値（またはUNDEFINED）を返す.
（実際は真である論理式の選言文と真偽値を調べる論理式の論理包含を取って、トートロジーならTRUEをパラドックスならFALSEをそれ以外ならUNDEFINEDを返す一種の糖衣構文です）
A # Aは真
A->B # AならばBも真
B? # Bも真
#=> true
A->B
B->C
(A->C)?
#=> true
論理演算子
一応確認しておきます.
~a
論理式aの否定.
a|b
論理式aとbの論理和.
a&b
論理式aとbの論理積.
a->b
~a|bの省略形.
a<->b
(a->b)&(b->a)の省略形.
パラドックスについて
2つの論理式の宣言が対立した場合でも特にエラーを吐く事はしません、
仮定が恒偽になるだけです. その場合、矛盾からは何でも導けてしまうので（不条理則）
意図せず仮定が恒偽になっていたときは少し不便です.
なので適宜仮定にパラドックスが起きていないか確認するのが
仮定と恒偽との包含論理が恒真になるのは仮定が恒偽のときのみなので、
(~P&P)?
を利用して確認します. まあでも面倒なので、
paradox?
という糖衣構文も用意しときましたよ.
A # Aは真である
~A # Aは偽でもある
paradox?
=> TRUE
実数に関わる公理系について
多くのプログラミング言語同様、実数に関わる公理の全てをプリインポートしているので、
現状ではHilbertでもそこはサポートしています.
若干ここが言語の一貫性を危うくさせるので廃止も考えています.
実数解析のための公理系インポート
postulate zfc_analysis
実解析
公理系zfc_analysisを仮定すれば、極限や微積分などの実解析を可能とします.
微分
d/dx(cos(x))
=> ( - sin( x ) )
d/dx(log(x))
=> ( 1 / x )
d/dy(y ** 2)
=> ( 2 * y )
d/dz(e ** z)
=> ( e ** z )
積分
S(log(x)dx)[0..1]
=> - oo
S( sin(x)dx )[0..pi]
=> 2.0
S( cos(x)dx )[0..pi]
=> 0.0
Matrix, Vector
(1 2 3; 4 5 6)
=> (1 2 3; 4 5 6)
(1 2 3; 4 5 6) + (1 2 3; 4 5 6)
=> (2 4 6; 8 10 12)
(1 2 3; 4 5 6) * (1 2 3)
=> (14 32)
関数
こんな感じ.
f(x, y) = x + y
f(2, 2)
=> 4
g(x) = x ** 2
g(2)
=> 4
ちなみに引数名は2文字以上を受け付けていません.
（；゜０゜）「２文字以上を受けつけてない！？」
また関数名はf, g, h のみしか受け付けておりません.
（；゜０゜）「！？」
（今後検討の余地あり）
この言語は別に大きなアプリケーションを複数人で作ることなどは全く想定していなくて、
可読性は自分のためのみで、その瞬間だけあればいい.
この貧しさこそ豊かさなんだという思想が根底にあります.
使い方
Rubyが使える環境であれば
$ gem install hilbert
や
$ echo "gem 'hilbert'" >> ~/.Gemfile; bundle install
などでhilbertgemをもってきてもらえらばhilbertコマンドが使えるようになるので
$ hilbert -i
Enjoy! ->
でインタプリタ（対話型）に入る事が出来ます.
また-zfcオプションを付ければ、実解析に関わる公理系を仮定した状態で対話型に入れます！
$ hilbert -i -zfc
Enjoy! ->
コンパイル先は３種類選べます.
（開発当初は全言語へのコンパイルを意気込んで実装していましたが、意味ないという事に気づきこの機能はほとんどメンテされていませんので極めて非推奨です）
Compile into R
$ hilbert -r foo.hr
Compile into Ruby
$ hilbert -rb foo.hr
Compile into Python
$ hilbert -py foo.hr
なぜRuby
-
コミュニティが大きく反応が得られやすいと思った
-
僕自身Rubyがいちばんいじれるのでアイディアをプロトタイプに落としやすかった. 処理速度に問題が出たらC言語拡張を使えばいいと思った.
-
Rubyが好きだった.
いい感じになってきたらHaskellで全部実装し直したいなと思ってます.