はじめに

ここ最近、カリー＝ハワード同型対応という概念に興味があって、色々文献を漁ったりセミナーを受講してみたりしました。しかし、私が無学なため、まだまだ具体的な理解が及んでいません。

そこで、自分でカリー＝ハワード同型対応がはっきり目の前に現れるもの……すなわち定理証明支援系を自作してみて、具体的なところや、まだ自分がわかっていないところを明らかにしようと思います。

なお、実装中の定理証明支援系のリポジトリはこちらです。記事の進捗に従ってコードが増えます。

カリー＝ハワード同型対応とは

まだ全然理解が及んでいないところなので詳しい説明はできないのですが、噂に聞いたところ、下記のような感じらしいです。

数理論理学の命題論理や述語論理と、プログラムの型付け規則や計算規則がきれいに対応する。
つまり、数学の論理とプログラムが対応し、証明とプログラムは同一のものとみなせる。
うまくやると、証明から具体的なプログラムを生成して、計算を行うことができる。
逆に、プログラムの持つ性質(かならず終了したり、かならずある範囲の値が出力される、など)も証明できる。

詳しいところは、下記のページの講義資料や、

以下のような参考文献に書いてあったりします。

しかし、なかなか本格的な説明は見つからず……。
（英語なら何かあるかも。情報募集中です！）

定理証明支援系とは

定理証明支援系は、読んで字のごとく定理の証明を支援するソフトウェアのことです。

数学の定理は、もっとも基礎となる公理(前提)から出発し、決められた推論規則を適用していき、目的の命題にたどり着くことによって証明されます。

証明の1つ1つのステップはごく簡単なものです。しかし、定理がすごいものになると当然ステップ数もものすごいものになり、人間には正しく書くのもチェックするのも難しいものになってしまいます。

そこで、コンピューターを使って、間違った証明をしないようにしたり、簡単な定理を自動証明したりするわけです。

コンセプト

というわけで、上記のような定理証明支援系を自分で作って、カリー＝ハワード同型対応を肌で感じてみようと思います。

コンセプトは以下のような感じでやってみようと思います。

実装言語はD言語
- 他になにも考えられないので。
とはいえ、D言語の型システムは使わない。型システムを自作する。
数学の基礎になる定理証明をやるソフトなので、D言語の安全性に関する機能を最大限使ってバグを防ぐ。
- その代わり、GCありを前提にし、パフォーマンスよりも安全なコードであることを優先する。
なるべく対話的に使えるものになるよう頑張る。
- ユーザーによるミスや予期しない入力についてチェックを行い、実行時エラーを出す。
なるべく弱いシステムにする
- 強いシステムは実装が大変です。
- 弱い論理体系(直観主義論理)でやった証明の方が、プログラミングや計算と相性が良いようです。
- 弱いシステムでどこまでできるのかも試してみたいです。

正直ただの素人の自分がカリー＝ハワード同型対応にどこまで近づけるか、乞うご期待です！

想定読者

一応、こんな人に向けて書いているつもり、というようなことを記載しておきます。

Java・C#・C++といったC系のオブジェクト指向言語を使ったことがある。
インターフェイスやクラスといった基本的なオブジェクト指向の概念や、配列やリストといったごく基本的なデータ構造を使ったことがある。
D言語の知識についてはなんとなくD言語ツアー(神コンテンツ)などを流し見れば大丈夫な感じになると思います。

つまり普通になんとなくプログラミングできる自分のような人が読めるような感じにしようと思います。

型を作る

さて、まず何はともあれ、論理および計算の基礎になる型の概念を作らねばなりません。
なんか型をいろいろやることでそれが論理になり、計算になる、というのが、今のところ私が手にしているカリー＝ハワード同型対応の理解の全てです。

それも、今回はプログラミング言語に組み込まれている型ではなく、プログラミングで型そのものを作るということをやる必要があります。

(型そのものを実行時に定義したり操作する必要があるため。Rubyとかなら組み込みの型を動的に使えたりするかもしれませんが、D言語は静的型付き言語なので……)

それに、プログラミング言語組み込みの型を使わずに、ちゃんと自分で定義していく方が、より型の難しさを肌に感じられるようにも思います。
そんなわけで、ぼくの考えたさいきょうの型を、これから作ってみます。

型とは何か……。それはあまりに深遠な問いで、つかみどころがありません。
とはいえ、プログラミングでは書きながら考えるということができます。
とにかくまずは型をこの世界にあらしめてみます。

