Coqチュートリアルへのアドバイスやご指摘
-
- いいね！0
Takashi Miyamoto
@tmiya_
今日の形式手法勉強会で使用した #Coq チュートリアル資料です。間違いとかあればご指摘頂けると嬉しいです。 http://www.slideshare.net/tmiya/coq-tutorial #Coq #fm_forum
2011-04-23 23:30:13
Takuya Hitomi
@takuchan
@tmiya_さんの #Coq チュートリアル資料 の24ページの下の注釈でCoqでもとまらない計算を記述することが可能だと書かれているけど、私の理解とは違う。
2011-04-23 23:50:43
Takashi Miyamoto
@tmiya_
@takuchan チュートリアル資料の間違いを訂正したいのでもう少し詳しく教えて頂けないでしょうか？CoInductiveの所の私の理解が不足してるのかも、です。
2011-04-23 23:55:22
Takuya Hitomi
@takuchan
@tmiya_ CoFixpointにおいて再帰的な呼び出しを行うことができる場所というのはCoInductiveに定義されたデータ型のデータ構築子の内側に限定されています。
2011-04-23 23:59:15
Takuya Hitomi
@takuchan
@tmiya_ その制約と、CoIndutiveなデータ型のデータ構築子に関してのみ評価戦略を遅延評価にすることによって、無限のデータ構造と、停止する関数のみ記述可能であるという、一見両立しないように見える事を両立させているはずです。
2011-04-24 00:00:46
Takuya Hitomi
@takuchan
@tmiya_ これらの制約によって例えばCoInductiveに定義された無限Listに対するFilter関数は定義できません。Inductiveに定義されたListに対するFilter関数は定義可能です。
2011-04-24 00:02:40
Takuya Hitomi
@takuchan
@tmiya_ 詳細は http://amzn.to/fH5haz の13章に書かれています。http://bit.ly/gX70MI でも触れられています。greatest fixpoints and strong normalisation could co-exists
2011-04-24 00:11:06
Takuya Hitomi
@takuchan
@tmiya_ あと個人的な意見なのですが、Curry-Howard対応のところでsimpl tacticsについて言及してほしいです。simpl tacticsの妥当性は正にCurry-Howard対応が存在することによって保証されているので…
2011-04-24 00:21:16
Takuya Hitomi
@takuchan
#Coq チュートリアル資料の内容がすばらしい。 http://bit.ly/fQ8vpn 述語論理の演繹規則とtacticsの対応関係なんかが一覧で初めに提示してあると、全体の見通しがよくなるかもしれない。
2011-04-24 00:29:23
Takashi Miyamoto
@tmiya_
@takuchan 解説ありがとうございます。チュートリアルをどう直すか考えてみます。確かに制約が多いので、CoInduction使えば書ける、と書くのはまずいですね。
2011-04-24 00:35:12
Takuya Hitomi
@takuchan
@tmiya_ ｢Coqでは停止しない関数は記述できない｣しかし｢無限リストなどは扱うことが可能である｣と書くのが正しいと思います。あるいは私が知らない何らかの方法で停止しない関数が記述可能なのでしょうか？それができると定理証明支援系として破綻するので、ないと思いますが…
2011-04-24 00:44:11
Takashi Miyamoto
@tmiya_
@takuchan ありがとうございます。無限リストを扱える話と、停止しない関数と、私が正確に書けてなかったのがまずかったです。そのように修正しようと思います。＞｢Coqでは停止しない関数は記述できない｣しかし｢無限リストなどは扱うことが可能である｣と書くのが正しいと思います。
2011-04-24 01:51:40
Takashi Miyamoto
@tmiya_
Coq で P:Prop の時に、~~~P -> ~P の証明をどう書くのが初心者に判りやすいでしょうか？ライブラリの定理やautoの類を使っては駄目として。最初にunfold notするのが実は判りやすいですかね。みんなはどう証明書くだろうか？#Coq
2011-04-24 01:59:36
@formal_de_hyde
停止性の証明は算術で行われる範囲？例えばGoodstein関数とかは書けない？ @tmiya_ Coqでは停止性を保証したプログラムしか書けない。
2011-04-24 08:42:41
Takashi Miyamoto
@tmiya_
@formal_de_hyde Goodstein関数は詳しく無くて良く解りません。例えばCollatz問題で初期値nに対して何回の操作で1になるかの回数を返す様な関数はCやHaskellで書くのは容易いですが、Coqでは(Collatz予想が解けるまでは)書けないはずかと。
2011-04-24 08:53:48
@formal_de_hyde
やっぱり、やってたか。 Contribution: Cantor On Ordinal Notations http://coq.inria.fr/pylons/contribs/view/Cantor/v8.3
2011-04-24 08:54:35
@formal_de_hyde
Goodstein関数というのは、停止はするんだけど、それが算術では証明できない、というものです。まあ、停止するというのは、もっと強い理論を使って証明されてるわけですが。@tmiya_ Goodstein関数は詳しく無くて良く解りません。
2011-04-24 08:59:06
やまだ
@yam6da
@tmiya_ 僕は「 (~A) が (A->False) に展開される」ことと、「Falseを導く」ことに若干戸惑いました。(含意+Falseを導く)ような演習をやった後なら、unfold notでもついていけると思います。昨日はelim派、今日はちょっとunfoldよりです。
2011-04-24 09:07:06
@formal_de_hyde
Collatz 問題の場合、入力が自然数ではダメでしょうね。Collatzの手続きが停止する自然数の範囲を型として定義（それが自然数全体と同じと予想されてはいるが）すればOKかとは思いますが。@tmiya_
2011-04-24 09:08:32
Takashi Miyamoto
@tmiya_
@formal_de_hyde ご教授ありがとうございます。Contribはあるけど、私が読んで判るかどうか。。。Goodstein関数の例を含めると、どういう風に書くと正確な記述になるのでしょう？
2011-04-24 09:19:58
@formal_de_hyde
ああ、それが余帰納法ってことなのかな？実は新しい言葉はあまり知らないんだよね。 @formal_de_hyde Collatzの手続きが停止する自然数の範囲を型として定義すればOK
2011-04-24 09:25:02
@formal_de_hyde
ええと、私のつぶやきは、単に質問なので、今のところ置いておいて結構です。任意の関数の停止性を証明する理論はないって、萩谷昌己氏もbitで書いてたし。@tmiya_ Goodstein関数の例を含めると、どういう風に書くと正確な記述になるのでしょう？
2011-04-24 09:28:41
@formal_de_hyde
「止マレ！」といえばハルヒ、「止れ！」といえば7bits。ああ、なんか自爆ツイート。http://nicosia.is.s.u-tokyo.ac.jp/pub/essay/hagiya/7bits/stop
2011-04-24 09:36:26