トップ «前の日(08-01) 最新 次の日(08-03)» 追記

日々の流転


2001-08-02

λ. 借りた本

Tags:

λ. Ruby Relaxer

う〜ん。感想っすか。PrologでDCGを使って書いたパーサのバグとるのに苦労したし、しばらくはXMLは勘弁って感じ。というかRelaxerって何?って状態なんで、そんな事訊かれても…

Tags: ruby

λ. Script-Fu

Script-Fuのinterp_slib.cにaproposという関数を見付けたので、コンソールで(apropos)とかしてみたら固まったし。

Tags: gimp

2002-08-02

λ. 最終発表

あらら……

発表向きのネタではないとは分かっていたのだけど、CPLの方は実装が間に合わなかったのだもの。しょうがないよね。……と思ったが、やっぱ成果物を作れなかったなりに、圏論ついて発表しておけば良かったなぁ。

まあ、これで明日から、真・夏休みって感じ。

λ. Ruby-GNOME2

えっと、GCとリファレンスカウンタの扱いで、またヤバイ点に気が付きました。とりあえず、見なかった事にしよう。

Tags: ruby

λ. さあ

寝よう

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

ψ むとぽん [え?(^^;)]

ψ さかい [例えば以下のスクリプト。 新しく作られたGtk::TextBufferは解放されるでしょうか? def my_te..]

ψ むとぽん [うーむ...。]


2003-08-02

λ. 某所で夏祭り

落ち込んでたけど、自分が今悩んでることが、どうでもよい小事に思えてきた。もうやりたいようにやろう。立ちふさがるものは全部なぎ倒して踏み潰せばいいし。


2004-08-02

λ. "擬データを用いた対話的関数プログラミングに関する研究", 石井裕一郎

を読んだ。単一代入や変数による通信は論理型言語みたいで面白いなぁ。私は関数論理型言語については全然知らないのだけど、ひょっとしたら関数論理型言語と相性のよいフレームワークなのではないだろうか。あと、関数型言語の視点でみると、参照透明性こそ保たれているものの、定義があまりにも操作的なので、もう少しなんとかならないかなぁとも思った。

[2005-07-28 追記] Haskellでcomonadベースの似たような枠組みを書いてみて気づいたのだけど、「4.2.5 競争的書き込み」のmergeRは有限のリストに対しては正しく動作しないはず。なぜならば、writeはnilに出会ったときに擬データをnilに確定しないため、mergeRの結果のリストの終端はいつまでたっても確定しない。

Tags: 論文

λ. 飲み会@串屋

.


2006-08-02

λ. Persistent Data Structures

MIT の Advanced Algorithms, Fall 2005 の第二回の資料 Persistent Data Structures を読んだ。

変更を行うとそれ以前のデータにアクセス出来なくなる ephemeral なデータ構造に対して、変更を行う以前のデータに自由にアクセス出来るデータ構造が persistent なデータ構造。過去のデータを自由に読むことは出来るけど、変更は最新のデータにしか出来ないのは partialy persistent なデータ構造。

ポインタを使ったデータ構造をpersistentにするための一般的な手法として fat nodes と path copying があるが、どちらも追加的コストが比較的大きい。それに対して、Sleator と Tarjan の modification box を使う手法は両者の優れた点を組み合わせた手法で、O(1) の追加的コストでいけるそうだ。

λ. 靖国神社:元軍人らの遺族、合祀取り消し求め初提訴へ

またしょーもない訴訟を……というのが正直な印象。この手の話は自衛官合祀訴訟の最高裁判決で一応の結論は出ていると思う*1のだが……。遺族の方には申し訳ないが、具体的利益のためにではなく、みずからの政治的主張のために裁判所を利用しているように見えて仕方が無い。

Tags: 時事

*1 最近、やいざわさんの<URL:http://www.yaizawa.jp/diary/?date=20060727#p02>へのコメントにも書いた

λ. 万能数値表現法 URR

