宣言型計算モデル

宣言型計算モデル Declarative Computation Model

日曜の ET セミナーに参加していただいた，日本 Ruby の会会長の @takahashim さん (北大での指導教官が同じ)に教えていただきました．

これだけだと単に abstract nonsense っぽいけど、これを土台にしていけば面白いことができそう、と思った記憶が。好きな論文。 http://twitter.com/takahashim/statuses/906523913

あのころからどれくらい変わったかは知りたいですねえ。日曜の話ではよくわからなかったので。http://twitter.com/takahashim/statuses/906527385

せっかく御足労いただいたのに，勉強不足ですいませんでした…

そもそも，何気なく 「宣言型パラダイム」という言葉を使ってきたのだけど，ちゃんと定義のある言葉だったのだと，ご指摘でいまさら気づいたという話．

もう 15 年前 (1993) の論文で，内容も古いし，特に内容も無いのですが，ざっと 10 分で ET の理論が目指すところを把握するには便利な日本語の論文だと思ったので紹介しておきます．

まぁ，CiNii でも，閲覧できる人は限られてしまうと思いますが… (とりあえず，北大ドメインの中からは，普通に PDF 取れます)

ざっと要点だけを挙げておくと．

・計算の概念の広がり

- ground な計算
-- 具体的な入力から具体的な出力を得るという計算
-- 最もベーシック，計算可能性の理論 （チューリング機械，ラムダ計算，．．．）

- non ground な計算
-- 変数を含むデータ構造の計算
-- Prolog の差分リストなど

- 抽象解釈
-- 元プログラムの抽象化 → 抽象実行 → 抽象情報の収集
-- プログラム自体が計算の対象となる

- タイプ推論

これらのような 「新しい種類の計算」 の重要性が増してきた．
しかし，今のところ，さまざまな計算モデルの共通の基盤と言えるものは計算可能性を論じる Turing の枠組み （と同等のレベルのもの）しかない．
このような高次の計算を有効に議論できるための構造を備えた理論的な枠組みが必要である．
それは各計算モデルの共通性と差異を数学的にはっきり示せる枠組みである．

・ 宣言型計算モデル
「計算 = 宣言的プログラムの等価変換」

計算をプログラム変換と見なしており，プログラム変換の議論が中心の理論構成となっている．
宣言型計算モデルは高次の計算を議論するためにとくに有効と考えられる．

Specialization Structure (現在の特殊化システムか ?) のオブジェクト空間により，関数型・論理型・項書き換えシステム・制約論理プログラミングなどを特徴付けることができる （実例付き）

・ （Specialization Structure 上の）宣言的プログラム

『プログラムというのは，普通は，「実際に動く」ことを前提とする．しかし宣言的プログラムは，純粋に数学的な概念であり，「実際に動く」 必要はない．プログラム変換によって数学的な意味での変化が議論できればよい．宣言的プログラムは，完全に宣言的な記述であり，無限の節からなるものも許され，計算可能性にはこだわらない．これに対して，論理プログラムは制御 (cut など) を含み，実際に動作することを前提としており，宣言的プログラムの位置付けとは異なることに注意する必要がある．』

・スキーマ理論

『いろいろなプログラミング言語に宣言的プログラムの理論を適用するためには，適切なオブジェクト空間を構成し，各プログラムの動作が対応する宣言的プログラムの等価変換と一致することをいえばよい．こうして宣言的プログラムとして認定できれば，宣言的プログラムの理論が提供する意味論や unfold 変換の理論などを使って明快に議論することができる．これは新しい知識表現などを構想し，その理論や処理系を作る時にとくに有用である．』

・ むすび

『宣言型計算モデルは，今後なすべきことはあまりにも多いが，これまでの計算モデルが生み出した多くの研究成果を自然に継承し，さらに発展させるために有効であると考えられる．』

---

ざっくりと言うと，CHR などとの比較の研究が一区切り付いて，UL/α 言語から ET 言語になって，仕様から N ルールを作るための理論が整備されてきた感じですね．

現在は，仕様の書き方の研究 （ウェブアプリケーションや GUI など，ダイナミックインタラクティブシステムへの応用），N ルール生成の研究，並列プログラムの生成と正当性の証明，N プログラムから D プログラムを生成する研究，N プログラムからハードウェアを生成する研究，D プログラムから命令型プログラムを生成する研究 （私） などなどを，いろんな人が研究している感じですね．

私も自分が関わっていないところの研究はさっぱりなので，詳しくは知らないのですが…