2001-12-08
λ. LLP: A Linear Logic Programming Language and its Compiler System
ふむふむ。WAMの勉強に丁度良いらしいので、後で見てみよう。
λ. Graphviz - open source graph drawing software (from 心身のバックアップ日記)
こんな便利なツールがあったとわ。情報数学Ⅰの授業で使わせてもらえば良かった。しかもRubyのバインディングまであるなんて最高。
2003-12-08
λ. イラク人道復興支援特措法に基づく対応措置に関する基本計画
私は中東情勢とかの事はよく知らないので、自衛隊派遣についてどうこう言うつもりもないけど、願わくば、一人も欠けることなく無事に日本へと帰って来て欲しいものだ。
そういえば、90式戦車とかは持ってかないんですね……
λ. ACL
acltomode/aclfrommode と acltopbits/aclfrompbits の違いは何だろう? man:acltomode(3) と man:acltopbits(3)を見る限り、使う定数しか違わないように見えるのだが……
Cygwinにはmodeとpbitsの両方ある。solaris 2.6 にはmodeの方しか存在しなかった。
……って、POSIX ACL はまた別なのか。LinuxとFreeBSDのAPIは POSIX ACL と。そうすると、ACLを扱うプログラムをポータブルに書くにはどうするのが一番よい? getfacl/setfaclコマンド?
λ. 読書
- 『マリア様がみてる — いばらの森』
- 今野 緒雪 [著], ひびき 玲音 [イラスト]
2004-12-08
λ. Announce: 圏論勉強会 (第二回)
そうそう。今週末は圏論勉強会の二回目がありますよ。堅苦しい集まりではないし、特に前提知識は必要ないので、圏論に興味のある人は是非お気軽に御参加下さい。(初参加の方は mixi:圏論勉強会(第二回) か haskell-jpメーリングリスト で参加を表明しておくと良いと思います)
- 日時
- 2004年12月11日(土曜) 14:00〜
- 場所
- タイムインターメディア様 2階会議室 (地図)
- テキスト
- Conceptual Mathematics: A First Introduction to Categories
2005-12-08
λ. 西尾レントオールがストップ高
昨日買い損ねた西尾レントオールがストップ高。小銭を惜しんで儲けを逃した。 もっとも、実際に騰がった原因は、僕が期待していた耐震検査関係ではなく、『UBS証券が同社株を新規「Buy2」、目標株価を3500円とした』ことだったので、別に予想が当たったわけではないのだけど、悔しいものは悔しいな。
λ. スクリプト言語Rubyの拡張可能な多言語テキスト処理の実装, 松本行弘 縄手雅彦
を読んだ。
2006-12-08
λ. 自由変数と限量子∀∃
かがみさんが「自由変数って」ということを書いていたので、自分の自由変数の理解を書いてみる。
任意の言語Lに対して、Lに含まれない定数記号xを新たに加えた言語をL{x}とする。そして、自由変数を含む式 φ(x) はLの式ではなくL{x}の式と考える。L{x}に更に新たな定数記号yを加えた言語はL{x}{y}と書けるが、L{x}{y}とL{y}{x}は区別せずに単にL{x,y}と書くことにする。そうすると、論理式φの自由変数の集合がFV(φ)であるとき、φ∈L(FV(φ))が成り立つ。
それから、LからL{x}への埋め込み I: L→L{x} が定義できる。この埋め込みには右随伴 L{x}→L や左随伴 L{x}→L が存在する場合があり、それぞれ(∀x)や(∃x)と書かれる。すなわち、任意の φ∈L, ψ∈L{x} に対して
- I(φ) |-L{x} ψ iff φ |-L (∀x)(ψ)
- (∃x)(ψ) |-L φ iff ψ |-L{x} I(φ)
【2006-12-14 追記】 檜山さんが「論理とはなにか？ (4:完) -- 論理から圏へ」で、「論理と圏の対応関係がうまくいっている例として直観主義論理があります」と書いていましたが、限量子を随伴で説明できることから、述語論理も圏と対応させることが出来ることがわかります。
