2003-04-04
λ. 新学期
色々と憂鬱。
λ. 入手した本
メディアセンターで処分される本を何冊かゲット。
- The Semantics of Destructive Lisp
- Ian A. Mason
- A Programming Approach to Computability
- A. J. Kfoury, Robert N. Moll, Michael A. Arbib
- Logical Foundations of Functional Programmming
- Gerard Huet
- The Mathematics of Inheritance Systems
- David S. Touretzky
- Equational Logic as a Programming Language
- Michael J. O'Donnell
- DATA COMPRESSION Techniques and Applications
- Thomas J. Lynch
2004-04-04
λ. gtk2hs-0.9.4 (その2)
数日間使ってみた感想。
他の言語でgtk2を使ったことがあればあまり戸惑わずに使える。けど、中途半端にインターフェースを変更している箇所もあるので注意。たとえば boxPackStart :: (BoxClass b, WidgetClass w) => b -> w -> Packing -> Int -> IO () はgtk_box_pack_start(GtkBox *box, GtkWidget *child, gboolean expand, gboolean fill, guint padding) のexpandとfillの二つの引数をPackingという型の単一の引数にまとめてしまってる。
実装を見ると、c2hsを使ってFFI周りのコードをCのヘッダファイルから自動生成した上で、その上にHaskellっぽいインターフェースを被せてる。これでだいぶ省力化出来てるのは素晴らしい。
ただ、シグナル周りとかの設計は少々ダサい気がする。実装にはg_signal_connect_data()を使うよりもGClosureの仕組みを活用した方が良いんじゃないかというのもあるが、それよりもまずシグナルごとに onClicked, afterClicked :: ButtonClass b => b -> IO () -> IO (ConnectIdo b) みたいな関数があるのってどうなのよ?
僕だったら、例えば以下のようなインターフェースにしたと思う。こういう設計にしなかったのには何か理由があるのだろうか。
signalConnect, signalConnectAfter :: obj -> (Signal obj t) -> t -> IO (ConnectId obj)
signalEmit :: obj -> (Signal obj t) -> t
signalName :: Signal obj t -> String
...
clicked :: (ButtonClass b) => Signal b (IO ())
2007-04-04
λ. Scott open filters & Compactness
通勤時間等に位相のお勉強。 4年前くらい前、Scott open filters とコンパクト性が理解できなくて悔しかったのだが、今同じところを見直したら簡単で普通に理解できた。 locale D で ΩD の scott open filters と D の compact saturated sets が対応するという Hofmann–Mislove (Scott Open Filter) Theorem も理解できた。
ψ 竹内 [竹内です。どうもご無沙汰しました。 遅れましたが、修士終了おめでとう。 いよいよ社会人っすね。 酒井君は有能なやり手..]
ψ 竹内 [時間がたってからもう一度勉強すると、 すんなり分かることってあるよね。 結局その繰り返しなんだろうなあ。 勉強続けて..]
ψ さかい [ありがとうございます。 やり手社員になれるかはどうかは分かりませんが、研修の結果、技術だけじゃなくマネージメントも面..]
ψ タナカコウイチロウ [＞マネージメントも面白そうだと思うようになりました ときどき出てくる、本の紹介するオジサンです。 チームワークに興..]
ψ たけを [うーん、個人的には酒井さんには技術を極めてほしいですけどね。 でも興味を持つことはいい事だし、最終的には本人の判断だ..]
ψ さかい [考えを整理したら、マネジメントというか「戦略的に問題解決を行うプロセス」とその手法に興味を持ったのかも。 学生時代..]
2008-04-04
λ. topos の internal language は?
ふと思ったので、調べもせずに書く。
- CCCの internal language は単純型付ラムダ計算
- LCCCの internal language は ∑ と ∏ による依存型を持つ型理論
では topos の internal language は何だろうか?
基本的には、∑ と ∏ による依存型を持つ型理論に対して、subobject classifier に関する項と規則を追加すればよいのだとは思うが、もしmonomorphismの判定(judgement)を入れるとすると、結構大きな拡張になるような気がする。 どう形式化するものなんだろうか……
【2008-04-20追記】 トポス (数学) - Wikipedia に「Kripke-Joyalの意味論とよばれる手続きによって集合論的論理式をトポスの対象と射についての言明として解釈することができる」とあった。 Kripke-Joyalの意味論については知らないのだけど、この意味論はトポスに対して完全なのだろうか?
2013-04-04
λ. ゴモリーの小数カットの導出メモ
Outline of an algorithm for integer solutions to linear programs でのゴモリーカット(Gomory's fractional cut)が、割と天下りに定義して、そのあと必要な性質を満たすことを証明しているけれど、これがちょっと気に入らなかったので、演繹的に導出してみた。(An algorithm for the mixed integer problem のゴモリーの混合整数カットの方ではないので注意)
準備
N を(0を含む)自然数の集合とし、(R, ≤R), (Z, ≤Z) をそれぞれ実数と整数の順序集合とする。 また、 I : (Z, ≤Z) → (R, ≤R) を順序集合間の通常の埋め込みとするが、たいてい省略する。
⌈-⌉, ⌊-⌋ : (R, ≤R) → (Z, ≤Z) をそれぞれ正の無限大方向への切り上げ(ceiling)と負の無限大方向への切り捨て(floor)とする。
随伴、モナド、コモナド、双対性
⌈-⌉ と ⌊-⌋ はそれぞれ I の左随伴と右随伴になっている。すなわち、以下が成り立つ。
- ∀a∈R, b∈Z. ⌈a⌉ ≤Z b ⇔ a ≤R I(b)
- ∀a∈Z, b∈R. I(a) ≤R b ⇔ a ≤Z ⌊b⌋
したがって、 I∘⌈-⌉, I∘⌊-⌋ : (R, ≤R) → (R, ≤R) はそれぞれ (R, ≤R) 上のモナド、コモナドとなっており、以下が成り立つ。
- ⌊a⌋ ≤ a ≤ ⌈a⌉
- ⌊⌊a⌋⌋ = ⌊a⌋
- ⌈a⌉ = ⌈⌈a⌉⌉
また、 ⌈-⌉∘I, ⌊-⌋∘I : (Z, ≤Z) → (Z, ≤Z) はそれぞれ (Z, ≤Z) 上のコモナド、モナドとなっており、こっちは更に強く、以下が成り立っている。
- ⌈I(a)⌉ = a for all a∈Z
- a = ⌊I(a)⌋ for all a∈Z
また、(-1)×- : (R, ≤R) → (R,≥R) によって、⌈-⌉と⌊-⌋は双対になっており、 ⌈a⌉ = - ⌊- a⌋ が成り立つ。
⌈-⌉ と ⌊-⌋ の分配性
a≤⌈a⌉ および b≤⌈b⌉ より a+b ≤R ⌈a⌉+⌈b⌉ = I(⌈a⌉+⌈b⌉) で、随伴性より ⌈a+b⌉ ≤Z ⌈a⌉+⌈b⌉ 。 双対性より ⌊a+b⌋ ≥Z ⌊a⌋+⌊b⌋ 。
さらに、帰納法により ∀n∈N. ⌈n×a⌉ ≤Z n×⌈a⌉ もいえる。 同じく、双対性より ∀n∈N. ⌊n×a⌋ ≥Z n× ⌊a⌋
ゴモリーの小数カットの導出
xi, y ∈ N が
- Σi ai xi + y = b …… (1)
を満たすとする。すると、
- Σi ai xi + y ≥ b … (2)
- Σi ai xi + y ≤ b … (3)
(3)の両辺に⌊-⌋を適用すると、⌊-⌋ の単調性より
- ⌊Σi ai xi + y⌋ ≤ ⌊b⌋ … (4)
⌊-⌋ の分配性と ⌊y⌋=y より
- ⌊Σi ai xi + y⌋ ≥ Σi ⌊ai xi⌋ + ⌊y⌋ ≥ Σi ⌊ai⌋ xi + ⌊y⌋ = Σi ⌊ai⌋ xi + y … (5)
(4), (5)に推移律を適用して
- Σi ⌊ai⌋ xi + y ≤ ⌊b⌋ … (6)
両辺に -1 をかけて
- Σi (- ⌊ai⌋) xi - y ≥ -⌊b⌋ … (7)
(2) と (7) の両辺を足し合わせて、
- Σi (ai - ⌊ai⌋) xi ≥ b - ⌊b⌋
■
