人気ブログランキング |

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)

ラムダ計算

Parsec の練習としてラムダ計算を行うインタープリタを作ったが、テストで使っていて、ラムダ計算自身にプログラム言語としての面白さがあるのではないかと感じるようになってきた。そこで、ラムダ計算の記事リストを作ることにする。ラムダ計算についてはほとんど知らないので、このリストについては拡充する予定だ。

ラムダ計算機 Ver 0.1

テキストファイルにコピペして、エディタでアンダースコア2つのパターンを全てスペース2つのパターンに置き換えれば、runghc で起動したり、ghc でコンパイルできる。以下の記事では全てこのインタープリタを使ってラムダ計算プログラムを実行できる。


ラムダ計算



# by tnomura9 | 2019-09-22 20:29 | Haskell 記事リスト | Comments(0)

パプリカ

Foorin


米津玄師


まにこ


上白石萌香




サビのところで元気になるが、全体に美しい旋律。色々な解釈ができそう。

# by tnomura9 | 2019-09-22 19:16 | ボーカロイド | Comments(0)

まにこ

米津玄師の「Lemon」を学園祭で歌っていた女子高生の YouTube サイト


癒される。


インタビュー記事


デビューシングル(H△G とのコラボ)


コラボ


twitter


# by tnomura9 | 2019-09-19 14:29 | ボーカロイド | Comments(0)

Lemon

米須玄帥の「Lemon」はいろいろなカバーが YouTube で聞けて楽しい。

本人

女子高生

GIRLFRIEND

Raon Lee

MELOGAPPA

マトリョーシカ

# by tnomura9 | 2019-09-16 15:51 | ボーカロイド | Comments(0)

ラムダ計算 再帰


ラムダ計算機でどうしてもやりたかったのが、Y コンビネータを使った再帰関数の記述だ。これを手入力で試すのは結構大変なので、次のような関数の定義ファイル defined.txt を作成して、ラムダ計算機 Ver 0.1 の :load コマンドで読み込んで検証することにする。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)))))))

これらの関数のうちで再帰関数に使うのが、

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

という Y コンビネータだ。この関数を β 簡約するともとの関数に戻ってしまうので β 簡約が永遠に終わらない。こんなもの何になるかと思うが Y の引数に関数 g を取ると次の用な関係が成り立つ。

(Y g) = g (Y g)

ここで g が関数 f と自然数 n を引数に取る場合、

(Yg) n = g (Yg) n = n * ((Yg) (n-1)) = n* ( n * (g (Y g) (n-1)) = n * (n-1) * ((Y g) (n-2)) = n * (n-1) * (g (Yg) (n-2)) = ... = n * (n-1) * ... * 2 * 1 * (g (Y g) 0) = n * (n-1) * ... * 2 * 1 * 1

というような再帰関数を記述することができる。

実行例は次のようになる。

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

コンソールから Y だけを入力すると (f (f ... といつまでも f を出力し続ける。コントロール+C で停止させないといけないがラムダ計算機自体も終了してしまう。

lambda> Y
(lf.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (

ラムダ計算機を再起動して (Y h) と入力すると今度は f が全て h に変わっている。(Y h) は束縛変数の f を h に置き換えるだけだから当たり前だが。(Y h) = h (h (h (h (Y h) .... と関数 h の再帰が延々と続いている。

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> (Y h)
(h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h

ところで、関数 g についてだが、これは関数 f と 自然数 n の2つを引数に取る。

g = (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))

つまり、g は束縛変数の f に何かの関数を n に自然数 n を割り当てると、n が 0 のときには 1 を返し、それ以外の n のときは n * (f (n-1)) を返す。上の関数を読みやすく書き換えると次のようになる。

g f n = if n == 0 then 1 else n * (f (n-1))

何のことはない階乗の定義だ。これを Y コンビネータの引数にすると、

g (Y g) n
= g (g (g (g ( ... (g (Y g) 0)...))))
= g (g (g (g ( ... (1) ... ))))
= g (g (g (g ( ... (2 * 1) ... ))))
= g (g (g (g ( ... (3 * 2 * 1) ... ))))
= n * (n-1) * ... * 2 * 1

となって n の階乗が計算できる。Y の関数としての機能は関数 g に再帰を提供することだった。ただ、ラムダ計算の驚くべきところは、これらの計算が変数の置き換えだけで実現できているということだ。つまり関数適用 (f x) と言ってもラムダ式 f の中の束縛変数をラムダ式 x で置き換えるだけなのだ。そうして置き換えられたラムダ式は新しい文字列(ラムダ式)に変わるだけだ。

上のプログラムではいかにも自然数の階乗が計算できたように見えるが、その実、新しいラムダ式が生成されたに過ぎない。ラムダ計算機はこのラムダ式の置き換えという統語論的な操作を自動化しているだけなのだ。しかし、その文字列の操作に対しチャーチ数などの意味を与えることで、階乗の計算のような複雑なプログラムとして解釈することができる。

しかし、これはラムダ式に限ったことではなく、プログラム言語は全てがそうだ。プログラム言語といってもその実、最終的にビット列に翻訳され、そのビット列が別のビット列に自動変換されるだけなのだ。ラムダ計算はその文法が単純なゆえに、このようなコンピュータ・プログラムの実体を明らかにしてくれる。

Y コンビネータの詳しい仕組みについては、「ラムダ計算をちょっと勉強したので忘れないうちに書いておく」というサイトで説明されている。

この記事では、とにかくラムダ計算機 Ver 0.1 でも Y コンビネータとそれを使った再帰関数が記述できるということを検証してみた。

Text.Parsec の使い方から始まって、Parsec のソースコードの解読。Monad Transformers Step by Step の解読、ラムダ計算機のプログラムというように、プログラム言語の作り方を調べてきたが、これで一応区切りをつける。非常に簡単なプログラム言語だが、ラムダ計算機はプログラム言語のインタープリタとして働く。トイプログラムだが、夢だったプログラム言語のインタープリタの記述ができたので自己満足。しかし、ちょっと疲れてきたのでプログラムネタはしばらくお休みにする。

# by tnomura9 | 2019-09-14 23:46 | Haskell | Comments(0)