Matzにっき(2006-07-26)より。面白い表現法だな。ただ、-∞ を表現しつつ +∞ や無限小は表現できないというのは少し気持ちが悪い。何故そうなっているかというと、以下のように区間分割を進めていき、その区間の最小値という形で表現されるため。

  • [-∞,∞)
    • [0, ∞)
      • [0,1)
        • [0.5, 1)
          • [0.25, 0.5)
          • [0.5, 1)
        • [0, 0.5)
          • [0, 0.25)
          • [0.25, 0.5)
      • [1, ∞)
        • [1, 2)
          • [1, 1.5)
          • [1.5, 2)
        • [2, ∞)
          • [2, 4)
          • [4, ∞)
    • [-∞, 0)
      • [-1, 0)
        • [-0.5, 0)
          • [-0.25, 0)
          • [-0.5, -0.25)
        • [-1, -0.5)
          • [-0.75, -0.5)
          • [-1, -0.75)
      • [-∞, -1)
        • [-2, -1)
          • [-1.5, -1)
          • [-2, -1.5)
        • [-∞, -2)
          • [-4, -2)
          • [-∞, -4)

λ. 『GOTH—リストカット事件』 乙一

GOTH―リストカット事件(乙一) を読んだ。 先に漫画の方を読んでいたからか、話の持っていきかたや描写が冗長に思えて仕方が無い。内容は普通に面白かったが。

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

ψ Keigo IMAI [お久しぶりです。 >万能数値表現法 Gray Codeに似てますね。(どちらもちゃんと理解してないんですが) htt..]

ψ さかい [お久しぶりです。 URR と Gray Code ってそんなに似てます? 共通してるのは区間への分割を繰り返す所くら..]

ψ Keigo IMAI [なるほどお…一般的なんですね。]

ψ さかい [多分…… 私が直接見たことのあるのだと、例えばこんな話があります。 Yves Bertot. CoInductio..]


2007-08-02

λ. Modal Algebras

昔、途中で挫折した First Steps in Modal Logic を再び読んでいるのだが、命題 3.4 の自然言語で書かれた証明に頭がこんがらがってきた。以前に読んだ時にはあっさり理解できたはずなのだが……。

これはどういう命題かというと、遷移関係が

  1. 反射的(reflexive)
  2. 推移的(transitive)
  3. pathetic: a R b ⇒ a=b
  4. 稠密(dense): a R b ⇒ ∃x. a R x R b

であることと、□X = {a | ∀x. a R x ⇒ x∈X} で定義される演算子 □ が

  1. Deflationary: □X⊆X
  2. Nearly inflationary: □X⊆□□X
  3. Inflationary: X⊆□X
  4. Nearly deflationary: □□X⊆□X

であることが、それぞれ同値だという命題。

それで、「頭がこんがらがるのは自然言語で証明が書かれているからだ」と思い、Agdaで書いてみた(ModalAlgebras.agda) 一応、頭はスッキリしたが、かえってややこしくなっている気もしないでもない。

追記

ちなみに、反射律を「a=b ⇒ aRb」と書くと、patheticであることと双対の関係にあることが分かる。 同様に、推移律を「(∃x. a R x R b) ⇒ a R b」と書くと、稠密性と双対の関係にあることが分かる。 考えてみれば当たり前だけど、最近まで気付いていなかった。


2008-08-02

λ. Categories with attributes (cwa)

依存型とcatamorphism の話を書くために、まずは依存型を持つ体系の圏論的なモデルとして Categories with attributes を導入する。

Categories with attributes

