Agda
先日MacBookAirにインストールしたAgda、とても快適に動くのだが、困ったことにtexモード（texコードを打ち込むとAquaemacs上でUnicodeの数学記号を出力する）の変換が出来ない。Ktさんに相談した結果、Texコードの変換機構は動いているが、emacsと日本語入…
以前、一度MacBookAirのAgdaをインストールしたのだが、間違えてインストールした際のユーザアカウントを消してしまい、新しいユーザアカウントで再インストールをしなければいけなくなった。この一週間というもの悪戦苦闘していたのだが、本日昼間にやっと…
Agdaでは、postulateで与えられた A : Set に対し、f : A -> Boolを定義した際、任意の t: A にたいし、 : Bool （ただし xがtに登場することを とここでは表記している）を定義することが出来ない。構成的型理論としては当たり前だけれど、やっぱり不便だ。
Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girard…
論文の続き。昼食は昼食は大学のカフェテリアで魚料理。食事中、D先生にMatin-Lofの '71年論文で循環性（）がその中核テーマだったので驚いた、と言った話をすると、テーブルの向こうにいたC先生がいきなり身を乗り出して来たので驚く。学者だ。C先生からHur…
英語の論文の続き。D先生からMartin-Lofの1971年論文のコピーをもらう。昼食は大学近くのレストラン、アラビアータ。なんとか食べれた。午後も続き、20時半まで。 何も食べずにホテルへ戻り、残っていた最後の風邪薬を飲み、そのまま寝る。
英語の論文の続き。外は明るいけれど気がついたら20時半。最後に残っていたNも帰るというので慌てて帰る。Jarntorgtの広場にあるパブで夕食。 テラスでビールを飲むにはいい気温。これで夜の21時半。熱気球も飛んでいる。 チェコビールとパスタ。
今後のAgdaの方針を決める討議、本日はUniverse Polymorphismに関して。 Agdaはご存知の通り、非常に厳格なpredicativityに基づいていますが、しかし厳格な可述性は、しばしばデータ型を定義する際の面倒の元になります。例えば record Cat: Set1 where Obj:…
開始は9時半から。 本日の講演は "A Tool for Automated Theorem Proving in Agda" (Fredrik Lindblad)のみ。定理の自動証明の効率化を図るツールをAgdaに実装する話。すみません、よく覚えていません、はい。
本日は班決め。私は、本日の発表について、英語の論文を書くことに。19時にみんなで退出、19時半から市中心部のレストランで夕食会。フランス料理、ビールと牛肉でお腹いっぱい。
"Using a logical theory of constructions for program verification" (Andreas Sicard)：コロンビアの大学の先生。講演のスライドはこちら、アブストラクトはこちら。 logical theory of constructions (LTC)上でgeneral recursive programs（停止しないプ…
バースと同じ内容を45分で発表。出来は、えーと、6回投げて8失点という感じ、散々でした。突っ込まれたポイントは 実装の対象となった様相論理の体系がなじみがなく、直感的な理解が難しい Agdaの停止判定機構に関する私の説明に、一部、Agda ver.1 そのまま…
開始は9時から。 "Formalization and test generation for a CPU architecture"：A君による発表。 "A Type of Partial Recursive Functions " (Ana Bove)：部分的帰納関数を型付けできるように、圏論を使って型を定義しようという話。面白かったです。対応す…
本日開幕。午前は講演。 開発者による新機能紹介（パターンマッチングをソフトウェアレベルで実現、これは "Agda in Agda" を目指す一歩と考えていいんだろうか？）、 "The power of Pi"（Wouter Swiersta)：依存型理論を売り込むためにはどうしたら良いか、…
その後は回復したA君と私が発表。45分のはずが30分になったので、大急ぎで終わらせる。和やかな雰囲気で終了。 驚いたのは、終わった後、わざわざG氏が握手に来たこと。お互い「出稼ぎ論理学者」なので、同種の臭いを嗅ぎ付けたんだろうか。
Agdaは現在開発真っ最中の言語で、昨日停止判定を合格しなかったプログラムが、今日の最新版では合格していたりすることが結構あります。例えば、ヒビルテさんのところの2006年3月25日*1に「アッカーマン関数の停止性を認識できない」と書かれていますが、現…
昨年11月の話の続報。 Agda2のdata typeの型の定義で、以下のようなデータ型 Predを定義しようとすると、「dataの型がSortではないのでParse エラーです」というエラーが出ると言う話を書いた。 Pred 0 = Set Pred n+1 = D ->Pred n ただし D: Set とする。 …
本日Ktさんから教えていただいた話、備忘のため。
本日Ktさんに聞いてわかったことを、備忘のためにメモ。Agda 2 でデータ型からデータ型 への関数を定義するとき、変数の束縛に関して、思いもよらないことがおこる（昨日はバグはこのせい）。 Aのデータ型は A : Nat -> A g : (n : Nat) -> ... の形をしてお…
これまで誤解していたが、Agda2のdata typeの型の定義で、 (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、 (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ ということ…
現在、Agda2で某論理体系を実装中、本日からタイプチェックを始めた。論理体系なので、列計算を定義したいと考えるのは自然な考えでしょう。というわけで、命題の列を定義しようとしたのだが・・・ Agdaのベースとなる直観主義的タイプ理論では、Proposition…
実は Agda の上で impredicative な議論が強力に展開できるということ、そして証明論的にはアホみたいに強いということ。驚きました。
全く意味はないんですが。出力データーが出てきて、妙にうれしかったので。2^{2^3}のはずです。
