2001-09-28
λ. ふと、計量経済モデルの分野におけるオープンソースってどうなんだろとか思った。ちょっと探してみたけど、見当たらないなぁ。
λ. 朝鮮語
入門講座でやった内容を夏休みの間にほとんど忘れてて焦る。それと、Emacsでハングルを入力するの面倒。はやくキーマップになれなくちゃ。trrみたいなタイプレッスンソフトってどっかにない?
試しに自分の名前を打ってみる。 사카이 마사히로
λ. 読んだコミックス
- 『サイレント・メビウス SIDE7』
- 『サイレント・メビウス SIDE8』
- 麻宮騎亜
- 『エクセル・サーガ 8』
- 六道神士
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になるように記述しないと駄目ですよー」と。
2006-09-28
λ. 生協でバスカードを買う
残念。生協ではバスカードはEdyで買うことが出来ない。 Edyに少しチャージしすぎてしまったのでEdyを消費したかったのだけど、Edyが使えないのならいつものように金券ショップで買っていれば良かった。しょぼーん。
2008-09-28
λ. A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments
A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments by Joseph A. Goguen and R. M. Burstall
To ease constructing institutions, and to clarify various notions, this paper introduces two further concepts. A charter consists of an adjunction, a “base” functor, and a “ground” object; we show that “chartering” is a convenient way to “found” institutions. Parchments provide a notion of sentential syntax, and a simple way to “write” charters and thus get institutions. Parchments capture the insight that the syntax of logic is an initial algebra. Everything is illustrated with the many-sorted equational institution. Parchments also explicate the sense of finitude that is appropriate for specifications. Finally, we introduce generalized institutions, which generalize both institutions and Mayoh's “galleries”, and we introduce corresponding generalized charters and parchments.
昔、向井先生にハードコピーを貰ったまま積読になっていた論文。 institutionの幾つかの定義と、典型的な場合についてinstitutionを作るためのcharterとparchmentという枠組みについての紹介。
institutionの定義に関しては通常の定義に加えて、以下の三つ組みによる定義があって、これ何で自分でこれ気づけなかったのかと思った。そして、この定義から一般化することで generalized institution が得られる。
- 関手 Mod : Signop → Cat
- 関手 Sen : Sign → Cat
- 対角自然変換 ⊧ : |Mod(_)|×Sen(_) → 2
charter は随伴から insitution を定義するためのもので、図で書くとこんな感じのもの。
![\xymatrix{ \mathrm{Sign} \ar@<1ex>@/^1pc/[r]^{F} \ar@{}[r]|{\bot} & \ar@<1ex>@/^1pc/[l]^{U} \mathrm{Syn} \ar[r]^-{B} & \mathrm{Set} \\ & G \ar@{|->}[r]^-{B} & \{\mathrm{true}, \mathrm{false}\} }](tex/34c003d1e64e2b805f0cbea7bc3c5055.png "\xymatrix{ \mathrm{Sign} \ar@<1ex>@/^1pc/[r]^{F} \ar@{}[r]|{\bot} & \ar@<1ex>@/^1pc/[l]^{U} \mathrm{Syn} \ar[r]^-{B} & \mathrm{Set} \\ & G \ar@{|->}[r]^-{B} & \{\mathrm{true}, \mathrm{false}\} }")
ここで Syn は syntactic system で、「文」だけでなく他の構文的な要素も含むような圏で、Bはそのなかから「文」の成分だけを取り出してくるような関手。こうしておいて Sen を BF で定義する。G は syntactic system の全ての解釈を集めてきたようなもの。 ただ、equational charter での G の定義はサイズの問題が無いのかちょっと不安。
parchment は、自由代数を使うことにして随伴になることを自動的に保障するもの。 関手 Lang : Sign → SigAlg を用意しておいて、Syn は Lang(Σ)代数の圏をΣに関してつぶして作る。
あと、個人的には「The original motivation for developing institutions was to do the “Clear tricks” once and for all, over any (suitable) logical system」と書いてあって、institutionのそもそもの動機が分かってスッキリした。ここで言っている“Clear tricks”というのは代数的仕様記述言語Clearで使われている以下のような手法のこと。
- use colimits to put theories together
- use diagrams as environments to keep track of shared subtheories
- use data constraints to define particular structures (i.e., abstract data types)
- use pushouts to apply generic theories to their “actual” arguments, and
- use theory morphisms to describe the bindings of actuals at interface theories (also called “requirement” theories).
![[ケーシーズキッチンのカレー]](./images/20090928_0.jpg)