Category with attributes (cwa) は依存型を持つ計算体系の圏論的なモデルとしてよく使われる圏で、以下の構成要素と条件からなる。

  • 圏 C
  • 終対象 1∈|C|
  • 前層 Fam : Cop → Set
    • 射に対する作用については S[f] := Fam(f)(S) という記法を用いる。
  • 任意の Γ∈|C| と S∈Fam(Γ) に対して、Γ・S ∈ |C| という対象と射 πS : Γ・S → Γ が存在する
    • 記法を濫用して πS のことを、単に S と書くことがある。
  • 任意の射 f : Δ → Γ と S∈Fam(Δ) に対して、射 f・S : Δ・S[f] → Γ・S が存在して、
    \xymatrix@+15pt{ \Delta\cdot S[f] \ar[r]^{f\cdot S} \ar[d]_{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Delta \ar[r]_{f} & \Gamma }
    がpullbackになっていて、さらに idΓ・S = idΓ・S と (f∘g)・S = (f・S)∘(g・S[f]) が成り立つ

依存型を持つ体系のcwaでの大雑把な解釈

まず、πS の section からなる集合を Tm(Γ, S) := {M: Γ→Γ・S | πS∘M = idΓ} と書くことにする。 そうすると、依存型を持つ体系はcwaに大雑把にはこんな感じで対応する。

  • 文脈 Γ は Γ∈|C| に対応し
  • 文脈 Γ での型 S 、すなわち Γ ├ S set であるような S は、S∈Fam(Γ) に対応
  • 文脈 Γ での項 M 、すなわち Γ ├ M : S であるような M は、M∈Tm(Γ, S) に対応

これは一見すると奇妙な解釈に見えるけど、スライス C/Γ を考えると、普通の解釈を一般化したものになっている。 C/Γでの終対象は C の idΓ: Γ→Γ なので、C での πS : Γ・S → Γ を C/Γ では単にSと書くことにすると、M∈Tm(Γ, S) は C/Γ ではちゃんと点 1→S とみなすことが出来る。
\xymatrix{ \Gamma \ar@{=}[dr] \ar[rr]^{M} & & \Gamma\cdot S \ar[dl]^{\pi_S} \\ & \Gamma }

代入

それから、M∈Tm(Γ, S) と f : Δ→Γ に対して、M[f] ∈ Tm(Δ, S[f]) を、pullback の性質から以下の図のように定義する。
\xymatrix@+15pt{ \Delta \ar@{=}@/_1pc/[ddr] \ar@/^1pc/[rrd]^{M\circ f} \ar@{.>}[dr]|{M[f]} \\ & \Delta\cdot S[f] \ar[r]_{f\cdot S} \ar[d]^{\pi_{S[f]}} & \Gamma\cdot S \ar[d]^{\pi_S} \\ & \Delta \ar[r]_{f} & \Gamma }

S[f] や M[f] と書いたが、これらはもちろん代入(substitution)を表している。 例えば、Γ ├ N : T と Γ, x : T ├ M : S から Γ ├ M[x:=N] : S[x:=N] を得ることが、N ∈ Tm(Γ, T) と M ∈ Tm(Γ・T, S) から M[N] ∈ Tm(Γ, S[N]) を得ることに対応している。
\xymatrix@+15pt{ \Gamma\cdot S[N] \ar[d]^{\pi_{S[N]}} \ar[r]^{N\cdot S} & \Gamma\cdot T\cdot S \ar[d]^{\pi_S} \\ \Gamma \ar[r]_{N} \ar@<1ex>[u]^{M[N]} & \Gamma\cdot T \ar@<1ex>[u]^{M} }

このように、構文的な代入を意味論的な代入にうまく対応させられるのが、cwaの嬉しいところ。

ただ、ちょっと面倒なのは weakening をする際にも、型や項の側では要らない変数を捨てるような代入を明示的に適用しなくてはいけないところ。 例えば、Γ ├ S set と Γ ├ M : S から weakening で Γ, x : T ├ S set と Γ, x : T ├ M : S を得るのは、S∈Fam(Γ) と M∈Tm(Γ, S) から、πT : Γ・T → Γ を使って S[πT]∈Fam(Γ・T) と M[πT]∈Tm(Γ・T, S[πT]) を得ることに対応する。
\xymatrix@+15pt{ \Gamma\cdot T\cdot S[\pi_T] \ar[d]^{\pi_{S[\pi_T]}} \ar[r]^{\pi_T\cdot S} & \Gamma\cdot S \ar[d]^{\pi_S} \\ \Gamma\cdot T \ar[r]_{\pi_T} \ar@<1ex>[u]^{M[\pi_T]} & \Gamma \ar@<1ex>[u]^{M} }

これくらいの例なら問題ないのだけど、ちょっと複雑なものを書こうとすると、すぐ訳がわかんなくなってしまうよ……*1

*1 うまい絵算の方法でもあるといいんだけどねぇ


2009-08-02

λ. 『洗脳原論』 苫米地 英人

洗脳原論(苫米地 英人)

読了。

Tags: