2005-09-01 [長年日記]
λ. 衆院選
すっかり忘れてたけど、そういやもうすぐ選挙だな。正直なところ小泉政権には不満も多いけど、消去法で選ぶと自民党しか残らない予感。
λ. A simple equational calculator
たまたま見つけて遊び中。
コメントに「Any variables mentioned in a replacement must have been mentioned in a pattern already matched. So for a law "p = r <= r1 = p1 & ... & rn = pn" Any variable in ri must be mentioned somewhere in p, p1, ... pi-1. Any variable in r must be mentioned somewhere in p, p1, ... pn.」と書いてあるんだけど、この条件が良く分からなかった。
あと、本当に簡単な等式しか証明できないみたいで残念。例えば以下のような規則から「pair f g . h = pair (f . h) (g . h)」という等式を証明することすら出来ないみたい。
pair/pi1: pi1 . pair f g = f pair/pi2: pi2 . pair f g = g univ: h = pair f g <= pi1 . h = f & pi2 . h = g
![[眉間に風穴の開いたモリゾー]](./images/20050902_0.jpg)
2005-09-05 [長年日記]
λ. 記憶（memo）する関数
「同じ変数に束縛されたものは二度計算されることはない」という性質を利用したメモ化で、同じ問題を書いてみる。memocc2.hs
2005-09-06 [長年日記]
λ. 『田中雄二の漢文早覚え速答法』＆『田村の現代文年間カリキュラム』
知人が受験生にこの二冊を紹介していた。いい本らしい。現代文はともかく、私は高校時代に古典と漢文が死ぬほど苦手だったんだが、こういう本を読んでいたらひょっとしたら違っただろうか?
2005-09-11 [長年日記]
λ. 風邪
風邪ひいたっぽい。喉が痛い。
λ. 衆院選
投票に行ってきた。
小泉政権の経済政策には不満が多かったし、郵政民営化も別に積極的に賛成しているわけではないのだけど、他の政党もその点では五十歩百歩だから比べられないし、他の政党は安全保障等の点で不安だったので、結局消去法で自民へ。もし、民主党にそういった不安点がなくて、かつリフレ政策でも公約にしてれば、民主党に投票することも真剣に検討したんだけどね……
最高裁判所裁判官国民審査は、今回の六人は特に×印を付けるべき理由も見当たらなかったので、そのまま投票。
それにしても、自民党ﾃﾗﾂﾖｽw 自民党単独で290議席以上って、おい…… それはそれで何か不安だ。
λ. LDAPのuserPassword
間違えてuserPasswordを空にしてしまったら、変更しようとしても「ldap_bind: Server is unwilling to perform (53)」「additional info: unauthenticated bind (DN with no password) disallowed」と言われるようになってしまって困った。結局adminになって設定しなおした。
2005-09-13 [長年日記]
λ. Windows用バイナリ
を作ったので適当に放置しておく。現在のCVSのソースからビルドしたものは振る舞いが変だったので、5月の時点のソースからビルドした。これらのファイルとemacsさえあれば最低限のことは出来る。あとライブラリは適当にCVSからとってくるべし。
2005-09-15 [長年日記]
λ. Propositional equality の証明の equality
Propositional equality の型である Id a b の要素はせいぜい一つしかないので、要素が二つ与えられたらそれらは等しいに決まっている。それを証明したい。が、以下のコードは内側のcaseの部分で「Error in the definition of eqId because: cannot case: exps [x, x] must be distinct variables.」というエラーになってしまう。(e1へのcaseでa,b,xがunifyされているためこのようなエラーメッセージになってる。2005-05-16 の case on non-var でも書いたが、この制約は必要以上に厳しい気がする)
eqId (|A::Set) (|a,|b :: A) (e1,e2 :: Id a b)
:: Id e1 e2
= case e1 of
(ref x)->
case e2 of
(ref y)->
ref@_ (ref@_ x)
Agdaでこの命題を証明する方法はあるだろうか? SET.alfa では Id a b の Collapsed も定義されてないし、やっぱり無理なのか? Per Martin-Löfの Intuitionistic Type Theory でもこれは証明できるので、「Martin-Löf. の型理論に基づく対話型定理証明支援系」と呼ばれているAgdaでこれが証明できないとしたら、納得いかん。
(2005-09-17 追記) Intuitionistic Type Theory は propositional equality type の strong elimination を含む extensional な型理論だから、「Agdaでも証明できるべき」という理由にはならない気がしてきた。というか、私はその辺りの話が全然分かってない。Intuitionistic Type Theory 以降の Martin-Löf 流の型理論を学ぶには何を読めば良いのだろう? Bengt Nordström, Kent Petersson, Jan M. Smith の Programming in Martin-Löf's Type Theory - An Introduction ?
(2006-02-05 追記) Thierry Coquand の Pattern matching with dependent types の p.9 には次のように書いてあった。
By contrast, it is not clear how to represent the following computation rule in term of the usual elimination rules4. We have seen that the unique contextual mapping
{y := x, p := refl(N,x), q := refl(N,x)}: (x : N) → Δ,
is a covering of Δ = x,y : N; p,q : Id(N, x, y). It follows that it is correct to add a new constant f : (x,y : N; p,q : Id(N,x,y))Id(Id(N,x,y),p,q) together with the computation rule
f(x, x, refl(N,x), refl(N,x)) = refl(Id(N,x,x), refl(N,x)) (x : N).
4 This problem has been independently suggested by Thomas Streicher.
(2006-04-18 追記) Michael Hedberg の A coherence theorem for Martin-Löf's type theory には次のように書かれていた。というわけで、elimIdではいくら頑張っても証明できないことになります。証明するにはAgdaに対して何らかの拡張が必要になるでしょう。
Although one might expect the identity sets to be collapse, it is impossible to prove in general that they are, as long as type theory is restricted to the standard elimination rules. This negative result is proved by Hofmann and Streicher [11], using a groupoid interpretation of type theory.
[11] M. Hofmann and T. Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.
(2006-05-14追記) この「A groupoid model refutes uniqueness of identity proofs」を読んだ。20060514#p01を参照。
2005-09-17 [長年日記]
λ. 型理論での形式的証明記述の技法について; 木下 佳樹, 高村博紀
メモ。Chainがちょっと面白かった。
(追記)「系統的な等号の与えかたで, すべての点で満足できるものはない」とあるが、Extensional Equality in Intensional Type Theory の型システムを直接実装したものはどうなんだろう。結構良い線をいっているのではないかと思うが。
(追記) 「Calculational Proof っぽい書き方」も参照。
(2008-02-04追記) どうでも良い点だけど、Leibniz equality との比較で「Id では, 等号の階層が上がってしまう, という問題は生じないが, 今度は, 外延性の問題が生じる.」とあるが、Leibniz equality でも外延性の問題は生じる。
2005-09-22 [長年日記]
λ. 型代入を遅延する最適化型推論アルゴリズム; 上野雄大, 大堀淳
LLDN 公園の部で教えたもらったときには気づかなかったけど、型代入の環境への適用を遅延するというアイディア自体は別に新しいものではないはず。例えば Mark P. Jones の Typing Haskell in Haskell で示されているアルゴリズムもそのようになっている。この辺りの話はよく知らないのでなんとも言えないけど、少なくとも folklore ではあったと思う。
もっとも、Typing Haskell in Haskell のコードは、ユニフィケーションの方はそのようになっていないけど。
2005-09-23 [長年日記]
λ. Agdaプラグイン機構; 池上 大介
を読んだ。使う側のインターフェースはシンプルでいい感じ。external予約語で書かれた項は、型チェック時に外部ツールが呼ばれる以外はabstractが指定された項と同じ扱いなのかな。それと、FOLプラグインの使用例を見ると、外部ツールには型情報も渡しているのかな。
2005-09-24 [長年日記]
λ. An Implementation of a setoid model in Agda
Extensional Equality in Intensional Type Theory の setoid model を、LEGOでの実装を元にAgdaで実装中。大体実装できた。
(2005-09-30 追記) だいぶ苦戦してしまったが、基本的な部分を何とか書けた。色々汚いので、きれいに書き直したいな。それと、LEGOでの実装と比較しなくては。
- Meta.agda
- Approximative Implementation of the meta theory.
- Setoid.agda
- Definition of the core model.
- Compr.agda
- Definition of context comprehension.
- Pi.agda
- Definition of ∏-types.
- Prod.agda
- Definition of (non-dependent) product types.
- Id.agda
- Definition of Identity types.
λ. 旅行
![[黒鳥]](./images/20050924_0.jpg)
![[光圀像]](./images/20050924_1.jpg)
![[葡萄狩り]](./images/20050924_2.jpg)
![[梨狩り]](./images/20050924_3.jpg)
2005-09-28 [長年日記]
λ. signature の equality に???
β変換すれば同じになるはずの(signatureで定義された)型が同一と見なされなくて、困ってしまった。例えば以下のコードのtestの定義では、「fm A (f x)」と「fm (Ty_m f A) x」はβ変換すれば同じシグネチャになるので、一見して型チェックは通りそうに見える。だが、実際には「t has type fm A (f x) but should have type that is equal to fm (Ty_m f A) x」と型エラーになってしまう。
Ty_o (X::Set) :: Type
= X -> Set
Ty_m (|X,|Y::Set) (f::X->Y) (A::Ty_o Y) :: Ty_o X
= \(x::X) -> A (f x)
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
= sig
c :: A x
test (|X,|Y::Set) (|A::Ty_o Y) (f::X->Y) (x::X)
(t::fm A (f x))
:: fm (Ty_m f A) x
= t
半日ほど悩んだ結果、この型エラーはfmの定義を以下のように書き換えれば回避出来ることに気づいた。しかし、このように書き換えなくてはならないのは直観的でないし、それに参照透明でもないように思う。何故このようになっているのだろうか?
fm' (Ax::Set) :: Set
= sig
c :: Ax
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
= fm' (A x)
【2006-05-03追記】 「薔薇色の明日」の「Agdaの型チェック通らず」というエントリで書かれていた以下の話(パーマリンクが機能していないようなので勝手に引用)は、ひょっとして同じことで悩んでいるんじゃないかという気がする。
Agdaでちくちくと証明を実装していたのだが、エラーメッセージによると型が合っていない。しかし、私の記述は、システムが「この型であるべきですよー」という型の略記でしかないので、普通は同じ型とみなしてくれてもよさそうである。
仕方がないから先生にお尋ねしたところ、「ここを変えてみたら？」という助言のままに書き換えたところ、エラーメッセージが変わった。「ここは型Aと記述されてますけど、型Aになるように記述しないと駄目ですよー」と。
2005-09-29 [長年日記]
λ. Freek Wiedijk. Comparing mathematical provers
を読んだ。各種のシステムの大雑把な比較。個々のシステムの詳細について触れられていないのは残念だけど、A rather subjective two-dimensional diagram は分かりやすかった。
![[A rather subjective two-dimensional diagram]](./images/20050929_2.png)
λ. 「時間を無作為にすごす」 by addie
今日の迷言。
![[2ゲーム目終了時の盤面]](./images/20050929_0.jpeg)
![[研究会の様子]](./images/20050929_1.jpeg)
2005-09-30 [長年日記]
λ. 2005年4月25日 福知山線5418M、一両目の「真実」
N.* D.* E.* (2005-09-29) より。実体験というのは凄いものだと感じた。圧倒される。
λ. 『四季 夏』, 森 博嗣
を読んだ。『四季 春』から(Fで言及されていた)両親の殺害にどのようにして至るのか。そこにギャップを感じていたので、その部分がどう表現されるのか非常に気になっていたが、きちんと描かれていて満足。あと、「そんな理屈が通るか?」「理屈は常に通ります」というやり取りに吹き出してしまった。緊迫したシーンなのに……
λ. 靖国参拝訴訟：小泉首相の参拝、違憲 職務行為と認定−−大阪高裁判決
またしょーもない判決を……
ψ yaizawa [新党大地は・・・? (違]
ψ さかい [だって、たしか私の選挙区に新党大地の候補者いなかったし(笑]
ψ yaizawa [> たしか私の選挙区に新党大地の候補者いなかったし 北海道民じゃないとバレちゃう気が・・・．]
ψ さかい [バレると何か問題があるんだろうか…… ってか、そんなyaizawaさんの選挙区には新党大地の候補者が(ry]
ψ yuragi [実家にいるとき、新党ムネオの演説が煩かったですよー。 前回の選挙で割と票が伸びてたから、意外と侮れなかったりします。..]
ψ yaizawa [ヒーローの私生活は謎に満ちているんですよ．(w うちの選挙区は南関東ブロックです (かなり普通な答え)．]
ψ さかい [> yuragiさん 今朝の毎日新聞にも「大地は自民支持層の一部と無党派層に浸透し、一議席に届く勢い」とか書いてあり..]