2001-08-08
λ. Gimp-Ruby
Gimp-PerlでもPDLを使ってるし、Gimp-Rubyでもメモリを効率的に操作するライブラリを使いたくなって来た。探してみると幾つかあるみたい。
λ. これから色々試してみようと思うけど、扱うのは主に画像データなので、線形代数的な機能の充実度はあんまし必要無くて、むしろ以下のような、あまり本質的でない部分が気になってる。
- C言語レベルでのインターフェースが洗練されていて、ドキュメントもちゃんとあるか?
- ポインタと開放用の関数を渡すことで、既にあるメモリブロックをラッピング出来るか?
- 既にあるメモリブロックを一時的にラッピングしてアクセス出来、そして、メモリが無効になった事を通知して、以降はアクセス出来ないようにする…といったことが出来るか?
- 非UNIX環境でもきちんと動作する。Windowsだとシンボルをちゃんとエクスポートして、他の拡張ライブラリから呼び出すことが出来るようになってるか?
λ. 誰か、お勧めのライブラリを教えて下さい。
> 既にあるメモリブロックを一時的にラッピングしてアクセス出来、そして、メモリが無効になった事を通知して、以降はアクセス出来ないようにする…といったことが出来るか?
—— アクセス出来ないようにはできないでしょう。どうしたいのか具体的にはわからないけど、タイミング的に難しいのでは。
アクセス出来ないようにってのは、既にcloseしたファイルとか、既に無効になってしまったWeakRef等と同様に、操作しようとすると例外が発生するってのを考えてました。
それと、念頭にあったのは、メモリブロックを受け取るようなコールバック関数です。C言語で定義されたコールバック関数内で、Ruby側で定義された実際の関数を呼び出して、引数としてメモリブロックを渡したいんです。そのコールバック関数を抜けたあと、そのメモリブロックがどうなるかは保証の限りではないので、普通はデータをまるごとコピーする必要があります。でも、使われるかどうかも分からない引数にそこまでするのも無駄な気がしますし、こういう機能があれば、一時的にラッピングしておいて、コールバック関数を抜ける際に通知して、以降はアクセス出来ないようにするという事が出来ると思ったんです。…やり過ぎかな。
> 非UNIX環境でもきちんと動作する。Windowsだとシンボルをちゃんとエクスポートして、他の拡張ライブラリから呼び出すことが出来るようになってるか?
—— どうすればできるんでしょうか?
Windowsだと.defファイルに記述されたシンボル以外はエクスポートされなくて外部からアクセスできないので、外部から呼び出すためには適切な.defファイルを作成する必要があります。ちなみに、mkmf.rbのcreate_makefile関数は.defファイルが存在しない場合に「Init_拡張ライブラリ名」だけを記述した.defファイルを自動生成します。
2003-08-08
λ. ITスキル標準人材育成研修
ORDBとUDFの話。実習はUDFを使った高度な検索ということだったので、SQLのLIKEって使いにくいなぁとも思っていたし、鬼車を使って正規表現によるマッチングなどやってみる。しかし、text構造体のvl_lenを、構造体のサイズではなく、vl_datの要素数と勘違いして、時間を結構無駄にしてしまい、あんまりたいしたことはやれなかった。くそぅ。
なんにしても、データベースコースは今日でお終い。それほど新しい知識を得たわけではないけれど、これまであまり縁の無かったデータベースを、ずいぶん身近に感じられるようになりました。吉田さんありがとう。
λ. MCC
案内用の画面って、あれはWindowsだったのか。「更新の通知」がポップアップしていて気がついた。しかもPowerPointかよ……
λ. 夕食
せっかく東京に出てきていたので、この機会にむとうさんと夕食。場所は壁の穴で、むとうさんに奢ってもらってしまった。感謝。おいしかったです。むとうさんに会ったのは初めてなのですが、想像していた以上にナイスガイでした。2人とも「まつもとゆきひろさんを囲む会」には申し込んでいなかったのはちょっぴり残念でしたが、とても楽しかったです。しかも、むとうさんに自宅まで送ってもらってしまいました。これまた感謝。ちなみに、むとうさんの車カッコよかったっす。
2004-08-08
λ. Lightweight Language Weekend 二日目
「その場でどう書く」の発表者は 9:30 集合だったのだけど特に打ち合わせをするでもなく10:00に。「その場でどう書く」の課題の発表を聞いて、ちと焦る。というのも、サーバ側でIOを行うときのWASHの流儀について何も調べてなかったのだった(ダメじゃん)。で、「LLとblog」のセッションを聞きながらコーディングしようと思ったら、なんかネットワークの調子が悪かったので控え室の方へ。まずはカレンダーを表示する部分を、メッセンジャーでお馬鹿な会話をしつつ、へろへろと書いていたら、これ思ったより面倒なんだよね。気が付いたら12時近いのに、まだカレンダーが表示できてねーよ!! この辺りで焦ってパニック状態になり、まともな思考が出来なくなる。その後もダメダメな感じで、LL侍の練習とかスクリーンに映る Lightning Talk の様子とかを横目でみつつ、泣きそうになりながらコードを書くのでした。 で、結局コードはダメダメだったけど、発表自体は全然緊張しなかったし、結構楽しかった。なんか、変な感じでハイだったのかも知れず。
2007-08-08
λ. Djinn, a theorem prover in Haskell, for Haskell.
今更ながら Djinn を試してみた。 Djinnは「型を入力として受け取り、その型を持つ関数を(もし存在すれば)返す」ようなプログラム。これはカリーハワード対応によって「論理式を受け取って、その証明を(もし存在すれば)返す」ことに対応するので、仕組みは定理証明機で、証明をHaskellプログラムとして書いてくれている考えることもできる。
まずは自明な例を試してみる。
Djinn> id ? a -> a
id :: a -> a
id a = a
Djinn> k ? a -> b -> a
k :: a -> b -> a
k a _ = a
Djinn> s ? (a -> b -> c) -> (a -> b) -> (a -> c)
s :: (a -> b -> c) -> (a -> b) -> a -> c
s a b c = a c (b c)
Djinn> bindMaybe ? Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe :: Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe a b =
case a of
Nothing -> Nothing
Just c -> b c
当然動作する。 これが出来るのは当たり前なのだけど、実際に見ると楽しいな。 それと、bindMaybeで定数関数じゃない方の関数が先に出て来るようになっているのはちょっと賢いかも。
再帰的データ型を試そうとしたが、これは対応していないようだ。
Djinn> data List a = Nil | Cons a (List a) Error: Recursive types are not allowed: List
ついでに少し意地悪な例を試してみる(20060429#p02 より)。
Djinn> dn :: Not (Not a) -> a Djinn> em ? Either a (Not a) -- em cannot be realized.
起動時のメッセージには「If the Djinn says the type is not realizable it is because there is no (total) expression of the given type.」と出てくるが、実際には完全ではない?
どんな決定手続きを使っているのか気になるところ。 LtUにはこう書いてある。
For the curious, Djinn uses a decision procedure for intuitionistic propositional calculus due to Roy Dyckhoff. It's a variation of Gentzen's LJ system. This means that (in theory) Djinn will always find a function if one exists, and if one doesn't exist Djinn will terminate telling you so.
また、ljt.p というPrologのコードがついていて、こっちには「Incorporates the Vorobëv-Hudelmaier etc calculus (I call it LJT). See RD's paper in JSL 1992: "Contraction-free calculi for intuitionistic logic"」と書いてあった。 LJTについては、<URL:http://www.computational-logic.org/iccl/events/WPT-2004/> にある“Normalising Permutations in Sequent Calculus”の概要に以下のように書いてあったので、自然演繹とうまく対応するシーケント計算ということのようだ。
In Prawitz's translation from the sequent calculus LJ to natural deduction, many proofs are mapped to the same one and only differ by the order in which inference rules are applied. One can be transformed into another by simple permutations of these rules. By the use of focusing conditions, a canonical proof can be elected in each permutation class, thus forming Herbelin's permutation-free calculus LJT, which is in bijection with proofs in natural deduction.
そういえば、自然演繹とシーケント計算の対応の問題については、去年のSLACSの A subsystem of sequent calculus isomorphic to natural deduction でも取り上げられていたな。私はあまり理解できていなかったけど。
関連
【2011-07-27 追記】
スタートHaskellの @pi8027 さんのLT「型から項を作る」で思い出して、再度試してみる。 Djinnのバージョンはリリースされたばかりの2011.7.23。
上で上手くいかなかった例は、型を具体化してみたら、うまくいった。
Welcome to Djinn version 2011-07-23.
Type :h to get help.
Djinn> dn :: Not (Not (Either a (Not a))) -> Either a (Not a)
Djinn> em ? Either a (Not a)
em :: Either a (Not a)
em =
case dn (\ a -> void (a (Right (\ b -> a (Left b))))) of
Left c -> Left c
Right d -> Right d
ただし、型変数名が違うとダメ。
Djinn> :clear Djinn> dn :: Not (Not (Either b (Not b))) -> Either b (Not b) Djinn> em ? Either a (Not a) -- em cannot be realized.
要は多相型には対応していないということね。 そりゃそうかと納得した。
2008-08-08
λ. マネックス証券の口座開設キャンペーン
マネックス証券が 新規口座開設 & 5万円以上(MRF買い付け)入金で、Amazon®ギフト券5,000円分プレゼント！ というキャンペーンをやっていた。 マネックス証券は、夜間取引のマネックスナイターとか幾つか気になっている機能があって、いい機会なので申し込んでみた。
λ. オリンピック開会式
演出過剰だけど、流石中国はスケールが大きいなと思わせる内容だった。 北朝鮮のマスゲームなんて目じゃないな。 まあ、飽きて途中で見るのを止めてしまったけど。
ところで、エクストリーム・聖火リレーの表彰式 ﾏﾀﾞｧ-? （･∀･ ）っ/凵⌒☆ﾁﾝﾁﾝ
2009-08-08
λ. “New Techniques that Improve MACE-style Finite Model Finding” by Koen Claessen and Niklas Sörensson
以前に、一階述語論理のモデル発見器であるParadoxを使って、数独を解いてみたりしたが、Paradoxの実装に使われている性能を改善するためのテクニックを説明した論文。 Paradoxの使っているテクニックだけでなく、その前提となる一階述語論理の有限モデルをSATソルバーを使って解くための基本的な手法についても分かりやすく書かれている。
splitting
splittingというのは、例えば { P(x, y), Q(x, z) } という節を、新しい述語 S を導入して、
- { P(x, y), S(x) }
- { ￢S(x), Q(x, z) }
という節集合に分割することを指す。
splitting をすることによって、個々の節に含まれる変数を減らすことが出来る。 節のインスタンス化(= 基礎化(grounding)?)の際に、節の数が変数の数の指数オーダーで膨れ上がるので、節に含まれる変数の数を減らすのは非常に重要。
splittingのためのヒューリスティックは色々あるが、これまでのはあまり良くなかった。 そこで、Paradoxで採用しているのは「述語をノード、述語のリテラルが変数を共有するという関係をエッジとするようなグラフを考え、その最小の連結成分をsplittingによって分離する、ということを繰り返す」というもの。
term definition
ひとつの目の新しいテクニックは、節に含まれる変数を減らすための term definition 。
例えば、{ P(f(a, b), f(b, a)) } を普通にフラット化すると、4つの変数を含む節 {a ≠ x, b ≠ y, f(x, y) ≠ z, f(y, x) ≠ w, P(z,w)} になってしまうけど、新しい定数記号t1,t2を導入して
- { t1 = f(a, b) }
- { t2 = f(b, a) }
- { P(t1, t2) }
という節集合に変換しておくと、フラット化したときに、
- { a ≠ x, b ≠ y, f(x, y) ≠ z, t1 = z }
- { a ≠ x, b ≠ y, f(y, x) ≠ z, t2 = z }
- { t1 ≠ x, t2 ≠ y, P(x, y) }
という、各々の節が3変数しか含んでいないような節集合に出来る。
increamental SAT
二つ目の新しいテクニックは、SATソルバーのインクリメンタルな機能の活用。 MACEスタイルの方法では、モデルのサイズnを増やしながら、サイズnのモデルの探索をSAT問題に落として、SAT solver に解かせる。これまではこれを毎回一からSATソルバーにかけていたが、SATソルバーのインクリメンタルな機能を使うことで、サイズnでの探索で得られた情報(特に conflict learning の結果)をSATソルバーがその後の探索で利用でき、探索を効率化出来る。
これをするにはSATへのエンコーディングを少し工夫する必要がある。
static symmetry reduction
三つ目の新しいテクニックは、同型なモデルを排除するような制約を制的に導入すること。 SEMのように自分で探索をする場合には探索を進めながらゴニョゴニョできるけど、SATソルバーを使うので探索を始める前に制約を静的に与えておかなくてはいけないのが難しい。
定数記号 {ai}i について考えると、I(ai)≦i すなわち
- { a1 = 1 }
- { a2 = 1, a2 = 2 }
- { a3 = 1, a3 = 2, a3 = 3 }
- …
という節集合によって値域を制限し、さらに 1 < i ∈ D と 1 < d ≦ i について、
- { ai≠d, a1 = d-1, a2 = d-1, …, ai-1 = d-1 }
という節を導入することで、aiの値をa1,…,ai-1で使われている値か、もしくはa1,…,ai-1で使われていない値のうちの最小のものに限定する。
関数記号がある場合についても同様だが、この場合には同型なモデルを完全に排除することは出来ない。
sort inference
四つ目の新しいテクニックはソート(型)の推論。 ソートの推論をすることで、ソート単位で symmetry reduction が出来るようになり、より細かい symmetry reduction が出来るようになる。 具体的な型推論は、関数(の引数と返り値)と述語(の引数)がすべて異なるソートを持つと仮定して、それから同じ変数が使われているところのソートを同じにしていくという、普通の方法でやっている。
