https://twitter.com/kinaba のログ (twilog の方が便利です。)
| GCJ 、 friends に足したい人が 10 人ではとても足りなすぎる | |
| 1+1=2 の証明って "S(0)+S(0)=S(S(0)+0),S(0)+0=S(0),S(S(0)+0)=S(S(0)),S(0)+S(0)=S(S(0))" の 67B で済むだろ JK 、と思ったら、 Russel のあれって ZFC での 1+1=2 を愚直に証 ... | |
| ヒルベルトとかゲンツェンとかはやっぱり偉大だなあということがよくわかる | |
| @nagise 1 の定義は "0 の次の数 " で 2 の定義は "0 の次の次の数 " で、 "x の次の数 " と "x+(0 の次の数 )" が常に等しいというのは定義ではなく定理、というのがわりと一般的なスタイルだと思います | |
| @alohakun あーいや、もちろんそうなんですけど http://us.metamath.org/mpegif/1p1e2.html に使われてる範囲ではその差は特に出てないような | |
| @taroleo ありがとうございます！助かります！実際のライセンスもこういう箇条書きで書かれていて欲しい… (^^; | |
| ていうか違うよ、これ、 1.0+0.0i + 1.0+0.0i = 2.0+0.0i の証明しとるやんそりゃ大変ですよ奥さん | |
| @alohakun 360 頁かかって証明されてるのがどっちなのか原本に当たってるんですけど全然読めない… ( 汗。複素数の方なら普通の数学でもマジメにやるとこれは 100 ページくらいはかかると思う | |
| o1p1e2 は普通 1+1=2 と言われたときに想像する定理そのもので、これは oa1suc を inline 展開して定数畳み込めばさっき張った 67B の証明になる。 1p1e2 はデデキントの切断上での加算の well-definedness とか証明が必要なの ... | |
| 54.43 はそのどちらでもなく cardinal 同士の加算を扱ってるように読めるのだけど。ここから o1p1e2 が出るのかな。わからんな。 | |
| 結論：よくわからん | |
| けどまあ「 1518 個のサブ定理」てのは「 GMP を使って 1+1 を計算させると依存する関数は 80 個でした 1+1 に関数 80 個！」てのと同じなので（ o1p1e2 を直接証明すればこの形式化でも 100step はかからない）どうなのかなーとは思う | |
| あさって出発なのにプレゼン資料が１枚もできてないというよくある状況 | |
| @anemo 単に、仕事さぼって開始時刻ギリギリにスタンばってたら順位が上になっただけでしかないという噂… | |
| OSI 参照ライセンス：ライセンスを７つのレイヤに分けて定義する | |
| http://www.books884.jp/ 復活してた！！！ | |
| 正直バラモスは偉そうすぎるのでアイコン変えたくなっているのは秘密 | |
| ドラクエ３で一番好きなモンスターはアルミラージだし | |
| うさみみ∩∩ | |
| そして自分でしっくりこなかったので戻す | |
| http://code.google.com/p/support/wiki/FAQ#Why_do_you_only_offer_a_small_set_of_licenses? http://google-opensource.blogspot.com/2008/05/standing-against-license-proliferation.html お願いしても聞いてくれなさげだなー。諦めよう。 github 辺り行ってみるか | |
| Google Code のは、 NewBSDL と LGPL と Artistic/GPL を選択肢から除いて、 AGPL と zlib/libpng ライセンスを入れれば宣言通りほとんどの開発者の needs を満たしつつライセンスの発散を防げると思うんだけどなー | |
| 帰るー |