https://twitter.com/kinaba のログ (twilog の方が便利です。)
| 先程のa+0=0+aを少し説明すると、「X=Yの時に限りeq<X,Y>型の値が作れる」ように型を作ってます。eq_refl/tran/symm等だけがeqを作れる"公理"。他の(真っ当な)手段では作れない。（確かにそう作ってある、とは誰も保証してないので、ここはそう信じる部分。） | |
| その準備の上で、inductive_proof::base()はeq<0+0,0+0>型の値を作っていて、同step()は、eq<0+N,N+0>の値が与えられれば、eq<0+s(N),s(N)+0>の値を作れるよ、という関数。あとは合わせて帰納法。 | |
| ただし、帰納法を回す側は、「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>は作れるんだろう」と仮定しちゃっているんだけどこれは本当は間違いで | |
| というのは、eq<略1> step( eq<略0> x ) { return step(x); } としてしまえば型チェックは通るけど、これじゃ無限ループして eq<略1> 型の値は作れてない。間違い。これを避けるために、本物の証明記述言語は、無限ループは書けないようになってる。 | |
| @natsutan 涙目でアサヒのsimple&quality colaというのを飲んでます（＞＜） | |
| @kururu_goedel なんとかならないんですかね。僕も問題だと思います。そういうTTLみたいな変数使った実装も結構目にしますけど、負けた気がするので僕は引数に順序入れて減少性を示す、で頑なに書きたい…けど大変ですよねえ。 | |
| 型システムで、止まらないかもしれない→と必ず止まる→を分けて、inhabitedであって欲しいところ(Proof Termを作るところ等)は確実に止まる→を使う、だけだとナイーブすぎて使えなさそうだけど、なんかちゃんとすればちゃんとなりそうな、って、なんか絶対あるよなそういうの | |
| @ranha さんが刺されて大惨事流血沙汰になったブログは面白そうなのでちょっと見てみたい…じゃなくて、はい、後でまとめておきます。たぶん水曜の夜になります | |
| @wraith13 しまいにはドンキホーテで大量購入していたので、前回バラではどこの店で勝ったのか忘れてしまった…思い出さなくては… | |
| computational なのと logical な構成子を分けて考える証明支援系って、そういえば前に講演を聞いた気がする… http://d.hatena.ne.jp/ytb/20090501/p1 この話だ。これは停止性とかそういう話とは別だったと思うけど。 | |
| アサインされました。しかしとりあえず眠いのでまたあした…zzz RT 最萌えの文言とか一番下のメッセージは一旦 @kinaba さんにアサイン、と。 | |
| 可換性もやってみようとしたけどめんどうだ。http://codepad.org/DydSnKP0 (途中)。nat::forall<X,Prop> から Prop[X/N] を導くには N がzeroとsuccからinductiveに作られてることの証明が必要。つまりNの型が…。 | |
| codepadってエラーが出てるコードはpermanentにできないのかな。 | |
| @kikx (forall x, P x) の証明オブジェクトが帰納法のベースとステップの証明をメンバ変数に持っておくのが正攻法なんですけど、帰納法ステップって多相型の関数なので、型を一度もごまかさないで変数にとっとくのってC++だと無理なんですよね、これ。 | |
| forallを帰納法に特化させない場合も同じことで、template<typename X> P<X> operator()(X x) な関数テンプレートを値として持たねばならぬ。C++/DよりJavaかScala辺りでやった方が多分楽。 | |
| @ranha forall::conv が、返値型がPropだけど実際にはProp型のオブジェクトを作れてないので、その辺がよろしくないです。 | |
| @kikx ∀x(0+x=x+0) の証明オブジェクトじゃなくて 任意のxに対して(0+x=x+0)の証明オブジェクトを返すジェネレータを作ってる感じですかね。これで ∀x∀y(y+x=x+y) の二重帰納法回せるかな… | |
| 具体的な値が与えられたときだけ動くんだから、そりゃ二重帰納法でもなんでもできるか。それもそうだ。genericsじゃなくてtemplateなC++でやるなら、forallの証明をチェックするのは諦めてforallをインスタンス化したらチェックが初めて走る、の方がとっても自然だ |