source/poet/type.d

/**
型のインターフェイス
*/
interface IType { }

はい、型ができました。

次に考えるのは、このinterfaceはどんな性質を持つべきか、そして、どんな操作が行えるべきかです。

D言語でクラスやインターフェイス・構造体といったものの性質を考えるとき、まず最初に検討するのは、それは変化するものか、変わらないものかということです。

型はおそらく変化しません。
型は何かしら定義されて生まれると思われますが、その後で、定義の内容が書き変わったりすることは無いと思います。

そこで、D言語の機能を使って以下のようにします。

source/poet/type.d

immutable interface IType {}

// immutable(IType)と毎回書くのが面倒なので別名定義。
alias Type = immutable(IType);

こうすると、このinterfaceを実装するclassはすべて不変(immutable)であることが要請されます。

D言語のimmutableはほんとうにimmutableです。メンバー関数などを使用して値を変えられないのはもちろん、別スレッドからの操作で知らないうちに値が変わったりすることもありません。安心して不変性を享受できます。

ただし、危険な操作がプログラマーによって意図的に行われない、@safeである、という前提条件があります……。そこで、以下のようにします。

source/poet/type.d

// @safe属性から下は、危険な操作を行えなくなる。
// 危険な操作の例: 強制的なポインタの型変換・D言語の外側のシステム関数の使用などなど
@safe:

immutable interface IType {}

alias Type = immutable(IType);

これで、安全な世界で不変なTypeを使う準備が整いました。

次に、これが持つべき操作、つまりメンバー関数を考えます。
型は何をできるべきか……。
型システムの実装のことを考えると、まず型同士を比較して、同じ型かどうか確かめられる必要があります。

比較のためのメンバー関数equalsを、なるべく厳密な方法で宣言してみます。

source/poet/type.d

immutable interface IType
{
    /**
    型同士を比較し、一致する場合はtrueを返す.
    Params:
        other = 比較対象の型
    Returns:
        型が一致する場合はtrue
    */
    bool equals(scope Type other) @nogc nothrow pure scope;
}

いきなりいろいろ属性が出てきてしまいました。ちょっと解説します。

まず、interfaceの先頭にあるものやaliasとして定義している属性も含めてequalsメソッドを展開すると、以下のようになります。

@safe
bool equals(
    scope immutable(IType) other
) immutable @nogc nothrow pure scope;

@safe
- 先述の通り安全な関数であることを要請します。
引数のscope
- 引数の使用がローカルスコープに限定され、たとえばグローバル変数へ参照がコピーされないことを強制します。
引数のimmutable()
- 引数がimmutableであることを要請します。
引数リストの後のimmutable
- immutableであるオブジェクトに対してのみ、このメンバー関数を呼び出せるようにします。
@nogc
- このメンバー関数がGCを必要とする操作(動的配列の確保など)を行わないことを強制します。
nothrow
- このメンバー関数がException(とその派生クラスの例外)をthrowしないことを強制します。
- でも実は、Errorの派生クラス(OutOfMemoryErrorなど)はthrowできます……。
pure
- グローバル変数などの状態の変更を伴わない"ピュア"な関数であることを強制します。
- でも実は、引数を通した状態変更は可能です……。
引数リストの後のscope
- メンバー関数のthisがscopeであること……つまり外部にthisが持ち出されないことを強制します。

えらい盛り盛りですね。D言語を使う場合、毎回これを全部付けないといけないのでしょうか……。
それは、プログラマーの自由に任されています。

厳密に属性を付けた方が呼び出せる場面が増えるため、ライブラリーを書くような場合はなるべく書いた方が良いです。
ただ、使われる場面が限られているアプリケーションのコードや、書き捨てのコードについては、せいぜいconst(C/C++のconstとだいたい同じ)や@safeを付ける程度で良い気がします。
また、テンプレート関数では一部属性を勝手に推論してくれたりもします。

D言語は、やはりC/C++の思想を受け継いでいて、プログラマーに最大の自由を与えるのでした。ただし、自由を与えつつ、身を守るための装備もまた豊富に揃えています。

今回は、なるべく安全・厳密に書くというコンセプトなので、積極的に盛り盛りにします。

試しに型を実装してみる

interfaceだけではやはりぼんやりしているので、とにかく型を実装してみます。

例として使えるようなサンプルの型にするので、名前はexampleとします。

source/poet/example.d

