D言語で作ってみる定理証明支援系(2) 関数を定義する

これまで

• 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では、そのスコープで見えている変数を使って関数適用が行われ、戻り値が新しい変数に格納される。
そういった動きが、色々考えた末に見えて来ました。

次回予告

だいたいここまでで力尽きたので、続きは次回にしようと思います。
次回は関数定義の実装に入ります。