等価変換型プログラムをかじる

議論の枠組みとしてのETパラダイム

　ETパラダイムには、さまざまなプログラミングモデルを統一的に議論したいというモチベーションもあります。そのためETの理論体系は、まずはETのプログラミングモデルに限定されない、より汎用的な仕様とプログラムの枠組みを定め、その上で確定節によるET仕様記述と、ETルールという書き換え規則によって定義されるETプログラムの枠組みを構築しています（図2）。

　これにより、同じ枠組みの上で、関数プログラミングや論理プログラミングなどの、ほかのプログラミングモデルを議論することが可能となります。当然、プログラミングモデルが異なれば、扱うデータ構造や手続きも異なってきます。そこでETの理論は、特殊化システム（Specialization System）という枠組みを定め、それらの違いを統一的に議論できる理論を構築しました。

　少し専門的になってしまいますが、特殊化システムによって、例えば関数プログラミングにおける遅延評価や論理プログラミングの単一化、それらの複合パラダイムである関数論理プログラミングのナローイングなど、さまざまな概念を統一的に議論できることがわかっています。

　ETパラダイムは、等価変換という一般的な原理に基づいて、形式的仕様記述から具体プログラム生成までの一貫した理論化を進めているので、その名が付いています。理論の肝となる「等価変換」とは、宣言的記述（確定節の集合）の意味を保存する変換という意味です。意味と言うと、何やら哲学的で難しい感じがしますが、要するに仕様（宣言的記述）よって定義される集合のことです。

　例えば、Prologの説明の際に出てきたappendという述語は、1番目のリストと2番目のリストを連結したリストが3番目の引数である、という関係を満たす集合の定義と考えることができます。この集合は無限集合で、例えばappend([], [], []),append([1], [], [1]), append([1], [2], [1, 2])のような形をしたアトムの具体例がその要素となります。

　そしてその集合において、どのようなデータ構造がアトムの引数に許されるのかということ、つまりプログラムが扱うデータ構造の種類は、特殊化システムの定義によって決まります。

仕様とプログラム、正当性関係

　ETの枠組みにおける仕様は、問題ドメインとそのドメインに含まれる具体的な問題の解（問題ドメインの背景知識）を確定節の集合で定義します。そしてETの枠組みにおけるプログラムは、解を得るための手続きをETルールの集合によって定義します。ETの計算の枠組みでは、状態を確定節の集合で表現します。そしてETルールは、確定節の集合を書き換えます。その際、変換前後での確定節集合の意味が等しいという、正当性関係を満たさなければなりません。

　プログラム合成のための枠組みを考えたとき、仕様に対する正当性という概念が厳密に定義されていることと、プログラムがルールによって記述されることが本質的に重要なのだと考えられています。ETルールは、単体で仕様に対する正当性を議論できるので、仕様からのプログラム生成を考えたとき、とても扱いやすい部品となるのです。

　ETの枠組みは、ETルールを仕様から自動生成するための理論的な枠組みを持っていますし、人間のひらめきによって記述したルールがETルールであることを証明する枠組みも持っています。これにより、機械による推論と、人間のひらめきを総動員し、効率的なプログラムを体系的に得るための理論が構築されています。