これまで
- D言語で作ってみる定理証明支援系(1) 型を作る
- D言語で作ってみる定理証明支援系(2) 関数を定義する (本記事)
- D言語で作ってみる定理証明支援系(3) 関数を定義する 実装編
リポジトリはこちら(随時開発中)
https://github.com/outlandkarasu/poet
はじめに
前回で、とりあえず型のインターフェイスTypeや関数型のクラスFunctionTypeができました。
今回は、その関数型を定義する手段を考えます。
関数の定義のしかたを考える
関数を定義するためには、関数の中身を考えなければなりません。
前回、関数は型と型を対応づけるということにしました。
# 型Aから型Rへ対応づける A -> R これの定義、つまり中身はどうなっているのでしょうか。
そして、具体的な関数がある場合、何が起きるのでしょうか？
妄想してみます。
# 型 A -> R の関数fがあるとする。 f: A -> R # 型Aの値aがある。 a: A # fに引数aを渡す。結果は型Rの値になる。 f(a) 上記のような妄想をしてみると、以下のようなことが言えそうです。
- 型には、それに属する値が存在する。
- 関数そのものも、関数型の値となる。
- そして、関数を使うと、ある型の値から別の型の値を作れる。
最後のことが重要になりそうです。
つまり、A -> Bがあるということは、Aの値があればBの値を作れる、ということになります。
A -> Bの関数とは、AからBを作れるという主張だとも言えます。
主張をするためには、証拠が必要になります。
Aの値があればBの値を作れる、という主張をするためには、Aがあったとして、そこからBを取り出す方法を示さなければなりません。
# A -> Bを定義する。 f: A -> B # Aがあったとして a: A # # なにか色々あって…… # # Bができた。 b: B # 以上で定義終了。 で、Aをどう色々やってBを作るのでしょうか……。
それをやるためには、まだ型に属する具体的な値についての考えが足りません……。
しかし、以下のようなものなら、ここまでの材料だけでも考えることができます。
# (A -> B) と (B -> C) があれば (A -> C) が作れる。 f: (A -> B) -> ((B -> C) -> (A -> C)) 具体的な値の中身に触れず、関数のみで済ませているのがポイントです。
関数はどれも、**ある値があれば……**という妄想の世界の住人なので、ある値がまだ無いうちは現実に突き当たりません。
そんなわけで、上記のfは**ある値があれば……**という妄想の世界の中だけで作ることができます。
とりあえず思いつきの擬似コードで書いてみます。
# (A -> B) と (B -> C) があれば (A -> C) が作れるはず。 # 「:=」という記号は、右辺の中身が左辺の定義になっているという意味のつもり。 # 「{}」で定義の入れ子を示す。 f: (A -> B) -> ((B -> C) -> (A -> C)) := { # A -> B があるとする。ここから、 (B -> C) -> (A -> C) が作れるはず。 ab: A -> B bcac: (B -> C) -> (A -> C) := { # B -> C があるとする。ここから A -> C が作れるはず。 bc: B -> C ac: A -> C := { # Aがあるとする。ここから C が作れるはず。 a: A c: C := { # abを使ってbが作れる。 b: B := ab(a) # bcを使ってCが作れる。 bc(b) } # Cが作れた。 # これで、AがあればCが作れることがわかった。 c } # A -> C が作れた。 # これで、B -> CがあればA -> Cが作れることがわかった。 ac } # (B -> C) -> (A -> C)が作れた。 # これで A -> B があれば (B -> C) -> (A -> C) が作れることがわかった。 bcac } # 以上で (A -> B) -> ((B -> C) -> (A -> C)) が作れた。 長くなってしまいましたが、確かに(A -> B) -> ((B -> C) -> (A -> C))が作れた気がします。
コードで表現する
上記の関数定義のしかたを、D言語のコードで表現してみます。
// 型を用意する。 immutable A = example(); immutable B = example(); immutable C = example(); immutable F = funType(funType(A, B), funType(B, C), funType(A, C)); // 型Fの関数fを定義する。 // dは、定義を進めるための情報の置き場となるオブジェクト(詳細はあとで考える) // abはFの第1引数のA -> B。この中ではA -> Bがあるとする。 auto f = define(F, (d, ab) { // 次に(B -> C) -> (A -> C)を作る必要がある。 // B -> Cがあるとする。 auto bc = d.begin(); // 次にA -> Cを作る必要がある。 // A があるとする。 auto a = d.begin(); // abを使ってbが作れる。 auto b = d.apply(ab, a); // bcを使ってcが作れる。 auto c = d.apply(bc, b); // Cが作れたので A -> C ができる。 auto ac = d.end(c); // A -> Cができたので(B -> C) -> (A -> C)ができる。 auto bcac = d.end(ac); // (B -> C) -> (A -> C)ができたので // (A -> C) -> ((B -> C) -> (A -> C))ができる。 return bcac; }); こんな感じにできそうです。(なんだかD言語で書いた方がすっきりしてますね)
（もっとdelegateなどを使って入れ子のスコープをちゃんと分けた方が良さそうに思えますが、今後対話型のユーザーインターフェイスなどを用意することを考えて、あえてフラットな関数呼び出しの連続の形にしています）
上記から、とりあえず関数を定義するのに必要な操作がわかりそうです。
一覧にすると次の通りです。
-
define(t, def)- 関数定義を開始する。
- 定義中の情報を貯めるオブジェクトの確保と、最初の引数の抽出を行い、定義を開始・終了する。
-
d.begin()- 関数定義の中で入れ子の関数定義を始める
-
defineのように、最初の引数を抽出する。 -
defineと違うのは、次に必要になる戻り値の型を引数取り出しの対象とする。
-
d.end(r)- 関数定義の中で入れ子の関数定義を終える。
- 戻り値となる
rを受け取って入れ子の定義を終了させ、目的の関数型の値を作る。
-
d.apply(f, a)- 関数定義の中で関数を呼び出す。
- 妄想の中で存在する関数
fを引数aで呼び出し、結果の値を返す。
実装を考える
上記の構想をとりあえずコードにしてみます。
@safe: /** 引数・関数適用の結果などを格納する変数。 とりあえず今は名前だけの構造体にしておく。 */ struct Variable {} /** 関数定義のためのクラス。 */ class Definition { /** 入れ子の関数定義の開始。 Returns: 引数を格納した変数 */ Variable begin(); /** 入れ子の関数定義の終了。 Params: result = 戻り値を格納している変数 Returns: 定義された関数を格納した変数 */ Variable end(Variable result); /** 関数を適用する。 Params: f = 適用する関数 a = 関数の引数 Returns: 関数を適用した結果を格納した変数 */ Variable apply(Variable f, Variable a); } だいたいこんな感じになると思います。
このDefinitionを操作していくことで定義が作られていくことになります。
さて、Definitionは、操作を通して明らかに状態が変わるので、中身が変化します。
その変化する中身には、どのようなデータ構造があるでしょうか？
前に書いてみたコードを見直します。
auto f = define(F, (d, ab) { auto bc = d.begin(); auto a = d.begin(); auto b = d.apply(ab, a); auto c = d.apply(bc, b); auto ac = d.end(c); auto bcac = d.end(ac); return bcac; }); beginとendの間でapplyが呼び出されています。
beginやapplyで変数(Variable)が出て来て、それがapplyやendで使われています。
begin・endの間に出て来た変数は、end後には使用できないことになりそうです。
そして、begin・endは何回でも入れ子になりそうです。
この手の入れ子構造は、スタックを使うと表現できそうです。
また、スタックの中で作られた変数は、そのスタックの中……つまりスコープの中でしか使えません。
まとめると、入れ子になったスコープのそれぞれに変数(引数も含む)が存在するという構造になりそうです。
beginにより新たにスコープが開始され、変数に引数が設定される。
endによりスコープが閉じられ、そして、前のスコープの変数に戻り値が設定される。
applyでは、そのスコープで見えている変数を使って関数適用が行われ、戻り値が新しい変数に格納される。
そういった動きが、色々考えた末に見えて来ました。
次回予告
だいたいここまでで力尽きたので、続きは次回にしようと思います。
次回は関数定義の実装に入ります。