More than 5 years have passed since last update.
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項で定義しです。
RequireImportListArithAsciiString.ImportListNotations.OpenScopestring_scope.Inductiveprim:=PtrIncr|PtrDecr|Incr|Decr|Get.Inductivestmt:=|SNil:stmt|Prim:prim->stmt->stmt|Put:stmt->stmt|Loop:stmt->stmt->stmt.Fixpointparse'(str:string):=matchstrwith|""=>(SNil,nil)|Stringxxs=>let(body,rest):=parse'xsinmatchxwith|">"%char=>(PrimPtrIncrbody,rest)|"<"%char=>(PrimPtrDecrbody,rest)|"+"%char=>(PrimIncrbody,rest)|"-"%char=>(PrimDecrbody,rest)|","%char=>(PrimGetbody,rest)|"."%char=>(Putbody,rest)|"["%char=>matchrestwith|nil=>(LoopbodySNil,nil)|conssrest'=>(Loopbodys,rest')end|"]"%char=>(SNil,consbodyrest)|_=>(SNil,nil)endend.Definitionparsestr:=fst(parse'str).brainf*ckを実行する上で、ここでは配列は自然数から自然数への関数で表し、入力を自然数のリストで表すことにします。配列、ポインタ、入力の組 (nat -> nat) * nat * list nat が環境になります。
ポインタのインクリメント/デクリメント(>/<)、ポインタが指す値のインクリメント/デクリメント(+/-)、入力からの読み込み(,)を処理して環境を更新する関数を以下で与えます。
Definitionrun_prim(env:(nat->nat)*nat*listnat)p:=let'(data,ptr,input):=envinmatchpwith|PtrIncr=>(data,Sptr,input)|PtrDecr=>(data,predptr,input)|Incr=>(funi=>ifNat.eq_deciptrthenS(dataptr)elsedatai,ptr,input)|Decr=>(funi=>ifNat.eq_deciptrthenpred(dataptr)elsedatai,ptr,input)|Get=>matchinputwith|[]=>env|x::rest=>(funi=>ifNat.eq_deciptrthenxelsedatai,ptr,rest)endend.出力 (.)やループ([/])の処理をLtacで行います。
Fixpointappend(s1s2:stmt):=matchs1with|SNil=>s2|Primps=>Primp(appendss2)|Puts=>Put(appendss2)|Loopbs=>Loopb(appendss2)end.Ltacrunenvc':=letc:=evalcomputeinc'inmatchenvwith|(?data,?ptr,?input)=>matchcwith|SNil=>idtac|Prim?p?c'=>letenv':=evalcomputein(run_prim(data,ptr,input)p)inrunenv'c'|Put?c'=>letx:=evalcomputein(dataptr)inidtacx;runenvc'|Loop?c1?c2=>letx:=evalcomputein(Nat.eq_dec(dataptr)0)inmatchxwith|left_=>runenvc2|right_=>runenv(appendc1(Loopc1c2))endendend.これで完成です。
気を付ける点としては、eval compute in x で項 x を評価しておかないと Ltac 内のパターンマッチに失敗する可能性があるところですね。
実際に書いたtacticを走らせてみましょう。
GoalTrue.run((fun_:nat=>0),0,[4;3])(parse",>,<[-<+>]<.").(* 足し算 *)run((fun_:nat=>0),0,[3;3])(parse",>,<[->[->>+<<]>>[-<+<+>>]<<<]>>.").(* 掛け算 *)run((fun_:nat=>0),0,@nilnat)(parse"+[>.+<]").(* 0,1,2... とすべての自然数を出力 *)対話環境で上のtacticを読み込むと、上の二つはそれぞれ 7 (= 4 + 3), 9 (= 3 * 3) とメッセージ欄に表示され、最後のtacticは 0 1 2 ... 無限に自然数が出力されます。
ということで、めでたく(？？)Coqがこの意味でチューリング完全であることが言えました。おしまい。
全体のコード：
https://gist.github.com/erutuf/6203173f602b524a908e422f4a7c480b
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme