Edited at

Coqはチューリング完全 -- Ltacでbrainf*ckインタプリタを書いた

More than 1 year has passed since last update.

この記事は、Theorem Prover Advent Calender https://qiita.com/advent-calendar/2017/theorem-prover のために書かれました。

Coqをある程度知っている人向けの小ネタです。

しばしばCoqの紹介において、「Coqでは停止するプログラムしか書けない」「(そのため)Coqはチューリング完全ではない」と言われることがあります。実はこれ、正しいと言えば正しいのですが、間違いと言えば間違いです。

確かに、Coqで再帰関数を定義するためのFixpoint, Program Fixpoint, Functionといったコマンドはどれも停止性を要求します。そのため、Coqから抽出したプログラムは無限ループを起こすことはなく、その意味で安全性が保証されることになります。

では、何が間違いか? これは「Coqでは停止するプログラムしか書けない」という言葉にからくりがあります。まず、Coqは証明支援システムであって、その中に Vernacular, Gallina, Ltac という三つの言語を持ちます。他言語に抽出されるのはGallinaの項であり、停止性が保証されるのもGallinaのみなのです。

つまり、他言語に抽出したプログラムに停止性が保証されていても、Coqの対話環境でVernacularコマンドやtacticを実行したときに無限ループに陥って応答が来ないことはあり得るのです。

(実際、昔は停止しないtacticをうっかり実行するとそのままCoqIDEごと落ちてしまうことがよくありました……。)

ということで、今回は「Coqでは停止するプログラムしか書けない」「Coqはチューリング完全ではない」というのが嘘であることを言うために、Ltacでbrainf*ckインタプリタを書いてみました。


色んなやり方があると思いますが、まず扱いやすいように構文木とパーサーを書きました。ここはGallina項で定義しです。

Require Import List Arith Ascii String.

Import ListNotations.
Open Scope string_scope.

Inductive prim := PtrIncr | PtrDecr | Incr | Decr | Get.

Inductive stmt :=
| SNil : stmt
| Prim : prim -> stmt -> stmt
| Put : stmt -> stmt
| Loop : stmt -> stmt -> stmt.

Fixpoint parse' (str : string) :=
match str with
| "" => (SNil, nil)
| String x xs =>
let (body, rest) := parse' xs in
match x with
| ">"%char => (Prim PtrIncr body, rest)
| "<"%char => (Prim PtrDecr body, rest)
| "+"%char => (Prim Incr body, rest)
| "-"%char => (Prim Decr body, rest)
| ","%char => (Prim Get body, rest)
| "."%char => (Put body, rest)
| "["%char =>
match rest with
| nil => (Loop body SNil, nil)
| cons s rest' => (Loop body s, rest')
end
| "]"%char => (SNil, cons body rest)
| _ => (SNil, nil)
end
end.

Definition parse str := fst (parse' str).

brainf*ckを実行する上で、ここでは配列は自然数から自然数への関数で表し、入力を自然数のリストで表すことにします。配列、ポインタ、入力の組 (nat -> nat) * nat * list nat が環境になります。

ポインタのインクリメント/デクリメント(>/<)、ポインタが指す値のインクリメント/デクリメント(+/-)、入力からの読み込み(,)を処理して環境を更新する関数を以下で与えます。

Definition run_prim (env : (nat -> nat) * nat * list nat) p :=

let '(data, ptr, input) := env in
match p with
| PtrIncr => (data, S ptr, input)
| PtrDecr => (data, pred ptr, input)
| Incr => (fun i => if Nat.eq_dec i ptr then S (data ptr) else data i,
ptr, input)
| Decr => (fun i => if Nat.eq_dec i ptr then pred (data ptr) else data i,
ptr, input)
| Get =>
match input with
| [] => env
| x::rest => (fun i => if Nat.eq_dec i ptr then x else data i,
ptr, rest)
end
end.

出力 (.)やループ([/])の処理をLtacで行います。

Fixpoint append (s1 s2 : stmt) :=

match s1 with
| SNil => s2
| Prim p s => Prim p (append s s2)
| Put s => Put (append s s2)
| Loop b s => Loop b (append s s2)
end.

Ltac run env c' :=
let c := eval compute in c' in
match env with
| (?data, ?ptr, ?input) =>
match c with
| SNil => idtac
| Prim ?p ?c' =>
let env' := eval compute in (run_prim (data,ptr,input) p) in
run env' c'
| Put ?c' =>
let x := eval compute in (data ptr) in
idtac x;
run env c'
| Loop ?c1 ?c2 =>
let x := eval compute in (Nat.eq_dec (data ptr) 0) in
match x with
| left _ => run env c2
| right _ => run env (append c1 (Loop c1 c2))
end
end
end.

これで完成です。

気を付ける点としては、eval compute in x で項 x を評価しておかないと Ltac 内のパターンマッチに失敗する可能性があるところですね。

実際に書いたtacticを走らせてみましょう。

Goal True.

run ((fun _:nat=>0), 0, [4;3]) (parse ",>,<[-<+>]<."). (* 足し算 *)
run ((fun _:nat=>0), 0, [3;3]) (parse ",>,<[->[->>+<<]>>[-<+<+>>]<<<]>>."). (* 掛け算 *)
run ((fun _:nat=>0), 0, @nil nat) (parse "+[>.+<]"). (* 0,1,2... とすべての自然数を出力 *)

対話環境で上のtacticを読み込むと、上の二つはそれぞれ 7 (= 4 + 3), 9 (= 3 * 3) とメッセージ欄に表示され、最後のtacticは 0 1 2 ... 無限に自然数が出力されます。

ということで、めでたく(??)Coqがこの意味でチューリング完全であることが言えました。おしまい。

全体のコード:

https://gist.github.com/erutuf/6203173f602b524a908e422f4a7c480b