あいさつ
計算機による一階述語論理の決定不能の取り扱い方を調べる中で
コンビネーター理論の理解が深まったので筆を取る事にした.
このたぐいのテクを用いると、識別子に依らない関数の再帰を定義出来る（！！）
# Zコンビネーター
Z = ->(f) {
->(x){
f.(
->(y) {x.(x).(y)}
)
}.(
->(x){
f.(
->(y) {x.(x).(y)}
)
}
)
}
# 識別子に依らずに階乗を定義！
Z.(->(_){ ->(n){ n == 0 ? 1 : n * _.(n-1) } }).(5)
# => 120
以下説明
自分の理解度の確認のためにも用語を１つ１つ丁寧に積み重ねて分かりやすくしたつもり.
λ式とは
λ式なんていかがわしい言葉を使っているがメチャ簡単な事、でも実は難しい.
皆さんおなじみ２次関数
f(x) = x ^ 2
「引数を二乗する手続きが大事で、関数名はfでもgでも構わんし邪魔」
って事はよくあると思うので、この手続きのみを抽出して抽象化したのがλ式
\lambda x. x^2
λ式の性質について述べきる事は不可能だが、単純ながらかなりパワフルな概念の１つ.
Rubyならブロック(Proc)とかlamdaとかで表せられる
->(x) { x ** 2 }
Haskellなら
(\x -> x^2)
Rubyはλ式そのものがオブジェクトとして存在出来てモノ感が強烈だ.
コンビネーターとは
玉虫色の言葉なので文脈に意味が依存しがちだが、この記事の文脈では、
コンビネーター...λ式全体の部分集合で、λ式のうちその引数によってのみ計算が構築されるもの.
とする. 簡単に言えば自由変数項がなく、余計な変数項がない計算に含まれないλ式.
# コンビネーターである
->(x) { x }
->(x) { ->(y) { x } }
# コンビネーターでない
->(x) { x + y }
-- コンビネーターである
\x -> x
\x -> \y -> x
-- コンビネーターでない
\x -> x y
不動点とは
不動点...引数と返り値が等しい様な値
aが関数fの不動点である事の必要十分は
f(a) = a
単純な例
f(x) = x ^ 2
の不動点は0, 1.
f(0) = 0 ^ 2 = 0\\
f(1) = 1 ^ 2 = 1
不動点コンビネーターとは
不動点コンビネーター...関数fを引数に取って関数fの不動点を返り値とするコンビネーター
コンビネーターCが関数fの不動点コンビネーターである事の必要十分は
f\bigl(C(f)\bigr) = C(f)
Yコンビネーターとは
Yコンビネーター...不動点コンビネーターの一つの例.
Y = (\lambda f . (\lambda x . f (x x)) (\lambda x . f (x x)))
要はちょっと入り込んだλ式.
Yコンが分かった所でRubyでチャレンジ
とりあえず愚直にRubyのラムダ式に落とす
Y = (\lambda f . (\lambda x . f (x x)) (\lambda x . f (x x)))
とりあえずこの式をRubyのλ式に落としてみた.
Y = ->(f) {
->(x) {
f.(x.(x))
}.(
->(x) {
f.(x.(x))
}
)
}
けっこイイじゃない、見た目.
こいつがYコンや、とりあえず愚直に定義に従って
\lambda x. x
の不動点を求めようとしてみる.
レッツ、コンビネート
f = ->(x){ x }
Y.(f)
# => SystemStackError: stack level too deep
SystemStackError: stack level too deep
ハイハイ. Yコンは不動点コンビネーターの中でもシンプルな例で評価戦略が値渡しだと無限ループを起こすようだ
そこでZコンビネーター
Zコンビネーター...Yコンビネーターをパワーアップさせたやつ.
Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
こいつなら値渡しでもおk. シコシコとRubyに翻訳
Z = ->(f) {
->(x){
f.(
->(y) {x.(x).(y)}
)
}.(
->(x){
f.(
->(y) {x.(x).(y)}
)
}
)
}
けっこイイじゃない、見た目.
レッツ、コンビネート
f = ->(x){ x }
Z.(f)
# => #<Proc:0x007fd1fd479cb8@(pry):129 (lambda)>
なんか返ってきたがこいつは一体...
v1 = Z.(f)
# => #<Proc:0x007fd1fd479cb8@(pry):129 (lambda)>
v2 = f.(Z.(f))
# => #<Proc:0x007fd1fd3c4908@(pry):129 (lambda)>
ZがZコンビネーター的な役割を果たすならば、v1とv2が同じ構造を持つλ式はずですが
動的に作られた異なるProcオブジェクトの同一性を判断するにはどうしたら...
頭を悩ましRubyのメーリスで投げかけた所、
RubyVM::InstructionSequenceを使うと良いとのご教授を頂いた.
ありがとうございました.
ISeq = RubyVM::InstructionSequence
ISeq.of(v1) == ISeq.of(v2)
#=> true
やった！うまくコンビネート出来てる！
この際Proc#==を上書いてしまえ
class Proc
def ==(other)
RubyVM::InstructionSequence.of(self) == RubyVM::InstructionSequence.of(other)
end
end
f.(Z.(f)) == Z.(f)
#=> true
ウオオオォ
どうなってんだよRuby.
計算手続きのそのもの同値性を確認出来るのはマジで使える.
再帰関数を識別子なしで定義
Z.(->(_){ ->(n){ n == 0 ? 1 : n * _.(n-1) } }).(5)
#=> 120
お、いい感じね.
皆さん良いお年を.