/**
モジュール宣言。しょせんこれはD言語ポエムなので、プロジェクト名はpoetとしました。
*/
module poet.example;

// 先ほどのTypeを使う。
import poet.type : IType, Type;

// とりあえずこれは必ず書く。
@safe:

/**
型のサンプル実装。
派生クラスは作れない。
すべてのメンバーがimmutable。
*/
final immutable class CExample : IType
{
    // overrideでインターフェイスの実装や基本クラスのオーバーライドであることを示せます。
    override bool equals(scope Type other) @nogc nothrow pure scope
    {
        // 仮実装
        return false;
    }

private:

    /**
    デフォルトコンストラクタ。
    関数の中身としてはGCを使っていないので、@nogcが付けられる。
    外部から直接呼び出せないよう、privateにしておく。
    */
    this() @nogc nothrow pure scope
    {
    }
}

// 面倒なのでやはりalias。
alias Example = immutable(CExample);

/**
Returns:
    例として使うための新しい型。
*/
Example example() pure nothrow // GCを使ってもpure。OutOfMemoryErrorの可能性はあるけどnothrow。
out (r; r !is null) // 必ず何かインスタンスが返る。
{
    return new Example();
}

とりあえずクラスを定義し、インスタンスが作れるようになりました。
次に、unittestを書きながらExampleのequalsの動きを考えてみます。

///
pure nothrow unittest // unittestも関数の一種で、属性が付けられる。
{
    // 「型が等しい」ということについて考える。
    auto t = example();

    // 自分自身とは等しい。
    assert(t.equals(t));

    // nullとは等しく無い。
    assert(!t.equals(null));

    // 別の型を作ってみる。
    auto u = example();

    // uとtは異なるインスタンスで、等しく無い。
    assert(!t.equals(u));
    assert(!u.equals(t));

    // uもまた自分自身と等しい。
    assert(u.equals(u));
}

example()関数は、新しい型を生成するという動作をするため、そこから生成されたインスタンスのequalsは上記のような動作が妥当だと考えました。

そんなわけで、テストの内容を実現するequalsの実装を考えます。瞬殺ですが……。

    override bool equals(scope Type other) @nogc nothrow pure scope
    {
        return this is other;
    }

これで、まだ例として使えるだけですが、型を作る手段がひとつ手に入りました。

関数の型を作る

型については、値の分類だったり集合だったりするんだろうな、というぼんやりとしたイメージがあります。そういった単純な箱のようなものだけで、何か動きのあるものを作るのは難しそうです。
いま手元にあるTypeだけでは明らかに何もできません。
(まだequalsしかできませんし)

そこで、次は、関数を作ってみます。
関数とは何か……これも深遠な問いですが、とりあえずいま手元にある型をもとに考えてみます。

関数は型である。
関数は、ある型から、ある型へ、型同士を対応づける。
- (それぞれ同じ型同士の場合もある)

この2つの性質を備えれば、ふだんプログラミングなどで使っている関数の最低限の条件は満たせそうです。

なお、これから、関数を書き表す記号として->を使おうと思います。たとえば、Aを引数に取ってRを返す関数はA -> Rと書きます。

さて、関数の概念をさっそくコードにして考えてみます。

source/poet/fun.d

/**
function は実はD言語の予約語なので、funという略記を使います。
*/
module poet.fun;

import poet.type : IType, Type;

@safe:

/**
関数の型。
引数・戻り値の型を持つ。
*/
final immutable class CFunctionType : IType
{
    // プロパティの定義
    @property @nogc nothrow pure scope // 属性はこういう風にまとめ書きもできます。
    {
        /// 引数の型
        Type argument()
        out (r; r !is null)
        {
            return argument_;
        }

        /// 戻り値の型
        Type result()
        out (r; r !is null)
        {
            return result_;
        }
    }

    override bool equals(scope Type other) @nogc nothrow pure scope
    {
        auto otherFunction = cast(FunctionType) other;
        if (otherFunction) // Functionであればnullでないのでtrue
        {
            // 引数・戻り値それぞれの型が等しければ等しい。
            return argument_.equals(otherFunction.argument_)
                && result_.equals(otherFunction.result_);
        }
        return false;
    }

private:

    this(Type argument, Type result) @nogc nothrow pure scope
    in (argument !is null) // nullはやめてね
    in (result !is null)
    {
        this.argument_ = argument;
        this.result_ = result;
    }

    Type argument_;
    Type result_;
}

