2006-04-27 [長年日記]
λ. Agdaの紹介Flash
やねうらおさんのswf形式で動画キャプチャで紹介されていたCam Studioを使ってみたくなったので、Agdaでの簡単な証明風景をキャプチャしてみた。
ネタは、あろはさんが最近The Coq Proof Assistant A Tutorial (3) Minimal Logicで (A->B->C)->(A->B)->A->C の証明をやっていたので、それを使わせてもらった。ついでに、A->B->Aも証明*1。Setと書いた部分はPropと書いたほうが論理っぽいんだけど、AgdaではPropはSetの別名に過ぎないし、Propを定義してるライブラリを読み込みたくなかったので、Setで通した。
それから、分かり易いように各種のコマンドは固有のキーバインディングは使わず、メニューとM-xから実行してみた。まあ、細かいことはともかく、これを見るとCoqをコマンドラインから使う場合に比べ、ゴールの管理が非常に直観的なことがわかると思う。もちろん、CoqでもCoqIDEやProof Generalを使えば同じくらい直観的に使えるんだと思うけど、試したことないんでよく知らない。誰かそれらを使った証明風景をキャプチャして紹介してくれると嬉しい。
【2024-09-01】 Flashはサポートが終了しているので、YouTubeにもアップロードしてみた。
他の証明環境の紹介動画
- Twelfでの証明行為 (hyさん)
- Coq-IDEでの証明行為 (hyさん)
- Coqでニコニコ :-] (yoshihiroさん)
*1 いわゆるSとKですな。
λ. 有限モノイドへの準同型写像への逆像としての正規言語の定式化
有限モノイドへの準同型写像への逆像 : 村田 真のチャンネル -北国tvからメモ。
正規言語の定式化の一つとして、有限モノイドへの準同型 写像への逆像を用いるものがあります。(中略) 文字列の集合Lが正規であるのは、適当な有限モノイドM、 準同型f, Mの部分集合Nがあって、L = {u | f(u) はNに属する } が成立するときです。
檜山正幸のキマイラ飼育記 - 長文の反応に驚き！でも書かれてるけど、非常にスマートな定義だと思った。
すばらしい。> Agda Flash
すばらしい。 JSON パーサはあると便利だなぁとは常々思っておりました。<br>3点ほど。<br>number の satisfy (`elem` ['1'..'9']) はふつう oneOf ['1'..'9'] ではないでしょうか。<br>同じく frac ですが、ここは digits だと「1.」みたいな数値も妥当とみなしてしまうので、 many1 digit ですね。<br><br>最後に、一般の JSON がどれくらい改行しているかはよく知らないのですが、 stringify では HughesPJ 等を使って適当に改行を入れた方が良いのかも、とちょっと思いました。
指摘ありがとうございます。<br>最初の二点は早速修正してみました。<br>最後のはHughesPJを使ったことがないので後で試してみます。
HughesPJ を使ってみましたが、ちょっと長いので<br>http://www.jmuk.org/d/?path=2006/04/27#d27t01<br>に書きました。参考になれば幸いです。
お、いい感じですね。<br>早速取り込んでみました。
はじめまして。<br>(実は、PPL Summer School 2004でお会いしてますが。)<br><br>Coq-ideを使った証明風景もキャプチャしてみました。<br>http://hy-orz.blogspot.com/2006/07/coq.html
ありがとうございます。早速リンクしました。<br>こうして比べてみるとなかなか面白いですね。<br><br>> (実は、PPL Summer School 2004でお会いしてますが。) <br><br>ごめんなさい。思い出せないです…… orz
私は受付をしていて、<br>さかいさんはヒビルテにコメントした方を探していました。<br><br>帰り際にちょっと話しただけなので、<br>覚えていなくて当然です ^^;
あ！ 思い出しました(^^;<br>あの時は探していたtradさんには結局会えませんでしたが、その節はどうも。<br><br># 今年の PPL Summer School はどうしようかなぁ……