みなさん、こんにちは、「発表者」です。 この番組ではリスナーの皆さんに「定理証明」の話題をお届けいたします。 たぶん、今回が最初で最後だと思います。
これから15分ほどの間、お付き合いくださいませ。
それではさっそくメールを読み上げていきたいと思います。 ラジオネーム「とあるHaskell golfer」さんから質問をいただきました。 （ありがとうございます）
「発表者」さん、こんにちは。（こんにちはー）
帰納的なデータ構造が満たす定理の証明は入門書に載っています。 （ふむふむ） でも、業務で使うプログラムに必要なデータ構造は帰納的というよりは 余帰納的であることが多いです。 こんなプログラムが満たす性質を定理証明したいのですが どうしたらよいでしょうか。 （ふむ） ただ証明するだけでなく、証明された定理からマシンで動くプログラムになってほしいです。
会社の同僚に「俺が引退するまでに使われるようになんの？プゲラ」と言われました。 「発表者」さんはこんなことを言われたことはありますか？ どうしたらギャフンと言わせられるか、教えてください。 よろしくお願いします。
というメールでした。
あー、これは言われてみればそうですよねー。 長さ付きのリストについてどうこうとか入門書に載ってますけど。
そんなことはわかってるんだよ！使えないよ！(w
帰納的なデータについては帰納的かつ構成的に証明することになりますから、 手順はよく知られています。
でも余帰納的なデータについての証明法はまだまだ発展途上です。と思います。
余帰納についてなにが難しいかというと、停止性の証明がむずかしい、 証明されたあとのプログラムをextractすることはできるのだろうか、 証明されたあとのプログラムは実際性能が悪いと思うので、 プログラマが普通に書くプログラムとのsemanticsの一致も示したい semanticsの一致というかbisimulationでもいいですけど
など、問題が山積みです。
「発表者」もどうしたらいいかわかりません！
余帰納的なデータを必要とする簡単なプログラムの例としてcat(引数なし)を挙げます。 cat(引数なし)についてどんなことを証明してほしいか、詳しいことは 「発表者の用意したgistのURL」に書いてあります。
URLに用意する文章はたとえばこんなかんじです:
Idris でやるなら
corecord はコンパイルできるのか？
corecord で定義された文字列を使った関数cat⊥を定義できるのか
cat⊥について、入力をもらったら出力した文字列は等しかったことを証明できるか
Idris.Eff catとcat⊥のsemanticsは同じか
(Idris.Eff cat は Haskell でコンパイルされた cat とだいたい同じなので？満足する)
などです。別の定理証明をつかうならこのようなことを定式化して、証明してください
リスナーの皆さま、なにかおわかりでしたらどしどしコメントを送ってくださいませ。
あてさきは「発表者のツイッターアカウント」または 「発表者のつくったgist」につなげるなどでお願いします。 ハッシュタグは（ProofSummit 2015のハッシュタグ）です。
さて、そろそろお別れの時間がやってまいりました。
ぷるーふさみっと2015、ライトニングトーク、ラジオー（仮） お聞きの皆様ありがとうございます。 このつぎの放送は来年以降になるかもしれませんが、たぶんありません。
それでは、まったねー。ばいばーい。