2013年12月25日

進捗アドベントカレンダーを開いた感想

進捗アドベントカレンダー、昨日で全ての記事がそろいました。
参加してくださった皆様、ありがとうございます。
でもやっぱりこんなのに参加するなんて奇特な方々だなあ、と思います。

さて、振り返ってみると、一番手(私)がいきなり出したは良いけどconnpassのページを更新してなかったり、なんだか記事の最初で「なんでこんな企画考えたんでしょうあの人」なんていってきた方がお二方ほどいたり・・・
なんかばたばたしてますね。
しかも皆さんなんだかんだで進捗ありありでしたね。
お一人くらい、「進捗ダメです」画像を五つくらい並べてくるかと思ってたんですが。
・・・ああそうか、始めた人間がくそまじめっぽそうなのを書いてしまったからですね。
空気読んでないのは私でした。申し訳ないです。

まあしかし、日付が変わる前から担当者のTwitterのページを開いて、そこからブログがあればそこも開いておいて、日付が変わってすぐとか、ちょこちょこチェックして、ということをやるのはなかなか楽しかったです。
本人が申告する前にconnpassの更新始めたりとか。

そういえば、申告方法を事前に決めていなかったのにあとで気づいたのが一番の失敗でしたね。
最終的には皆さんが私にtweetすることで私が載せる、という形にしてしまいましたが。

