brainfuck interpreter in Coq

Coq Haskell

Haskell 、Erlang の次のブームは Coq に違いありません。とりあえず基本ということで、Coq でひねりのない brainfuck インタプリタを書いてみました。動作例。Coq のコードが色づけできないとは何事か。

Eval compute in
  (finite_execute "
    +++++++++[>++++++++>+++++++++++>+++++<<<
    -]>.>++.+++++++..+++.>-.------------.<++
    ++++++.--------.+++.------.--------.>+.
   " "" 500).

     = "Hello, world!"%string
     : string

残念ながら (?) Coq では停止性が保障された関数しか定義できません。ここでは最大評価ステップを指定しないといけないという仕様にしてごまかしています (引数の 500 がそれ) 。

Coq は定理証明器なので定理が証明できます。以下は 「Hello, world! のプログラムは Hello, world! を出力する」という定理。

Theorem Hello_world:
  finite_execute "
    +++++++++[>++++++++>+++++++++++>+++++<<<
    -]>.>++.+++++++..+++.>-.------------.<++
    ++++++.--------.+++.------.--------.>+.
  " "" 500 = "Hello, world!"%string.

以下それの証明。不適切極まりない例ですね。Coq で FizzBuzz のパクリだし。

Proof.
  compute.
  reflexivity.
Qed.

さらに、Coq で定義した関数や証明からプログラムを抽出することができます。

Extraction Language Haskell.
Extraction "Brainfuck" init_thunk evaluate.

これで Brainfuck.hs が生成されます。Haskell は当然停止しない関数も定義できますので、ちょちょいとドライバ (生成されたコードを呼び出すコード) を書いてやることで Haskell による Brainfuck インタプリタが作れます。それはなんと Hello, world! のプログラムが正しく扱えることが証明済みのインタプリタなのです。ドライバ部分にバグがなければですが。

$ time runhugs Main.hs `cat hello.bf`
Hello, world!

real    0m0.610s
user    0m0.380s
sys     0m0.160s

$ time runhugs Main.hs `cat quine.bf` > quine2.bf

real    0m5.921s
user    0m0.450s
sys     0m5.400s

$ diff quine.bf quine2.bf


以下コード。

Section Brainfuck.

Require Import ZArith.
Require Import List.
Require Import Streams.
Require Import Ascii.
Require Import String.

Open Scope Z_scope.

Inductive Inst : Set :=
  | i_incr  : Inst
  | i_decr  : Inst
  | i_right : Inst
  | i_left  : Inst
  | i_getc  : Inst
  | i_putc  : Inst
  | i_open  : Inst
  | i_close : Inst
  | i_exit  : Inst.



(** パーサ **)
Section Parser.

Fixpoint parse_aux (s : string) :=
  match s with
  | EmptyString => nil
  | String "+" s' => i_incr  :: parse_aux s'
  | String "-" s' => i_decr  :: parse_aux s'
  | String ">" s' => i_right :: parse_aux s'
  | String "<" s' => i_left  :: parse_aux s'
  | String "," s' => i_getc  :: parse_aux s'
  | String "." s' => i_putc  :: parse_aux s'
  | String "[" s' => i_open  :: parse_aux s'
  | String "]" s' => i_close :: parse_aux s'
  | String _ s' => parse_aux s'
  end.

Definition parse (s : string) : (list Inst * list Inst) :=
    (nil, parse_aux s).

End Parser.



(** 評価器 **)
Section Evaluator.

(* 現在の命令を取り出す *)
Definition fetch (c : (list Inst * list Inst)) : Inst :=
  match c with
  | (_, i::_) => i
  | (_, nil) => i_exit
  end.

(* 命令列の zipper を進める *)
Definition next (c : (list Inst * list Inst))
    : (list Inst * list Inst) :=
  match c with
  | (l, i::r) => (i::l, r)
  | (l, nil) => (l, nil)
  end.

(* 現在のセルに 1 を足す *)
Definition incr (s : (Stream Z * Stream Z)) : (Stream Z * Stream Z) :=
  match s with
  | (l, Cons x r) => (l, Cons (x + 1) r)
  end.

(* 現在のセルから 1 を引く *)
Definition decr (s : (Stream Z * Stream Z)) : (Stream Z * Stream Z) :=
  match s with
  | (l, Cons x r) => (l, Cons (x - 1) r)
  end.

(* ヘッダを右のセルへ動かす *)
Definition right (s : (Stream Z * Stream Z)) : (Stream Z * Stream Z) :=
  match s with
  | (l, Cons x r) => (Cons x l, r)
  end.

(* ヘッダを左のセルへ動かす *)
Definition left (s : (Stream Z * Stream Z)) : (Stream Z * Stream Z) :=
  match s with
  | (Cons x l, r) => (l, Cons x r)
  end.

(* 一文字読み込んで現在のセルに書き込む *)
Definition getc (s : (Stream Z * Stream Z)) (i : string)
    : ((Stream Z * Stream Z) * string) :=
  match s with
  | (l, Cons _ r) =>
    match i with
    | EmptyString => ((l, Cons 0 r), EmptyString)
    | String c i' => ((l, Cons (Z_of_nat (nat_of_ascii c)) r), i')
    end
  end.

(* 現在のセルの値を文字として出力する *)
Definition putc (s : (Stream Z * Stream Z)) : ascii :=
  match s with
  | (_, Cons c _) => ascii_of_nat (Zabs_nat c)
  end.

