C++で定理証明(?)
uezato yuya
@ranha C++のtemplateは良く知らないけど、全部判明してからじゃないと一致性チェック出来ない?(多分部分特殊化された状態でふにゃふにゃしたものをstructuralに見てくれない?)のでこれでヤるのは無理かなーと思った。(2009-10-18 17:52:09) link
@ranha うーんなんかC++ではむりぽいのう… http://d.hatena.ne.jp/ranha/20091018/1255857502(2009-10-18 18:22:49) linkKazuhiro Inaba
@kinaba #proofparty C++でa+0=0+aの怪しげな証明をば… http://codepad.org/L4feGX1J(2009-10-19 17:40:01) link
@kinaba proposition用テンプレートを特殊化して勝手にインスタンス作られると破綻する。もちろん型安全性を壊す様なことをされると破綻する。停止しない計算を書かれても破綻する。そもそもグローバル変数を使い回すせいで二重帰納法されると破綻する。(2009-10-19 17:42:47) link
@kinaba addみたいなinductiveな関数を汎用に追加できるようにするのは、やればできるけど面倒なのでやってないだけ。(2009-10-19 17:44:26) linkkikx
@kikx ふむふむ、これは型theoremのインスタンスpが作れたから証明できたってことだな(2009-10-19 18:49:40) link
@kikx *pfがNULLでもいいところがなんか問題なきもしなくもないがよくわからん(2009-10-19 18:58:58) link
@kikx このままだと、forall y , (forall x, x+0=0+x) -> y+0=0+y. にできないなあ。(2009-10-19 19:15:03) linkめどすけ
@heppoko_maid @kikx なるほど。ざっとしか見てませんが、induction stepは関数になるので*がついてると。たしかにNULLだと困りそうですが、NULLにはならないように見えますので問題ないのでは。(static assertでNULLチェックできれば追加するといいかも)(2009-10-19 19:28:21) link
@kikx あーわかったぞ、templateはforallする変数名とPropの引数名がまじってるからよくないんだな(2009-10-19 20:07:42) link
@heppoko_maid @kikx これは正確には、forallという名前付けの問題(?)のように見えます。nat::forallはinductionに特化した証明になっているので、沖句さんの使っているforallのような(functor的な)使い方はできないですね。(2009-10-19 21:00:52) link
@kikx こんな感じでforall に apply をつけてみたんだけど、NとYが違うのでまだうまくいってないのです。http://codepad.org/d3ELuDVL(2009-10-19 21:23:21) link
@kikx たぶん、T -> Y -> subs::type のインスタンスがあれば残りは埋められるんじゃないかなと思っているのです(2009-10-19 21:25:43) link
@heppoko_maid @kikx こうやろうとすると、forall::applyの証明がパラメータYの構造に依存してしまうような。forallは普通の定義にして、inductionからforallまたはsubtypeが出てくるようにすればいいのかなーと、なんとなく思ってます(2009-10-19 21:32:52) link
@ranha Conceptあったら状況は変わったんだろうか・・・。うひっ。(2009-10-19 23:41:10) link
@kinaba 先程のa+0=0+aを少し説明すると、「X=Yの時に限りeq型の値が作れる」ように型を作ってます。eq_refl/tran/symm等だけがeqを作れる”公理”。他の(真っ当な)手段では作れない。（確かにそう作ってある、とは誰も保証してないので、ここはそう信じる部分。）(2009-10-20 00:05:52) link
@ranha C++は中身書かなくて良いから型さえ書けりゃあ証明した事に成る。ぶもも。(2009-10-20 00:08:54) link
@kinaba その準備の上で、inductive_proof::base()はeq<0+0,0+0>型の値を作っていて、同step()は、eq<0+N,N+0>の値が与えられれば、eq<0+s(N),s(N)+0>の値を作れるよ、という関数。あとは合わせて帰納法。(2009-10-20 00:10:43) link
@kinaba ただし、帰納法を回す側は、「eq<0+s(N),s(N)+0> step( eq<0+N,N+0> ) という型のつく関数があるなら、確かにeq<0+N,N+0>からeq<0+s(N),s(N)+0>は作れるんだろう」と仮定しちゃっているんだけどこれは本当は間違いで(2009-10-20 00:12:49) link
@kinaba というのは、eq<略1> step( eq<略0> x ) { return step(x); } としてしまえば型チェックは通るけど、これじゃ無限ループして eq<略1> 型の値は作れてない。間違い。これを避けるために、本物の証明記述言語は、無限ループは書けないようになってる。(2009-10-20 00:15:55) link
@ranha .@kinaba 面白かったので、私が勝手に面白いみたいなエントリをはてなに書こうと思ってたんですけどそれはちょっとクオリティ下げて他の人に刺される気がするので、良かったらblogで解説してください！(2009-10-20 00:17:28) link
@kinaba @ranha さんが刺されて大惨事流血沙汰になったブログは面白そうなのでちょっと見てみたい…じゃなくて、はい、後でまとめておきます。たぶん水曜の夜になります(2009-10-20 00:43:11) link
@heppoko_maid 前に書いていたのは、nat_ind P := P 0 -> (forall x. P (S x)) -> forall x. P x が帰納法なので、forallをbasisとして用意しておいてそれをsubstに適用したほうが簡単じゃないかと思った次第。(2009-10-20 01:40:59) link
@heppoko_maid 帰納法をつかって(natに特化した)forallを言ううまいやり方はどうも思いつかないなあ。(2009-10-20 01:41:37) link
@heppoko_maid substが完全一致ではなくて、ちょっと弱めてeqなのは言えるのかもしれない。(2009-10-20 01:44:16) link
@ranha うーん 多分加算可換性をC++のコンパイルタイムに証明出来た気がする・・・。Lemma毎に取りあえずnamespace分けていたのだけれども、そうするとパターン変数(何の意味も無い兎に角パターン変数だけ表す)が全部別々になって悲しいので、共通に括りだしてやり直せば・・・。(2009-10-20 04:39:46) link
@ranha forallの形でやりにくい(forallな変数が2つとか出てくると)ので、9個ぐらいまでの場合を準備しておいてどうこう、とやるか、やっぱりパターン変数をglobalに置いてどっこいしょみたいな感じなのかなぁ・・・。という。(2009-10-20 04:41:00) link
@ranha namespaceってtemplate引数持てないのかぁ。なんかもう普通に依存型のモジュールとかではぼそぼそとか思ったけど。(2009-10-20 12:21:21) link
@kinaba 可換性もやってみようとしたけどめんどうだ。http://codepad.org/DydSnKP0 (途中)。nat::forall から Prop[X/N] を導くには N がzeroとsuccからinductiveに作られてることの証明が必要。つまりNの型が…。(2009-10-20 12:33:06) link
@ranha ただforall tな所に型が潜り込んでで縛りが無い(例えばzeroとsuccに関係性が無い)ので、ダメダメだなーと思います。ふーみゅ・・・。一応証明テンプレート(baseとstep)があるのでユーザはそれに則る様にすれば・・・とは思うんですが。(2009-10-20 14:37:45) link
@ranha なんだろう、Conceptは知らないんですけど、Conceptがあればtype family的な事が出来て、一見無関係な型に制約を付けて無関係では無くしたり、後は明らかに違法なものが渡ってくる事を防いだりは出来るのかなぁ・・・。(2009-10-20 14:38:30) link
@ranha struct Dummy{}; struct zero{}; template struct succ {}; これだと、succみたいなのも出来るのがソレっていう感じなんですが、一方succみたいなパターンを表す型も渡したいので…(2009-10-20 14:56:15) link
@kinaba @kikx (forall x, P x) の証明オブジェクトが帰納法のベースとステップの証明をメンバ変数に持っておくのが正攻法なんですけど、帰納法ステップって多相型の関数なので、型を一度もごまかさないで変数にとっとくのってC++だと無理なんですよね、これ。(2009-10-20 16:27:04) link
@kinaba forallを帰納法に特化させない場合も同じことで、template P operator()(X x) な関数テンプレートを値として持たねばならぬ。C++/DよりJavaかScala辺りでやった方が多分楽。(2009-10-20 16:33:59) link
@kinaba @ranha forall::conv が、返値型がPropだけど実際にはProp型のオブジェクトを作れてないので、その辺がよろしくないです。(2009-10-20 16:40:54) link
@ranha . @kinaba そこはもう完全に不味い匂いがぷんぷんぷんぷんする所なんですが、そもそも不味いですけども、C++的にどのタイミングでどのくらいテンプレート周りが固まって行くかとか分からないので全体が霧掛かって分からない感です。取りあえずソコを考え直します。(2009-10-20 16:48:25) link
@kikx http://codepad.org/AjZoGD52 やっとコンパイル通ったよー ＞@kinaba @ranha @heppoko_maid(2009-10-20 17:39:59) link
@ranha forallの形を辞めて、template引数で渡って来た値の意味を全称変数にしちゃって、帰納的操作を全部隠蔽してそこに投げさせる感じかなー(2009-10-20 17:49:21) link
@kinaba @kikx ∀x(0+x=x+0) の証明オブジェクトじゃなくて 任意のxに対して(0+x=x+0)の証明オブジェクトを返すジェネレータを作ってる感じですかね。これで ∀x∀y(y+x=x+y) の二重帰納法回せるかな…(2009-10-20 17:50:52) link
@kikx A->B は全部 template struct AimplB { static B proof() {}; }; で表現しないと、どうしようもない気がするけど、実際にインスタンシエートされないと型があってるのかわからんなあ(2009-10-20 17:53:33) link
@kikx やっぱりインスタンシエートしないと型チェックされないのがいかんなあ。コンセプトとか使えばいいわけ？(2009-10-20 18:01:02) link
@ranha 私のヤツは実際に値入れてまわすと死ぬなぁ・・・。これは良く無い・・・。あとLeibniz Equalityも書こうと思ったけど酷い感じになる取りあえず晩ご飯！！(2009-10-20 18:01:17) link
@kinaba 具体的な値が与えられたときだけ動くんだから、そりゃ二重帰納法でもなんでもできるか。それもそうだ。genericsじゃなくてtemplateなC++でやるなら、forallの証明をチェックするのは諦めてforallをインスタンス化したらチェックが初めて走る、の方がとっても自然だ(2009-10-20 18:01:26) link
@kikx C++だと証明されたプログラムとして使うなら、結局有限個のインスタンスに対して証明できれば十分だし、これでいいのかなあ(2009-10-20 18:07:35) link
@ranha Conceptは一体何が出来たんだろう夢膨らむ。いや膨らまないけど…(2009-10-20 18:16:19) link
@ranha ていうかテンプレート引数はソレ自体の型が無い(情報が無い)ので、依存型みたく出来ない(あいつらは一応Πx∈T.P(x)みたいな感じで情報はある)のでそういう所でC++は違うのかなーっていうか。(2009-10-20 18:20:38) link
@kikx struct forall { template FroallImpl::prop proof(ForallImpl proofed); } にすればいい気がしてきた(2009-10-20 19:11:07) link
@ranha C++で再びNat上での加算の可換性の証明を行った。 http://d.hatena.ne.jp/ranha/20091021/1256055346(2009-10-21 01:16:24) link
@ranha 物凄くどっち付かずに成っている・・・。kinabaさんの方法だとコンパイル時に強めのチェックが掛かるけれども今のままだと少し手厳しいのと、私が１つ前に張ったconv付き(forallの全称変数を具体化)のヤツはまぁ何とか残念にくぐり抜ける系だったので、もうそれを認めるとか…(2009-10-21 01:44:39) link
@ranha kikxさんのと今張ったものは、コンパイル時の「証明本体」の部分のチェックがゆるゆるガバガバすぎ。はふぅ。(2009-10-21 01:45:50) link
@ranha ああー でもaddの定義を変えて、元のeq_addにすれば何とか成るかも…(2009-10-21 01:50:05) link
@kinaba http://bit.ly/O3ywA にっきかいた。#proofparty の人たちには別に新しいことは何も書いてないですが(2009-10-22 02:20:51) linkhttp://twitter.com/ranha/status/4963443406
http://twitter.com/ranha/status/4963710852
http://twitter.com/ranha/status/4992309733
http://twitter.com/ranha/status/4992902814
http://twitter.com/ranha/status/4993087027
http://twitter.com/ranha/status/4998693697
http://twitter.com/ranha/status/4998668844
http://twitter.com/ranha/status/5012168330
http://twitter.com/ranha/status/5012178660
http://twitter.com/ranha/status/5012427153
http://twitter.com/ranha/status/5013852410
http://twitter.com/ranha/status/5014581387
http://twitter.com/ranha/status/5014724694
http://twitter.com/ranha/status/5014907543
http://twitter.com/ranha/status/5014961041
http://twitter.com/ranha/status/5021794451
http://twitter.com/ranha/status/5022366059
http://twitter.com/ranha/status/5022390225
http://twitter.com/ranha/status/5022477888
http://twitter.com/ranha/status/5009375909
http://twitter.com/kinaba/status/4986574175
http://twitter.com/kinaba/status/4986609522
http://twitter.com/kinaba/status/4986629525
http://twitter.com/kinaba/status/4992837647
http://twitter.com/kinaba/status/4992942470
http://twitter.com/kinaba/status/4992987276
http://twitter.com/kinaba/status/4993053072
http://twitter.com/kinaba/status/4993650737
http://twitter.com/kinaba/status/5009660665
http://twitter.com/kinaba/status/5013585023
http://twitter.com/kinaba/status/5013673067
http://twitter.com/kinaba/status/5013758164
http://twitter.com/kinaba/status/5014600290
http://twitter.com/kinaba/status/5014726804
http://twitter.com/kinaba/status/5048073877
http://twitter.com/kikx/status/4987449708
http://twitter.com/kikx/status/4987553208
http://twitter.com/kikx/status/4987765703
http://twitter.com/kikx/status/4988486871
http://twitter.com/kikx/status/4989678555
http://twitter.com/kikx/status/4989716060
http://twitter.com/kikx/status/5014473813
http://twitter.com/kikx/status/5014632634
http://twitter.com/kikx/status/5014721330
http://twitter.com/kikx/status/5014803334
http://twitter.com/kikx/status/5015583215
http://twitter.com/heppoko_maid/status/4987936670
http://twitter.com/heppoko_maid/status/4989307974
http://twitter.com/heppoko_maid/status/4989831474
http://twitter.com/heppoko_maid/status/4994894814
http://twitter.com/heppoko_maid/status/4994908081
http://twitter.com/heppoko_maid/status/4994963273