アドベントカレンダーを次にやるとしたら、次の二点を気をつけたいですね。
・担当日をどうするか。参加時点で希望を出した方が楽。Qiitaさんのアドベントカレンダーは参加する日付も指定出来るみたいなのでそっちの方が良かったかな。
・申告、更新方法をどうするか。これまたQiitaさんだと自分で更新できましたね。やっぱそっちの(ry

以上、ちょっとした反省とか所感でした。
これから一週間という短い間の年末、なんとか少しでも進捗を出したいものですね。
posted by chiguri at 00:56| Comment(0) | 雑多

2013年12月14日

Coq/Agdaのどちらを使う?

この記事はTheorem Prover Advent Calendar 14日目の記事です。

さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら

Σ(●△●)<Isabelleの人が一人で大半埋めてるじゃねえか!?

というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。

え、CoqとAgdaのことはnotogawaさんが書いてただろって?
細けえこたぁいいんだよ!

・CoqとAgda、どちらを使うべき?


好きな方を選べば良いと思うのですが、個人的な考えを挙げます。

1:性質+証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関してはAgdaもたくさん使われていますので、それこそ好みでいいでしょう(個人的にはCoqがいいと思いますが)。
2:プログラム記述+検証についてはCoqの方がいいです。こちらは型や関数の記述自体は割と単純であることを想定しています。tacticもいいですし、SSReflectも便利(らしい)です。
3:型を複雑にして、いろいろな性質を型に持たせたプログラミングをしたいならAgdaの方がいいです。Coqだとプログラムを証明と一緒に(tacticで)書く勇気が必要になります(そうじゃないとやっていられません)。慣れればそれなりにできますが、いちいちイライラします。
4:型の階層を意識したいなら断然Agdaです。なにせCoqはSet/Prop/Typeの区別しかしませんし(内部でTypeのヒエラルキーは計算していますが、表に見えづらいです)。

1は比較的どちらでも良いですし、4は迷いようがありません。
したがって、おそらく悩むことが多いのは2/3の問題でしょう。
選択の一助になれば幸いです。

ちなみに、OCamlとHaskellの一方を使っているから、はほとんど理由になりません。
どうせ大した差ではありません。
スタートアップで一日差がつくかつかないかくらいです。

・inversion大好き


inversion tacticは便利です。(すでに何回主張したか忘れた)
簡単に説明すると、inversion tacticは「この帰納的述語が成り立つためにはどういうことが成り立っている必要がある?」というのを定義から見つけてくる優れものです。
このとき、成り立たないパターン(帰納的述語のコンストラクタのパラメータに一致しない)があるときは勝手にそれらに関して矛盾を作って証明してくれます。
(よって「起こりうるパターンが一つもない」、つまり矛盾していれば証明完了するわけですが、それはあくまで結果論)
inversionなかったらCoqの証明を勧めるとかありえませんね。
(ただしinversionの生成する項ははっきり言って読めない)
Agdaで同じこと?・・・reflection使えば、できたりするのかな・・・?

・で、証明しないの?


最近AgdaでD-Case書きまくってるので勘弁してください。
次があったら例題使って、最初の4分類が何を言いたいのか書いてもいいのですが・・・
タグ:Coq Agda
posted by chiguri at 00:14| Comment(0) | Coq

2013年12月06日

よしひろさんの問いにAgdaで答えよう

これはTheorem Prover Advent Calendarとはまったく関係のない記事である。
いや、来週くらいに書くけど。

昨日(世界のどこかの時間では)の担当だったよしひろさんが書いた記事
依存関係のある値のうちの一部をrewriteしようとしたときの問題
に最後にこんな一言があった。
> また、依存型に定評のあるAgdaではどうなるかなども興味深い。

なるほど、この問いには答えねば。
そう思いAgdaを起動してまねた記述を作る。
ファイル名はYIquestion.agdaとする。

module YIquestion where

open import Data.Nat
open import Relation.Binary.Core

postulate
f : (n : ℕ) → n > 0 → ℕ
h : (n : ℕ) (H : 2 * n > 0) → f (2 * n) H ≡ n

postulate
x : ℕ
H : x > 0

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = ?

同じ流れならここでeqを展開(rewrite相当)、Coqではエラーの出る展開である。
だが、エラーメッセージがなんか違うぞ・・・

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the inferred
indices [x] with the expected indices [2 * 1]
when checking that the expression ? has type f x H ≡ 1

(●△●)??
Hが問題とかそれ以前の問題のようだ。
え、なに?xと2*1をunifyしようとして詰まった・・・??
何を言ってるのだろう。

というヒントを元に作った正解はこちら。

goal' : (x : ℕ) → (x ≡ 2 * 1) → (H : x > 0) → f x H ≡ 1
goal' .2 refl H = h 1 H

goal : (x ≡ 2 * 1) → f x H ≡ 1
goal eq = goal' x eq H

最初のgoal'の記述は

goal' x eq H = ?

からeqを展開して作成した。
これを見ると何となく見えてくるのは、
どうもAgdaは引数が実際になんだったかしかreflで書き換えないらしい
ということである。
つまり、Coqの場合同様にHが依存していることももちろん問題だったのだが、それ以前に
xが適当に置かれた変数であるせいで、展開できない
ということの方がよっぽど問題だったという。

やっぱりAgdaのエラーメッセージはわかりにくい・・・

ちなみにCoqでは上のやり方に相当するパターンマッチではなくeq_indなどで書き換えているので注意。
posted by chiguri at 21:39| Comment(0) | Agda

2013年12月01日

進捗報告

進捗アドベントカレンダー1日目の報告書
・アドベントカレンダー
 幸いなことに23人もの発表者が集まった。こんな訳の分からないアドベントカレンダーに参加してもらって奇特に思えて仕方がないありがたい限りである。

・第一日目担当者の予想
 進捗が芳しくないこともあり、安直な方向へと進んだ結果、予想通り自分であった。自分で決めるのだから予想を外せば良いものを。

・FOSEでの発表
 いくらなんでも話を縮めるために例を簡略化しすぎたようだ。後で元担当教員にだめ出しを食らった。

・そのほか
 きっと24人目が来てくれると信じているが、来なかったら多分24日目はまた私だ。
 そして今日はやることがあってやばい。そんな先の話はどうでもいい。11月戻ってこい。

以上が私の進捗である。
さて、次はかの有名なよんた様(keita44_f4さん)である。
よんた様、進捗はいかほどでございましょうか?
posted by chiguri at 00:16| Comment(0) | 雑多