yicesを使ってみようとしてみる
今日 8/5 はIDOLM@STER MASTER SPECIALシリーズの最後となるMASTER SPECIAL 06が発売されるので、まずそれを買います。
そして次に、ぼくのはじめてのりすぷ！！
これは何?
SMT-COMP 2009という、SMTのcompetitionがあります。(SMT-COMPのページを見ると分かるんですが、Yices2で参加してるみたいですね。)
SMTとは何か、という事については。
http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
要するに分かりません。
多分最終的にSAT-Solverに落とし込んでるんでしょうけど、SATっていうかあんまりlogic,logicしたものだと人間には優しくないので、ちょっと優しさを注入してあげた系なんですかね。
分かりませんよー。
インストールしてみる
取って来て、解凍して、ディレクトリbinに入って、./yicesが出来る事を確認しました。
何かやってみる
と言われても・・・。
その他
http://yices.csl.sri.com/language.shtml#language_dependent_types
これはそこまで依存型という意味合いでは無い感じがしますねー。
どのみち、ユーザがこれを使って操作をする、という点では恩恵に授かれる事は無さそう。
型に直接制約が書けるっていうぐらいなのかなぁ・・・。でも確かに便利っちゃあ便利か。型が一貫して満たすべき制約ですね。
(define-type pos (subtype (v::int) (> v 0))) ;; posはintに制約がくっついたもので、値としては1以上になる。 (define x::pos) (assert (= x 0)) ;; ので、これは満たされない
(define-type non-neg (subtype (v::int) (>= v 0))) ;; non-negは値としては0以上となるint まぁ Yicesにはnat型って在ります (define x::non-neg) (assert (= x 0)) ;; ので、これを満たすx(当然ですが、x=0です)はあり得ます (check)
(define-type tst (subtype (v::int) (= v (ite (> v 0) 1 -1)))) ;; iteはif_then_elseの略です。 ;;値によって型が決まるわけでは無いですけど、これは面白いかもしれません。そうかなー ;;vが0より大きな値を持つ時は1に限り、そうで無い時は-1に限る。 ;;つまり、int 1かint -1しか持たない型という事ですね。 (define x::tst) (assert (= x 0)) ;; のでこれを満たすxは存在しない (check)
(define-type tst (subtype (v::int) (= v (ite (> v 0) 1 -1)))) (define x::tst) (assert (= x 1)) ;; xの値は(int 1)か(int -1)で、まぁそうするとありますねというだけ (check)
(define min::(-> x::int y::int (subtype (r::int) (and (or (= r x) (= r y)) (<= r x) (<= r y))))) ;; min は 関数の定義では無くて、型を与えてる事に注意です。 ;; とはいえ、下で(min x y)とかやってるので分かるのですが、 ;; yices的にはuninterupted functionとかで、bodyの無い関数みたいな感じですね多分。これは嘘かもしれません。 ;; min :: (x::int) -> (y::int) -> (r:: subtype int)という感じですね。 ;; で、rの型τは、その値v::τは (v=x か v=y) かつ (v<=x) かつ (v<=y)という感じで ;; x と yで、型τが決まるので、これは依存型っぽいですねー。 (define x::int) (define y::int) (assert (> (min x y) x))
この例では何も吐いてくれないので(x < yの時でもx > yの時でもx = yの時でも明らかですね)
(define min::(-> x::int y::int (subtype (r::int) (and (or (= r x) (= r y)) (<= r x) (<= r y))))) (define x::int) (define y::int) (define z::int (min x y)) ;; まぁτはintの部分集合みたいな感じなのでこれで大丈夫なんでしょう (assert (>= z x)) (check) /Users/ranha/Yices/yices-1.0.21/bin% ./yices -i -e deptype5.ys sat (= x 0) (= y 1) (= (min 0 1) 0)
ちなみに、オプションはyices --helpで出ます。ちなみにiはinteractive,eはモデルを出力する(デフォルトではdisaable!!)で、tcはtype-checking(これもデフォルトではdisable!!)です。
それと、yicesではAlloyあたりと違ってモデルを複数吐くんじゃあ、なくて、1つしか吐きません。
(define-type PC (scalar pc1 pc2 pc3)) (define x::(subtype (y::PC) (or (= y pc1) (= y pc2)))) ;; (define x::PC) (assert (/= x pc1)) (assert (/= x pc2)) (check)
xの型τは値としてpc1かpc2しか取らない型PCのsubsetです。
ので、2つのアサーションを満たすx::τは存在しません。
まとめ
まだAlloyよりは良いんじゃないかなーと思ったんですが、Alloyの方がスタイリッシュですよねー。
で、どう見てもりちゅぷって感じなので、かいじょ→する関数を書こうと思うんですが、これletrecとか無いのでうーん。
Recursive Typeな感じにやろうにも、定義出来る型(再帰なADTは書けるんですが)がdata Mu a = Make (Mu a -> a)なんて出来ないので、うーんという。
それと、これADTから値取り出すとかいう事が出来ないので(recordと同じ感じでselect使ってもダメでした。selectはrecordだけです)、そういう意味でも壊滅的。top-downじゃなくてbottom-upでもそもそと探る感じにすれば方向変えていけるかなー。
妥当なのはRecursive TypeにDependent Type組み合わせるとかかしら。
いやまった
(define-type foo (-> int int)) (define f::foo) (assert (forall (n::nat) (= (f n) (* n (f (- n 1)))))) (assert (= (f 1) 1)) (assert (= (f 0) 1)) (assert (= (f 2) (* 2 1))) (check)
これだなー。
で、これをyicesに投げても帰ってこないので、---max-instances=
ということで、nat全体じゃなくて0<=値<=10な型fact_natを作ってそれでやってみました。
(define-type fact_nat (subtype (n::nat) (<= n 10))) (define-type foo (-> fact_nat int)) (define f::foo) (assert (= (f 1) 1)) (assert (= (f 0) 1)) (assert (forall (n::fact_nat) (= (f n) (* n (f (- n 1)))))) (define x::int) (assert (= (f 5) x)) (check) /Users/ranha/Yices/yices-1.0.21/bin% ./yices -i -e -tc -mi 11 fact.ys unknown (= x 120) (= (f 1) 1) (= (f 0) 1) (= (f 5) 120) (= (f 2) 2) (= (f 6) 720) (= (f 3) 6) (= (f 7) 5040) (= (f 4) 24) (= (f 8) 40320) (= (f 9) 362880) (= (f 10) 3628800) (= (f 11) 39916801) <- なんで... (= (f 12) 479001613) <- 私は餡子が苦手なんですよねぇ・・・。ほんと悲しい
それで結局思うんですけど、普通に計算もしたいし、何か無くしてしまったものも探したいなら、やっぱりちゅらぶりんなPrologだよねーっていう事でPrologなんですけど、Prologはなんか型があれなので、そういう視点から見たさいきょうのぷろろぐを見つければこの世で無敵なんじゃないかという。
http://twitter.com/ranha/status/3131651736
うーんあながち・・・。
処理系としての蓄積がどこにあるのか(それこそPrologをSAT-Solver Baseで実装する)とかっていうのは兎も角として、Prologはちゅらぶりんなんじゃないかなーと思うので。起きたらCurry辺りを漁ってみようかな。
メモ
VS3: SMT Solvers for Program Verification
