この記事は、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