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

この記事は、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項で定義しです。

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

```coq
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で行います。

```coq
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を走らせてみましょう。

```coq
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