https://twitter.com/kinaba のログ (twilog の方が便利です。)
| ∩(._.)∩ | |
| 昏論会ウィキ http://www45.atwiki.jp/konron 昨日はちゃんと全部追えてなかったので読んでる。shinh さんのチョイスが素晴らしいな。この前の 3SAT で P=NP の話、よくわからんことになっているということがよくわかった。 #konronkai | |
| あらためて、参加者のみなさま、変な遊びに付き合っていただきありがとうございました、と一日遅れでご挨拶。 #konronkai | |
| @salmonpasta へろー ＼(._. ) | |
| @ikegami__ あんまりソートされそうに見えないんですがこれはソートされるんですか （目test | |
| @ikegami__ [2,1,0] が [1,0,2] になりそうな | |
| 「止まるかどうかは（処理系に教えるのが面倒いので）さておき、止まるならこのqsortはちゃんとソートしてる」が証明できればいいやって気分の日は結構あると思うんですけど、そういうのができる証明支援系って何かあるんでしょか。無論そういう項が証明の中に混ざると破滅なのでそこは型ではじく | |
| @takuchan 基本的にはCoqやAgdaと同じで停止すること前提でよいのではないかと思っています。Aと書いたら停止するA。"停止しないかもA (以下nA)"とA->BからはBは演繹できない。演繹できるとすればnB(…が安全かどうか怪しいですが無理なら健全になるまで弱めて…) | |
| @yoriyuki 興味があります。computational な部分と logical な部分を結局分けて考える、というのはCoqもそうですし、割と普及しているやり方だと思うんですが、そこのところもう少し進めてなんとかなりそう/なにかありそうな気がして。 |