Fixpoint open_aux (d : nat) (l : list Inst) (r : list Inst) { struct r }
    : (list Inst * list Inst) :=
  match r with
  | (i_open :: r') => open_aux (S d) (i_open :: l) r'
  | (i_close :: r') =>
    match d with
    | O => (i_close :: l, r')
    | S d' => open_aux d' (i_close :: l) r'
    end
  | (i :: r') => open_aux d (i :: l) r'
  | nil => (l, r)
  end.

(* 現在の開き括弧に対応する閉じ括弧まで進む *)
Definition open
    (c : (list Inst * list Inst))
    (s : (Stream Z * Stream Z))
    : (list Inst * list Inst) :=
  match s with
  | (_, Cons 0 _) =>
    match c with
    | (l, i_open :: r) => open_aux O (i_open :: l) r
    | _ => next c
    end
  | _ => next c
  end.

Fixpoint close_aux (d : nat) (l : list Inst) (r : list Inst) { struct l }
    : (list Inst * list Inst) :=
  match l with
  | (i_close :: l') => close_aux (S d) l' (i_close :: r)
  | (i_open :: l') =>
    match d with
    | O => (l', i_open :: r)
    | S d' => close_aux d' l' (i_open :: r)
    end
  | (i :: l') => close_aux d l' (i :: r)
  | nil => (l, r)
  end.

(* 現在の閉じ括弧に対応する開き括弧まで戻る *)
Definition close (c : (list Inst * list Inst)) : (list Inst * list Inst) :=
  match c with
  | (l, r) => close_aux O l r
  end.


(* 一ステップ評価する *)
Definition evaluate
    (thunk : ((list Inst * list Inst) * (Stream Z * Stream Z) * string))
:=
  match thunk with
  | (code, state, input) =>
    match fetch code with
    | i_incr  => Some ((next code, incr  state, input), None)
    | i_decr  => Some ((next code, decr  state, input), None)
    | i_right => Some ((next code, right state, input), None)
    | i_left  => Some ((next code, left  state, input), None)
    | i_getc  =>
      match getc state input with
      | (state', input') => Some ((next code, state', input'), None)
      end
    | i_putc  =>
      Some (((next code), state, input), Some (putc state))
    | i_open  => Some ((open code state, state, input), None)
    | i_close => Some ((close code, state, input), None)
    | i_exit  => None
    end
  end.

(* 評価を有限回繰り返す *)
Fixpoint finite_loop
    (thunk : ((list Inst * list Inst) * (Stream Z * Stream Z) * string))
    (count : nat)
    { struct count }
    : string
:=
  match count with
  | O => EmptyString
  | S count' =>
    match evaluate thunk with
    | Some (thunk', Some out) => String out (finite_loop thunk' count')
    | Some (thunk', None) => finite_loop thunk' count'
    | None => EmptyString
    end
  end.

End Evaluator.



(* 初期状態のテープ *)
CoFixpoint inf_tape : (Stream Z) := Cons 0 inf_tape.
Definition init_state := (inf_tape, inf_tape).



Definition init_thunk (code : string) (input : string) :=
  (parse code, init_state, input).



Definition finite_execute (code : string) (input : string) :=
  finite_loop (init_thunk code input).



(* Hello, world! を実行する *)
Eval compute in
  (finite_execute (
    "+++++++++[>++++++++>+++++++++++>+++++<<<" ++
    "-]>.>++.+++++++..+++.>-.------------.<++" ++
    "++++++.--------.+++.------.--------.>+." 
   ) "" 500).



(* Hello, world! のプログラムが Hello, world! を出力することを証明する *)
Theorem Hello_world:
  finite_execute (
    "+++++++++[>++++++++>+++++++++++>+++++<<<" ++
    "-]>.>++.+++++++..+++.>-.------------.<++" ++
    "++++++.--------.+++.------.--------.>+." 
   ) "" 500 = "Hello, world!"%string.
Proof.
  compute.
  reflexivity.
Qed.

(* echo に foo を入力すると foo を出力することを証明する *)
Theorem Echo:
  finite_test "+[,[>+>+<<-]>[.[-]]>]" "foo" 5000 = "foo"%string.
Proof.
  compute.
  reflexivity.
Qed.



End Brainfuck.



(* Haskell のコードを出力する *)
Extraction Language Haskell.
Extraction "Brainfuck" init_thunk evaluate.

以下 Haskell のドライバ。

module Main where

import Brainfuck
import System
import Char

nat_of_int 0 = O
nat_of_int n = S $ nat_of_int (n - 1)

int_of_nat O = 0
int_of_nat (S n) = 1 + int_of_nat n

ascii_of_char = ascii_of_nat . nat_of_int . ord
coq_string_of_string [] = EmptyString
coq_string_of_string (c : s) =
    String0 (ascii_of_char c) $ coq_string_of_string s

char_of_ascii = chr . int_of_nat . nat_of_ascii
string_of_coq_string EmptyString = []
string_of_coq_string (String0 a s) = char_of_ascii a : string_of_coq_string s


mainloop = next . evaluate
 where next None = EmptyString
       next (Some (Pair thunk' None)) = mainloop thunk'
       next (Some (Pair thunk' (Some output))) =
           String0 output $ mainloop thunk'

main :: IO ()
main = do
    args <- getArgs
    let args' = coq_string_of_string $ args !! 0
    input <- getContents
    let input' = coq_string_of_string input
    let thunk = init_thunk args' input'
    putStrLn $ string_of_coq_string $ mainloop thunk

言うまでもないですが、Coq はこういうことをするものではないです (笑) 次はもうちょっと真面目なことをやります。次があったら。