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) | 雑多

2013年11月19日

そしてまたSML#

もうあきらめたって良いと思うんだが。
SML#のビルドを試してみた。1.2.0。
どうでもいいつまらないことで詰まったのでメモ。

今度はpaxかcpioがないとダメだと言われた。
多分前も言われた。
mingw-getで入るのはbsdcpio.exeとかで、コピーして使った。
なんかしらんがlibz-1.dllがないとか言われたのでlibz1.dllの名前を書き換えてWindowsフォルダにたたき込んだ。
いろいろダメな気がする。

・・・あれ、でも割とすんなり終わった。時間はかかったけど。
posted by chiguri at 02:12| Comment(0) | PC

2013年11月05日

Windows用Agdaのインストーラで詰まったこと

講義で一斉にインストールを試したのだが、一応注意とメモとして。
10人ちょっとだが、ネットワークが死ぬのが怖いので、極力インストーラがネットワークを見に行かないようにインストーラを改変(注:この決断が正しかったことを後に知る)。
起こったエラーは次の二つ。

1)インストール時、関連するパスに日本語があるとエラーを起こす。
2)F-SecureのDeepGuardがcabalでインストールしたcpphsやなんだったか忘れたがHaskell用のmakeっぽいプログラムをトロイの木馬として認識する。

1は一応Known issueだったらしいことを後に知った。
なお、インストールパスのみならず、tempフォルダが配置されるユーザ名が日本語でもアウト。
(cabalでのAgdaインストール時に文句を言う)
もちろん後でユーザ名を変えてもユーザディレクトリ(C:\Users\ほげ の「ほげ」の部分)が日本語である限りアウトなのを付記しておく。
こんなの講義中にやられたら死ぬわ。
(ちなみに講義では新しくアカウントを作らせた)

2は困った。
幸い、cpphsの方は尋ねるだけなので、その時点で許可を出しつつF-Secureの設定から一時的にDeepGuardを停止することで回避。
Agda自体にはこれらの実行ファイルは必要ないので、後に引っかかっても特に問題なし。

こんなの一度も出たことないんだけどなあ・・・
もう21世紀も13年目なのに、また日本語ユーザ名に苦しむとか勘弁してほしい。
というかこの学科そんなアカウント作らせるの勘弁して。
いやまじめに。


ちなみにネットワークについて。
割り当ての教室に学内ネットワークが届かないという抱腹絶倒な環境だった。
cabalだけじゃなかったらどんなネットワーク環境作っても死にましたって。
(基本的にネットワークを見に行かないのだが、cabal updateだけは避けられなかったため、インストール時にネットワーク必須)
posted by chiguri at 18:39| Comment(0) | Agda

2013年10月31日

進捗Advent Calendarの進捗報告

これは進捗Advent Calendarの内容例として書いた、第-31日目です。
もし進捗をどう書いて良いか分からない場合、参考にしてみてください。

・進捗Advent Calendar
 ・10/30:進捗AdventCalendar募集開始(URL
 ・10/30夜:想定最低人員10人を超えたので決行を決定、それに伴い一部情報を更新
 ・10/31朝:記事が必要な日数24に対して半分超え
 ・10/31昼:本記事を例として記述
 ...
 ・12/1:決行予定
 ・12/25 午前0時:終了予定
・艦これ
 ・10/28:陸奥さん飛龍さんGet
 ・10/31:阿武隈さんGet
 ・11/1:艦これのイベント開始予定(重要!)

以上が進捗になります。
さて、初日はどなたでしょうね。
初日の担当者の方、進捗どうですか?
posted by chiguri at 13:27| Comment(0) | 雑多