トップ «前の日(11-12) 最新 次の日(11-14)» 追記

日々の流転


2001-11-13

λ. データベース概論の課題にとっても苦労。

λ. 朝鮮語

JSA見ました。

ゆーけんが***で**されているらしい。有名人は大変だねぇ。


2002-11-13

λ. 講演「通貨危機とIMFの役割」 (by 伊藤隆敏)

すっかり寝過ごしてしまった。自己嫌悪。


2004-11-13

λ. AVL木でGADTを試してみる

Programming in HaskellProgramming:玉手箱:その他花谷さんが書いていたAVL木のコードをたまたま見て、GADT を試すいい機会と思い、GADT で「左右の木の高さの差が高々1以下」という制約を表現するように書きかえてみた。AVL.hs

花谷さんのコードではbalance関数を挿入用と削除用で共有するようになったが、このコードだと(処理は同じなのに)型が違うために共有出来ていない。型をうまく定義すれば共有できる?

AVL木でGADTを試してみる(2) に続く...

Tags: haskell

2006-11-13

λ. FreeMind

MindMapは存在は知っていたが、これまで試したことはなかった。 しかし、先週の「伊藤洋一のRound Up World Now!」でFreeMindというツールが紹介されていたので、いい機会と思って試してみることにする。

参考:

本日のツッコミ(全2件) [ツッコミを入れる]

ψ takot [「伊藤洋一のビジネストレンド」のPodcastのほうは, もう1年以上聞いてます.こっちと何が違うのかな.]

ψ さかい [僕も「伊藤洋一のビジネストレンド」を一年くらい聴いてたのですが、最近こっちも聴くようになりました。 「伊藤洋一のビジ..]


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 ではこんなにシステマティックにやってはいないけど。

Tags: 論文 圏論

*1 終対象ではないので注意。