人気ブログランキング |

<   2019年 09月 ( 31 )   > この月の画像一覧

ラムダ計算 SKI コンビネータ 3


ラムダ記法の関数を SKI コンビネータで表すのは機械的にできる。次の3つのルールを機械的に適用していくだけだ。

1)λx.M = M ... λ抽象は外して良い
2)((x z) (y z)) = (S x y) z ..... (x z) (y z) の形の関数適用は変数 z をくくり出せる。
3)x = I x ..... 変数 x だけの項は (I x) の形に変えることができる。
4)a = (K a) x ..... 項 a は (Ka) x の形に変えることできる。このとき、(K a) を関数適用する x は任意の項を使うことができる。

このルールに従って、前回も紹介した、

λxyz.x(yz)

を SKI コンビネータで置き換えてみると、次のようになる。

lambda> (lx.(ly.(lz.(x (y z)))))
(lx.(ly.(lz.(x (y z)))))
lambda> (x (y z)) ...... ルール1)を使ってラムダ抽象を除去して body だけにする。
(x (y z))
lambda> (((K x) z) (y z)) ..... ルール4)を使って x --> (K x) z にする。
(x (y z))
lambda> (((S (K x)) y) z) ..... ルール2)を使って z をくくりだす。
(x (y z))
lambda> (((((K S) x) (K x)) y) z) .... ルール4)を使って S -> (K S) x にする。
(x (y z))
lambda> (((((S (K S)) K) x) y) z) ..... ルール2)を使って x をくくりだす。
(x (y z))
lambda> (= M ((S (K S)) K)) .... 求めるコンビネータは S(KS)K である。
lambda> (((M x) y) z)
(x (y z))

ラムダ記法の関数は、atom か、関数抽象か、関数適用のどれかで記述されているので上のルールを適用していけば、どのようなラムダ項も SKI コンビネータで記述することができる(はずだ)。

しかし、上のルールは変数が1回しか現れないときは機械的に適用できるが、(x (x x)) の様に同じ変数が何回も現れる場合は適用できるのだろうか。

lambda> (x (x x))
(x (x x))
lambda> (x ((I x) (I x)))
(x (x x))
lambda> (x (((S I) I) x))
(x (x x))
lambda> ((I x) (((S I) I) x))
(x (x x))
lambda> (((S I) ((S I) I)) x)
(x (x x))
lambda> ((S I) ((S I) I))
(lz.(z (z z)))

問題ないようだ。

by tnomura9 | 2019-09-30 18:54 | Haskell | Comments(0)

ラムダ計算機 設定ファイル


ラムダ計算機に関数の定義を読み込ませる設定ファイル defined.txtもだいぶ充実してきたので別記事として紹介することにした。ラムダ計算機に設定ファイルを読み込ませるためには次のように :load コマンドを用いる。ラムダ計算機 lambda.hs は runghc で起動することもできるし、ghc lambda.hs でコンパイルすれば lambda コマンドで実行できる。

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> ((Y g) 3)
(ls.(lz.(s (s (s (s (s (s z))))))))

設定ファイル: defined.txt

$ cat defined.txt
(= true (lx.(ly.x)))
(= false (lx.(ly.y)))
(= NOT (lx.((x false) true))))
(= AND (lx.(ly.((x y) false)))))
(= OR (lx.(ly.((x true) y)))))
(= IMPLY (lx.(ly.((OR (NOT x)) y))))
(= 0 (ls.(lz.z)))
(= succ (lw.(ls.(lz.(s ((w s) z))))))
(= pred (ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x))))))
(= add (lx.(ly.((x succ) y))))
(= mult (lx.(ly.((x (y succ)) 0))))
(= 1 (succ 0))
(= 2 (succ 1))
(= 3 (succ 2))
(= 4 (succ 3))
(= 5 (succ 4))
(= 6 (succ 5))
(= 7 (succ 6))
(= 8 (succ 7))
(= 9 (succ 8))
(= isZero (lz.(((z false) NOT) false)))
(= pair (lx.(ly.(ls.((s x) y)))))
(= fst (lp.(p true)))
(= snd (lp.(p false)))
(= cons (la.(lb.(lf.((f a) b)))))
(= car (lx.(x true)))
(= cdr (lx.(x false)))
(= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))
(= g (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))
(= Z (lf.((lx.(f (ly.((x x) y)))) (lx.(f (ly.((x x) y)))))))
(= I (lx.x))
(= K (lx.(ly.x)))
(= S (lx.(ly.(lz.((x z) (y z))))))


by tnomura9 | 2019-09-29 19:30 | Haskell | Comments(0)

ラムダ計算 SKI コンビネータ 2


SKI コンビネータでどんなコンビネータが作れるか試してみた。まず I コンビネータは恒等関数だし、K コンビネータは定数関数だ。これは論理値の true に当たる。これを利用して KI コンビネータで論理値の false が作れる。その他、SKK コンビネータは I コンビネータと同じ。SII コンビネータで自己言及コンビネータが作れる。

lambda> I
(lx.x)
lambda> K
(lx.(ly.x))
lambda> (K I)
(ly.(lx.x))
lambda> ((S K) K)
(lz.z)
lambda> ((S I) I)
(lz.(z z))

これは端末から色々と入力すると自然に見つかるが、目的のラムダ項を作るための方法はないのだろうか。そこで単なる関数適用 (x y) を SKI コンビネータで記述するにはどうすればいいか考えてみた。

lambda> (x y)
(x y)
(I x) = x だから ((I x) y) = (x y) になる。

lambda> (I x)
x
lambda> ((I x) y)
(x y)

これは I コンビネータに x と y の2つの引数を与えると、関数適用になることを示している。つまり、関数適用を行うコンビネータは I だ。

それでは、 (x (y z)) の場合はどうすればいいだろうか。

 lambda> (x (y z))
(x (y z))

変数 z は (S (x z)) ((y z)) の形を取ると引数として外にくくり出せる。そこでまず、x を (K x) z の形に変える。

lambda> (((K x) z) (y z))
(x (y z))

これで z をくくりだして body の部分を ((S (K x)) y) の形にまとめることができる。

lambda> (((S (K x)) y) z)
(x (y z))

この時点で変数 y も z もくくりだされてしまったので後は x を外に出すだけだ。変数 x が含まれるのは (K x) の部分なので (S (K x)) の関数適用の部分を (S (x z)) (y z)) の形に整える必要がある。K コンビネータを利用すれば S = ((K S) x) に置き換えることができる。

lambda> (((((K S) x) (K x)) y) z)
(x (y z))

((K S) x)) (K x) の関数適用の部分は S コンビネータを利用して変数を外にくくりだすことができる。すなわち、((K S) x)) (K x)) = ((S (K S)) K)) (x) である。

lambda> (((((S (K S)) K) x) y) z)
(x (y z))

無事に全ての変数をくくり出せたので、

S(KS)K

が求めるコンビネータである。

lambda> (= M ((S (K S)) K))
lambda> (((M x) y) z)
(x (y z))



by tnomura9 | 2019-09-29 08:25 | Haskell | Comments(0)

ラムダ計算 SKI コンビネータ


コンビネータとはラムダ式の body の変数が全て束縛変数となるラムダ式(関数)のことだ。例えば λx.x は引数の値をそのまま返す恒等関数だが、ラムダ抽象された変数は x で body の部分の変数も x しかない。

lambda> ((lx.x) a)
a

このようなコンビネータには名前がつけられているものがある。上の恒等関数にも名前がつけられており I (Identity combinator) コンビネータと呼ばれる。

I = λx.x

ラムダ計算機で検証すると次のようになる。

lambda> (= I (lx.x))
lambda> (I a)
a

また、K コンビネータ (Constrant combinator) は2つの引数を持ち、第一の引数を渡すと、引数1個の関数になる。この関数は引数にどのような値を与えても最初に与えられた第1引数の値を返す。このため定数関数と呼ばれている。

K = λxy.x

ラムダ計算機では次のようになる。

lambda> (= K (lx.(ly.x)))
lambda> ((K a) x)
a

S コンビネータ (Substitution Combinator) は構造が複雑で、第3引数に第1引数を関数適用したものを、第3引数に第2引数を関数適用したものに関数適用する。

S = λxyz.(xz)(yz)

ラムダ計算機では次のようになるが、あまり有り難みがわからない。

lambda> (= S (lx.(ly.(lz.((x z) (y z))))))
lambda> (((S x) y) z)
((x z) (y z))

実は、この SKI コンビネータには特別な性質がある。この3つを組み合わせると、ラムダ抽象を使わずにどのようなラムダ式でも記述できるのだ。そこで、それを検証してみることにする。

先ず、恒等関数だが、これは I コンビネータそのものだ。

lambda> I
(lx.x)
lambda> (I a)
a

また、K コンビネータは論理式の true そのものだ。

lambda> K
(lx.(ly.x))
lambda> ((K a) b)
a

そこで K コンビネータを I コンビネータに関数適用すると、それは false になる。

lambda> (K I)
(ly.(lx.x))
lambda> (((K I) a) b)
b

true と false ができたので、条件分岐を作ってみたいが、ラムダ抽象を使わずにどうやって作ればいいのだろうか。条件分岐は引数が c x y の3つなので I コンビネータや K コンビネータでは役不足だ。それで、S コンビネータを使うことを考えてみる。作りたいラムダ式は次のようなものだ、

λcab.cab

このラムダ式の body の部分を取り出すとこれは ((c a) b) である。これは変数 a を変数 b と c に順に関数適用していることを示している。

lambda> ((c a) b)
((c a) b)

そこで I コンビネータを c に関数適用すると次のようになる。

lambda> (((I c) a) b)
((c a) b)

すなわち I コンビネータが条件分岐を表す関数である。I = λx.x なので I は引数を一つしか取らないが、(I a) の値は関数なので引数を取れる。したがって、I は結果的に3つの引数を取ることが可能なのだ。これがラムダ式が高階関数であることの威力だ。

lambda> I
(lx.x)
lambda> (I true)
(lx.(ly.x))
lambda> (((I true) a) b)
a

Ω - コンビネータ λ.(x x) は最も単純な自己言及関数だが、これも SKI コンビネータで表現できる。Ω - コンビネータの body の部分を次のように等価なラムダ式に置き換えていけばいい。

lambda> (x x)
(x x)
lambda> ((I x) (I x))
(x x)
lambda> (((S I) I) x)
(x x)

したがって、Ω = SII である。

ラムダ式を SKI コンビネータで表すと、束縛変数が表に出てこない。ラムダ抽象を使わずに関数適用のみでラムダ式を記述することができるからだ。スタックにプッシュしたデータをやり取りする場合のように、束縛変数の名前が不要になってしまう。すなわち、α変換に関して考慮しなくて良くなる。コンビネータにはこのようにプログラミングのフレームワークを変える性質もあるようだ。そうして、この SKI コンビネータはラムダ記法と同じ様にチューリング機械と同等の表現力がある「チューリング完全」らしい。

SKI コンビネータのうち I コンビネータは次のように SKK で定義できるので、理論的には S コンビネータと K コンビネータだけで全ての関数が表現できる。しかし、上の例でも分かるように I コンビネータを利用したほうが使いやすい。

lambda> ((S K) K)
(lz.z)
lambda> (((S K) K) hello)
hello


by tnomura9 | 2019-09-28 22:21 | Haskell | Comments(0)

ラムダ計算 括弧の対応


ラムダ計算機では括弧の省略ができないので、どうしても括弧の対応の管理が大変になる。しかしラムダ式の文法の単純さを考えたら、入力のやり方で煩雑さを減らせる。

ラムダ計算で括弧が出現するのは、ラムダ抽象の (λx.M) と関数適用 (M N) の2つだけだ。そのうえ、カッコ内に存在する項は2つしかない。そこで、入力するときに、これらの場合に括弧の対応を先にやってしまっておけば対応する括弧の検討もしなくて済む。

先ずラムダ抽象の場合、(lx.) 括弧の中に変数のラムダ抽象だけを記入する。ボディは後で記入するようにする。たとえば、ラムダ記法の true は次の順序で入力していくとよい。

(lx.)
(lx.(ly.))
(lx.(ly.x))

また、これを変数に束縛するときは (= true ) のように = と 変数名とスペースを括弧でくくったものを最初に作成する。そうしてそのスペースのあとに上の要領でラムダ項を記入していく。

(= true )
(= true (lx.))
(= true (lx.(ly.)))
(= true (lx.(ly.x)))

また関数適用の場合は、何も入れない括弧 ( ) を入力する。そうしてその中に関数適用を記入していくのだ。

()
(() )
((lx.x) )
((lx.x) a)

ユーザーが定義した関数を使うときは、先頭に関数の引数分の括弧を記入する。たとえば、true の様に引数が2個の場合最初に括弧を2つ記入し、そのあとに関数とスペースを置く。それに続けて第1引数とその後ろに閉じ括弧、スペース、第2引数、閉じ括弧という風に記入していく。

((true
((true a)
((true a) b)

このラムダ抽象と、関数適用の書き方の原則を守っていれば比較的複雑な項も括弧の対応をあまり気にしないで記入していくことができる。たとえば if 文の場合引数の文のラムダ抽象を先に作成し、そのあとにボディの部分を記入する。

(= if )
(= if (lc.))
(= if (lc.(lx.)))
(= if (lc.(lx.(ly.))))
(= if (lc.(lx.(ly.( )))))
(= if (lc.(lx.(ly.(( ) y))))
(= if (lc.(lx.(ly((c x) y)))))

if を使うときは、引数が c, x, y の3つなので先頭に3つの括弧を置く。そうして引数を与えるたびに閉じ括弧で閉じる。

(((if
(((if ture)
(((if true) a)
(((if true) a) b)

NOT の定義を if 関数を利用して行うときは上のやり方を組み合わせて次のようにする。ユーザ定義のif 文は引数が3つなので、先頭に3つの括弧を記入する。

(= NOT )
(= NOT (lx.))
(= NOT (lx.(((if ))
(= NOT (lx.(((if x))
(= NOT (lx.(((if x) false)))
(= NOT (lx.(((if x) false) true)))

これらのルールで Y コンビネータのような複雑な項も記述が簡単になる。

(= Y )
(= Y (lf.))
(= Y (lf.(() ())))
(= Y (lf.((lx.) (lx.)))
(= Y (lf.((lx.(f ()) (lx.(f ())))))
(= Y (lf.((lx.(f (x x)) (lx.(f (x x))))))

実際にラムダ計算機で入力した結果は次のようになる。

lambda> (= true (lx.(ly.x)))
lambda> (= false (lx.(ly.y)))
lambda> (= if (lc.(lx.(ly.((c x) y))))
lambda> (= if (lc.(lx.(ly.((c x) y)))))
lambda> (((if true) a) b)
a
lambda> (= NOT (lx.(((if x) false) true)))
lambda> (NOT true)
(lx.(ly.y))
lambda> (= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))

このように、括弧の対応づけは要素的な項が現れるたびに行っておけば煩雑さを免れる。

by tnomura9 | 2019-09-27 08:08 | Haskell | Comments(0)

Li-sa-X, BABYMETAL, Kalafina

Li-sa-X
Li-sa-X 『リトル・ウイングス feat. YOYO』

BABYMETAL

Kalafina


by tnomura9 | 2019-09-26 21:24 | ボーカロイド | Comments(0)

ラムダ計算 Z - コンビネータ


JavaScript でラムダ式が簡単に記述できることがわかったが、Y - コンビネータは動かなかった。それは JavaScript の式の評価は値渡しで行われるので Y g = g (Y g) = g (g (Y g)) = ... と Y g の評価が無限に行われるからだ。しかし、前回の記事で、次のような Z - コンビネータを使うとうまく行くことを示した。

> Z = f => (x => f(y => x(x)(y)))(x => f(y => x(x)(y)))
[Function: Z]
> Z(f => n => n ? n * f(n-1) : 1) (5)
120

Z - コンビネータは Y - コンビネータに変数 y を付け加えただけだ。このプログの過去記事の 「Z - コンビネータ」にも説明記事を掲載している。

Y = (λf . (λx . f (x x)) (λx . f (x x)))
Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

そこで、ラムダ計算機でも Z - コンビネータを作ってみたら動作確認ができた。

lambda> (= Z (lf.((lx.(f (ly.((x x) y)))) (lx.(f (ly.((x x) y)))))))
lambda> ((Z g) 3)
(ls.(lz.(s (s (s (s (s (s z))))))))

括弧の多いラムダ計算機で Z - コンビネータを記述するのは結構大変だったので、設定ファイルの defined.txt に追加した。

ファイル名 defined.txt
(= true (lx.(ly.x)))
(= false (lx.(ly.y)))
(= NOT (lx.((x false) true))))
(= AND (lx.(ly.((x y) false)))))
(= OR (lx.(ly.((x true) y)))))
(= IMPLY (lx.(ly.((OR (NOT x)) y))))
(= 0 (ls.(lz.z)))
(= succ (lw.(ls.(lz.(s ((w s) z))))))
(= pred (ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x))))))
(= add (lx.(ly.((x succ) y))))
(= mult (lx.(ly.((x (y succ)) 0))))
(= 1 (succ 0))
(= 2 (succ 1))
(= 3 (succ 2))
(= 4 (succ 3))
(= 5 (succ 4))
(= 6 (succ 5))
(= 7 (succ 6))
(= 8 (succ 7))
(= 9 (succ 8))
(= isZero (lz.(((z false) NOT) false)))
(= pair (lx.(ly.(ls.((s x) y)))))
(= fst (lp.(p true)))
(= snd (lp.(p false)))
(= cons (la.(lb.(lf.((f a) b)))))
(= car (lx.(x true)))
(= cdr (lx.(x false)))
(= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))
(= g (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))
(= Z (lf.((lx.(f (ly.((x x) y)))) (lx.(f (ly.((x x) y)))))))

ちなみに、コンビネータって何という話になるが、これは単に body 部分の変数がすべてラムダ抽象による束縛変数しかないラムダ式のことだ。

また、Haskell の場合は、ラムダ記法で Y コンビネータを記述しようとしても型推定でエラーになってしまうが y x = x (y x) で関数 y を定義すると無名再帰関数を記述することができる。Y - コンビネータの本質が (Y g) = g (Y g) という不動点 (Y g) であることが分かる。

Prelude> y x = x (y x)
Prelude> y (\f n -> if n == 1 then 1 else n * f (n-1)) 5
120


by tnomura9 | 2019-09-26 04:22 | Haskell | Comments(0)

JavaScript の無名再帰


JavaScript でラムダ式が記述できるのがわかったので Y コンビネータで階乗の計算をしようと思ったが、何度やっても stack overflow になってできなかった。JavaScript では値渡しなので Y(g) = g (Y(g)) = g (g (Y(g)) = ... と無限に展開されてしまうからだ。りょうじさんのブログをのぞいたら次のように Z コンビネータを使ったらできるのがわかった。

> Z = f => (x => f(y => x(x)(y)))(x => f(y => x(x)(y)))
[Function: Z]
> Z(f => n => n ? n * f(n-1) : 1) (5)
120

ラムダ計算機の場合名前渡しなので、Y コンビネータが動いたらしい。ラムダ計算のモデルを Monad Transformers Step by Step から借用したのでそこまでは理解していなかった。プログラムの世界は奥が深い。

しかし、これで型なしラムダ計算が JavaScript で実験できることがわかった。表記もかなり簡潔だ。ラムダ計算のプログラミングスタイルが実用的なプログラムにも使えるのかもしれない。面白いことになってきた。

by tnomura9 | 2019-09-25 06:23 | Haskell | Comments(0)

JavaScript のラムダ式


JavaScript でラムダ式が使えるのを知った。実験するのにブラウザのコンソールも使えるが、Ubuntu で js を使ってみた。

$ js
> function add (x,y) {return x+y}
undefined
> add (2,3)
5
> addl = (x,y) => x+y
[Function: addl]
> addl (2,3)
5

=> を使うのでアロー記法とも呼ぶのだそうだが、関数の定義が随分コンパクトにできる。この方法だと無名関数が簡潔に書けるので map などの高階関数を使うのも快適にできる。

> array = [1,2,3]
[ 1, 2, 3 ]
> array.map (x => x*x)
[ 1, 4, 9 ]

実際はこれはラムダ記法の一種なので、ラムダ式を記述することもできる。たとえば恒等関数は次のようになる。

> id = x => x
[Function: id]
> id (5)
5
> id ("foo")
'foo'

チャーチ数も次のように定義できる。

> zero = s => z => z
[Function: zero]
> (zero (x => x*2)) (1)
1
> one = s => z => s(z)
[Function: one]
> (one (x => x*2)) (1)
2
> two = s => z => s(s(z))
[Function: two]
> (two (x => x*2)) (1)
4
> three = s => z => s(s(s(z)))
[Function: three]
> (three (x => x*2)) (1)
8

JavaScript で使えるとなるとラムダ計算の知識も無駄にならない。

by tnomura9 | 2019-09-25 00:04 | Haskell | Comments(0)

Graham Hutton

「Programming in Haskell」の著者 Graham Hatton 教授のビデオ講座



by tnomura9 | 2019-09-23 17:15 | Haskell | Comments(0)