2002-08-28
λ. DRb vs Gtk::Plug & Gtk::Socket
なかださんが「面白そう」と言ってくれたので、試しに簡単なものを作ってみる。細かなエラー処理などは省略。
# drbembed.rb
require 'drb'
require 'gtk2'
module DRbEmbed
class Socket < Gtk::Socket
def initialize
super()
@drbobj = nil
end
def add(arg)
@drbobj = arg
add_id(@drbobj.__drb_embed_plug_id__)
end
end
end
module Gtk
class Widget
def __drb_embed_plug_id__
if parent
unless parent.is_a? Gtk::Plug
raise TypeError.new("parent isn't Gtk::Plug")
end
else
Gtk::Plug.new.show.add(self)
end
parent.id
end
end
end
次に埋め込まれるWidgetの例。DRbを普通に使ってるだけ。
require 'drbembed'
server = DRb::DRbServer.new(nil, Gtk::Button.new('This is remote widget'))
puts server.uri
Gtk.main
で、このWidgetをリモートから使ってみる。コンテナとしてDRbEmbed::Socketを使う事以外、ほとんど何も気にしなくて良いはず。
require 'drbembed'
there = ARGV.shift || raise("usage: #{$0} <server_uri>")
DRb.start_service(nil, nil)
remote_widget = DRb::DRbObject.new(nil, there)
win = Gtk::Window.new
socket = DRbEmbed::Socket.new
win.add(socket)
win.show_all
socket.add(remote_widget)
remote_widget.show
remote_widget.signal_connect('clicked'){
puts 'Hello DRb!'
}
Gtk.main
う〜ん。もう少し改良の余地があるかな。
2005-08-28
λ. クロージャ
もちろん、Haskellでも出来ますよ。
ioCounter :: IO (IO Integer)
ioCounter =
do ref <- newIORef 0
return $ do modifyIORef ref (1+)
readIORef ref
test =
do c <- ioCounter
c >>= print -- => 1
c >>= print -- => 2
【2006-03-28 追記】 鷲見さんの sumim’s smalltalking-tos の 「Perl6 あなどれじ。クロージャ記述の短さ対決！」というエントリのコメントで、このコードを元に増分を毎回指定できるようにしたバージョンが紹介されていた。面白い。
2006-08-28
λ. 人狼SNSに参加
stinさんに招待していただいたので、参加。 stinさん、ありがとうございました。
<URL:http://wolfsbane.jp/?m=pc&a=page_f_home&target_c_member_id=474>
2007-08-28
λ. ビジネス実務マナー技能検定試験2級
合格していた。
λ. Paradoxes of classical predicate calculus
The Coq Proof Assistant - A Tutorial の「Paradoxes of classical predicate calculus」のところが面白い。古典一階述語論理だと Smullyan's drinkers' paradox 「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」が証明できてしまうそうだ。 へぇ。
例によってagdaで示してみる。
drinker (!D::Set) (!d::D)
(!EM::(X::Set) -> Either X (Not X))
(!P::D->Set)
:: Exist (\(x::D)-> P x -> (y::D) -> P y)
drinker =
case EM (Exist (\(x::D) -> Not (P x))) of
(Left e )->
struct
fst :: D
fst = e.fst
snd :: P fst -> (y::D) -> P y
snd = \(px::P fst) -> case e.snd px of { }
(Right ne)->
let f (!x::D) :: P x
f = case EM (P x) of
(Left px )-> px
(Right npx)->
let e :: Exist (\(x::D) -> Not (P x))
e = struct
fst :: D
fst = x
snd :: Not (P fst)
snd = npx
in case ne e of { }
in struct
fst :: D
fst = d
snd :: P fst -> (y::D) -> P y
snd = \(z::P d) -> f
ところで、zyxwvさんが謎と思っているのはどの部分なんだろう? 一階述語論理の推論規則の話だろうか?
一階述語論理の推論規則には 「∀x.P[x] から P[t] を導く規則」や「P[t] から ∃x.P[x] を導く規則」が含まれている(ヒルベルト流でも自然演繹でもシーケント計算でも)。 ここでビミョーなのが一階述語論理では勝手に自由変数を置いて使える点。 そのため、一階述語論理では勝手に置いた自由変数tについて (∀x.P[x]) → P[t] が証明出来る。同様に P[t] → (∃x.P[x]) も証明できるため、それらから (∀x.P[x]) → (∃x.P[x]) も証明出来る。 しかし、論理式の意味を考えると、∀x.P[x] は領域が空なら真である一方で、∃x.P[x] は領域が空なら偽だし、さらに P[t] は領域が空なら解釈不能になってしまう。 これらの矛盾を避けるため、一階述語論理のモデル論では領域Dは空集合でないこと前提とされている。
一方、Coq等の基づいている型理論では自由変数を勝手に置いたり出来無いため、これらを一階述語論理の場合と同様に証明する証明することは出来ないし、またDが空集合である場合も許される。 そのため、ここでは一階述語論理を模すため、Dの要素dの存在を明示的に仮定している。
(追記: 「定数記号」と書いていた部分を「自由変数」に変更した)
![[カタツムリ]](./images/20080828_0.jpg)
