Coq で Quine

Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごとく Gist 上 https://gist.github.com/4700318 にも同じものを置いておきました。

Coq の特性あれこれ

Quine なるものを初めて聞いた人は wikipedia:クワイン_(プログラミング) あたりを見てみましょう。「自分自身のソースコードを標準出力する。ただし空ファイルでなく、入力は受け付けない」というのが一般的な Quine のお作法ですが、Coq で書くにはいくつか考えねばならない点があります。

標準出力……。

最大の問題として、Coq 単体では出力ができません。純粋すぎる相手というのは得てして扱いにくいものです。悩んでどうにかなる問題でもないので、コードの最後を Eval compute in として、ここが評価されたときにコード全体と同じ文字列になることを目指しました。

文字列の扱い

大部分の言語と違い、Coq は文字列を扱うのにいちいちライブラリを読み込む必要があります。使うライブラリは Ascii と String。

ascii 型の方はコンストラクタの引数に bool を 8 個取って、8 ビット ASCII コードとして読むものです。

Inductive ascii : Set :=
    Ascii : bool ->
            bool -> bool -> bool -> bool -> bool -> bool -> bool -> ascii

ちなみに実験してみるとわかりますが、引数の順番は下位ビットが先です。

Eval compute in Ascii true  false false false
                      false false true  false.

    = "A"%char
    : ascii

また、string 型の方はリストと同じ構造を持っています。

Inductive string : Set :=
    EmptyString : string | String : ascii -> string -> string

EmptyString が nil、String が cons 相当のコンストラクタですね。string_scope を開いておくと文字列の結合 append が + でシュガーされるので、見やすくするためにこれを使いました。

クォーテーションの扱い

文字列のデリミタは " です。Quine を書く上で、文字列の中に " が出現するためエスケープを考える訳ですが、ここで若干問題が。どうも Coq では (少なくとも CoqIDE の表示上は) 記号 " を単体で表示させることができないようです。実際、ASCII コード 34 を評価すると

Eval compute in ascii_of_nat 34.

     = """"%char
     : ascii

となり、"" で一文字分 (つまり "" が " のエスケープ表現) となっていることがわかります。ここは若干不本意ですが、「表示文字列中の " と "" との差には目をつぶる」として逃げることにしましょう。

Quine の実装

以上のことを踏まえて具体的なコードを作っていきましょうか。

まず大まかな構造として、次のような形を考えます。

Definition Q : string := [空欄 A].
Eval compute in [空欄 A'].

この Eval compute in [空欄 A']. でコード自身が表示されればよいわけです。

ステップその 1

Definition と Eval の二つの文がある以上、[空欄 A'] はこの二つの文をつなげた文字列が入るはずです。そこで、次のような形になることがわかります。

Definition Q : string := [空欄 A].
Eval compute in [空欄 B] ++ "." ++ [空欄 C].

非形式的な言い方をすれば、[空欄 B] が「Q にしかるべき文字列を代入せよ」、[空欄 C] が「「このコードを表示せよ」を表示せよ」を表す部分です。

ステップその 2

次に、[空欄 C] について考えます。意味するところが「〜を表示せよ」なので Eval compute in を入れたいところですが、そうすると堂々巡りになってしまいそうですね。回避策として、前半で定義している Q を参照します。

Definition Q : string := [空欄 A].
Eval compute in [空欄 B] ++ "." ++ Q.

そうすると、Q は「〜を表示せよ」でなくてはならないため、Eval compute in で始まることがわかりました。

Definition Q : string := "Eval compute in [空欄 D]".
Eval compute in [空欄 B] ++ "." ++ Q.

ステップその 3

次に埋めるべきは [空欄 B] です。ここには前半部に対応する「Q に 「Q の中身」を定義せよ」を意味するコード文字列が入るはずですね。「Q の中身」を文字列として表すのに、冒頭に挙げた参照文献では Q に対して Haskell の show を使っています。Coq に show はないので、手動でデリミタ " を付けましょう。文字列「Q の中身」は """" ++ Q ++ """" です。

Definition Q : string := "Eval compute in [空欄 D]".
Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.

ステップその 4

これでほとんど完成しました。後は [空欄 D] として、実際に Eval compute in の引数になっている「"Definition Q : string := " ++ """" ++ Q + """" ++ "." ++ Q.」をそのまま持ってきてエスケープすればオッケー。

Definition Q : string := "Eval compute in ""Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.

完成！

ライブラリの読み込みなどを追加し、また見やすくなるように適宜改行を入れたりした完成品が以下になります。はてなブログのベタ打ちだと若干見づらいですが、Gist の方を見てもらうと地の文と文字列との境目が分かりやすいかと。

Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "
Eval compute in ""
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.

その他補足

ここで書いた Quine は当然ですが最短ではありません。改行が無駄ですし、型宣言も省略できます。あるいは、今回は構成手順に重きを置いたためこの形になりましたが、もしかしたらもっと本質的にいい書き方があるかもしれません。しかしまあ、そもそも Coq は短く書くことに向いた言語ではありませんし、無理に追求はしないことにしましょう。なお、どうしても短い Quine が書きたい人は wikipedia:HQ9+ あるいは PHP の利用をおすすめします。

ちなみに今回は深入りはしませんが、「自分自身のコード」に言及する上でキモになっているのが [空欄 C] の中身「「このコードを表示せよ」を表示せよ」という部分です。こういう表現の背後には Kleene の再帰定理があり、またかの有名な不完全性定理の証明と関係があったりして面白い部分ではあるのですが、それはまた別の話。