Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
Help us understand the problem. What is going on with this article?

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

More than 3 years have 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

erutuf13
Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away