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

# これまで

* [D言語で作ってみる定理証明支援系(1) 型を作る](https://qiita.com/outlandkarasu@github/items/dc8c022cf226a4686a06)
* D言語で作ってみる定理証明支援系(2) 関数を定義する (本記事)
* [D言語で作ってみる定理証明支援系(3) 関数を定義する 実装編](https://qiita.com/outlandkarasu@github/items/02dc8fb9e7ae84e01a4a)

リポジトリはこちら(随時開発中)
https://github.com/outlandkarasu/poet

# はじめに

[前回](https://qiita.com/outlandkarasu@github/items/dc8c022cf226a4686a06)で、とりあえず型のインターフェイス`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言語のコードで表現してみます。

```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`で呼び出し、結果の値を返す。

# 実装を考える

上記の構想をとりあえずコードにしてみます。

```d

@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`は、操作を通して明らかに状態が変わるので、**中身が変化します。**
その変化する中身には、どのようなデータ構造があるでしょうか？
前に書いてみたコードを見直します。

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

## 次回予告

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