alias FunctionType = immutable(CFunctionType);

/**
関数の型を作る。

Params:
    argument = 引数の型
    result = 戻り値の型
Returns:
    指定された型の引数・戻り値の関数。
*/
FunctionType funType(Type argument, Type result) nothrow pure
in (argument !is null)
in (result !is null)
out (r; r !is null)
{
    return new FunctionType(argument, result);
}

///
pure nothrow unittest
{
    import poet.example : example;
    auto t = example();
    auto u = example();

    // 型tを引数に取り、uを返す関数。つまり t -> u
    auto f = funType(t, u);
    assert(f.argument.equals(t));
    assert(f.result.equals(u));
}

/// equalsのテスト
pure nothrow unittest
{
    import poet.example : example;
    auto t = example();
    auto u = example();
    auto f = funType(t, u);

    // 関数も自分自身とは等しい。
    assert(f.equals(f));

    // nullとは等しく無い。
    assert(!f.equals(null));

    // 同じ型の別の関数
    auto g = funType(t, u);
    assert(f.equals(g));
    assert(g.equals(f));

    // 異なる型の関数
    auto h = funType(u, t);
    assert(!f.equals(h));
    assert(!h.equals(f));

    // 引数・戻り値どちらか一方が違えば違う。
    assert(!f.equals(funType(t, t)));
    assert(!f.equals(funType(u, u)));
}

とりあえず一気に関数を書き下してみました。
これはまだ引数・戻り値の型の情報しか持っていません。でも、結構これでいける気もします。

複数の引数を取る関数の型を考える

なるべく弱いシステムを作るという今回のコンセプトに沿って、このシステムで扱う関数も引数を1個だけに限定します。
プログラミングや数学などで日常的に使う関数の場合、引数が2個以上あるのは普通です。でも、今回のシステムで作れる関数は常に引数が1個です。

実は、関数の引数を1個に限定しても、本当の意味で弱くなるわけではありません。
カリー化という方法で、1引数関数だけを使ってあたかも複数の引数を取れるような関数を作ることができます。

たとえば、A・B・Cを引数に取ってRを返すような関数A -> B -> C -> Rを作りたいとします。
このシステムでは1引数関数しかないので、直接はこの関数を作ることはできません。
そこで、1つ引数を受け取ったら、「次の引数を取る関数」を返すようにします。
関数を1つずつカッコで括って書くと、以下のような感じです。

A -> (B -> (C -> R))

この関数に対して、まずAを渡すとB -> (C -> R)が返ります。続いてBを渡すとC -> Rが返ります。そして最後にCを渡すと、最終ゴールのRが手に入ることになります。

（この仕組みの実装を考えると、えっ、最初の方で受け取った引数とかどこに保存しておけばいいの？とか気になりますが、とりあえず今は考えないことにします）

とういわけで、複数引数の関数は次のように書けます。

auto a = example();
auto b = example();
auto c = example();
auto r = example();
funType(a, funType(b, funType(c, r)));

かったるいのでユーティリティ関数を作ります。

source/poet/fun.d

FunctionType funType(Type a, Type b, scope Type[] types ...) pure nothrow
in (a !is null)
in (b !is null)
out (r; r !is null)
{
    auto r = (types.length == 0) ? b : funType(b, types[0], types[1 .. $]);
    return new Function(a, r);
}

///
pure nothrow unittest
{
    import poet.example : example;

    auto a = example();
    auto b = example();
    auto c = example();
    auto r = example();

    // 1引数関数の型の生成
    auto f1 = funType(a, b);
    assert(f1.argument.equals(a));
    assert(f1.result.equals(a));

    // 2引数関数の型の生成
    auto f2 = funType(a, b, c);
    assert(f2.argument.equals(a));
    assert(f2.result.equals(funType(b, c)));

    // 3引数関数の型の生成
    auto f3 = funType(a, b, c, r);
    assert(f3.argument.equals(a));
    assert(f3.result.equals(funType(b, c, r)));
}

これで複数引数の関数の型も定義できるようになりました！

次回予告

次回は、関数を定義する、そしてつまり証明するということができるようになるまで進めてみようと思います。

D言語で作ってみる定理証明支援系(1) 型を作る

目次

はじめに

カリー＝ハワード同型対応とは

定理証明支援系とは

コンセプト

想定読者

型を作る

試しに型を実装してみる

関数の型を作る

複数の引数を取る関数の型を考える

次回予告