2004-11-13
λ. AVL木でGADTを試してみる
Programming in Haskell の Programming:玉手箱:その他 で花谷さんが書いていたAVL木のコードをたまたま見て、GADT を試すいい機会と思い、GADT で「左右の木の高さの差が高々1以下」という制約を表現するように書きかえてみた。AVL.hs
花谷さんのコードではbalance関数を挿入用と削除用で共有するようになったが、このコードだと(処理は同じなのに)型が違うために共有出来ていない。型をうまく定義すれば共有できる?
AVL木でGADTを試してみる(2) に続く...
2006-11-13
λ. FreeMind
MindMapは存在は知っていたが、これまで試したことはなかった。 しかし、先週の「伊藤洋一のRound Up World Now!」でFreeMindというツールが紹介されていたので、いい機会と思って試してみることにする。
参考:
2008-11-13
λ. “Functorial Semantics of Algebraic Theories” by F. William Lawvere
ちょっと前に読んだ論文。 代数セオリーやそのモデルの形式化を最初に見たときは「へぇー」と思った。 言われてみれば当たり前なんだけどね。 どう形式化するかというと、代数セオリーを自然数を対象とし対象nが対象1*1のn個の直積となっている小さな圏Aとして定義する。 例えば群であれば、この条件と以下から自由生成される圏がセオリーになる。
- e : 0→1
- inv : 1→1
- μ : 2→1
- μ∘〈e, id〉 = id
- μ∘〈inv, id〉 = id
- μ∘〈μ, id〉 = μ∘〈id, μ〉
同様に束を考えると、前述の条件と以下から自由生成される圏がセオリーになる。
- ∨, ∧ : 2→1
- true, false : 0→1
- ∧∘〈π2, π1〉 = ∧
- ∨∘〈π2, π1〉 = ∨
- ∧∘〈∧, id〉 = ∧∘〈id, ∧〉
- ∨∘〈∨, id〉 = ∨∘〈id, ∨〉
- ∧∘〈id, true∘!〉 = id
- ∨∘〈id, false∘!〉 = id
- ∧∘〈id, id〉 = id
- ∨∘〈id, id〉 = id
- ∧∘〈π1, ∨〉 = π1
- ∨∘〈π1, ∧〉 = π1
そして、セオリー間の射を対象を保存する関手とし、これらのなす圏をJとする。 セオリーAのモデルとなる代数はAからSetへの直積を保存する関手と考えられるし、準同型は関手の間の自然変換と考えられるので、A代数の圏は一種の関手圏。Jの射 f : A→B に対して関手 Setf : SetB→SetA はB代数の圏からA代数の圏への忘却関手になり、この関手の左随伴が存在する。
さらに、ある圏があるセオリーの代数の圏になっているための条件、などなど。
【2008-11-19追記】 ところで、どっかで見たような話だなぁと思ったら、Conceptual Mathematics: A First Introduction to Categories(F. William Lawvere/Stephen Hoel Schanuel) の ARTICLE III: Examples of categories の 11. Types of structure あたりでこういう話は散々やったのだった。 もちろん、Conceptual Mathematics ではこんなにシステマティックにやってはいないけど。
*1 終対象ではないので注意。
