Edited at

Lazy K プログラムを書く

More than 1 year has passed since last update.


Lazy K プログラムを書く

難読プログラミング言語 Lazy K でプログラムを書いてみたので、その時に学

んだことなどを記録しておきます。

λ計算を使いますが、紹介するので知らなくても読めます。

前提知識


  • 関数型プログラミングの基本的なアイデア (再帰、無名関数、高階関数など)


λ計算超入門


λ計算 is 何

Lazy K を理解するためには、λ計算を知っている必要があります。

λ計算は、簡単に言えば「めちゃめちゃシンプルな関数型言語」です。シンプ

ルすぎるので整数型もなければリスト型もありませんが、それでも十分な計算

能力があることが証明されています (あとでその片鱗を見ていきます)。

λ計算はそのシンプルさのために数学的に扱いやすく、プログラミング言語と

しては実用性がないものの、理論面の研究で利用されます。


λ計算の構文

λ計算にあるのは1引数の無名関数と関数呼び出しの2つだけです。ここでは

無名関数を次のように表現することにします:

\x.x [x を受け取って x をそのまま返す関数]

これはたとえば javascript 風に書けばこんな関数です:

function(x) { return x; }

関数呼び出しは、関数の右に引数を置くことで表現します:

f x [関数 f を引数 x で呼び出す]

たとえば、

(\x.x) y [受け取ったものをそのまま返す関数に y を渡す]

と関数呼び出しすると、その結果は

y

と等価です。

これらを組み合わせると、たとえばこんな関数も作れます:

\x.fx [x を受け取って、それを関数 f に渡した結果を返す関数]

ところで、この関数に登場した f の正体はこの関数の中に書かれていません。

このように、関数のどこか外で定義されている変数を 自由変数 と言います。

一方、 x は関数の引数だということが明らかになっているので、自由変数で

はありません。


2引数以上の関数を作る

λ計算には1引数関数しかないと書きましたが、次のように関数の中で関数を

作ることで、2引数関数(らしきもの)を作ることができます:

\f.(\x.fx) [f と x を受け取り、f に x を渡した結果を返す関数]

試しに引数を2つ与えてみます:

(\f.(\x.fx)) a b [上の関数に2つの引数 a, b を渡す]

^ ^ ^
= (\x.ax) b [外側の引数 f に a が渡る]
^ ^ ^
= ab [内側の引数 x に b が渡る]

これは次の javascript プログラムが動くのと同じ原理です。納得のいかない

方は実行してみると理解できるかもしれません:

the_function = function(f) { return function(x) { return f(x); }; };

the_function(alert)("hoge");

2引数以上の関数を書くとき、いちいち無名関数をネストするのは面倒なので、

次のように省略して書くことにします:

\w.(\x.(\y.z)) → \wxy.z


カリー化

λ計算の面白い性質の1つは、たとえば2引数関数に引数を1つだけ渡して呼

び出してもエラーにならず、たんに引数の一つ減った関数が返ってくるところ

です (なにしろ実体は1引数関数ですから……)。

(\xy.xy) a

= \y.ay

得られた1引数関数に残りの一つの引数を渡してやると、ついに結果が返って

きます。

(\y.ay) b

= ab

このような性質を「関数がカリー化されている」と言います。これは Haskell

Curry さんの名前からきていて、いかにも Haskell 言語の名前の由来になって

います。

名前はともあれ、このような性質があるということは知っておくと役に立ちま

す。


Lazy K とは


コンビネータ計算

λ計算はそれだけでもかなりシンプルな言語ですが、実はこれもさらにシンプ

ルにできることがわかっています。というのも、λ計算で書けるすべての無名

関数は、次の3つの関数の組み合わせで作ることができることがわかっている

のです:

S = \xyz.(xy)(yz)

K = \xy.x
I = \x.x

したがって、これらの3つの関数さえあれば、λ計算からさらに無名関数の構

文を取り除くことができます。これを コンビネータ計算 と言います。

たとえば、次のラムダ式:

\xy.yx

は無名関数を使わなくとも、 SKI の組み合わせで次のように表せます (なぜそ

うなるかはさておき、まずは表せるという事実に注目してください):

S(K(SI))K

Lazy K は、このコンビネータ計算でプログラムを書く言語です。


Lazy K のプログラム

Lazy K のプログラムは、 SKI の組み合わせで書かれた1つの関数です。この

関数は、自然数のリストを受け取って自然数のリストを返さなければなりませ

ん (ちょっと待って、λ計算に自然数とかリストなんてあった?→あとで紹介

します)。

Lazy K プログラムに渡される自然数のリストは、標準入力から受け取った文字

列の ASCII コードを並べたものです。返すべき自然数のリストは、標準出力に

表示したい文字列の ASCII コードを並べたものです。

たとえば、Lazy K の "Hello, World!" はこんな雰囲気の関数になります (標

準入力 x を受け取って、その内容にかかわらず "Hello, World!" を ASCII

コードのリストとして返す):

    H   e    l    l    o    ,   W   o    r    l    d    !   \n

\x.{72, 101, 108, 108, 111, 44, 87, 111, 114, 108, 100, 33, 10}

これを SKI の組み合わせに直してやれば立派な Lazy K プログラムになります。


自然数を表現する


そもそも自然数って何だ

そもそも自然数は、(すごーく簡単に言うと) 次のようなものとして定義できま

す:


  • 0 というものがあり、これは自然数である (1 とする人もいる)



  • どの自然数 N にも、 N の「一つ後ろの数」 (succ(N) と表現する)

    があり、これは自然数である


    • ただし succ は次の性質を満たす:


      1. succ(N)≠N である

      2. N≠M ならば succ(N)≠succ(M) である





実際、私たちがふだん自然数だと考えるあらゆるオブジェクトはこの定義に沿っ

て次のように表現することができますし、またこの定義に沿って表現できない

ものは自然数ではありません (詳しくは「ペアノの公理」で検索):

0 = 0

1 = succ(0)
2 = succ(succ(0))
3 = succ(succ(succ(0)))
...

ここから、自然数を表現するためにはオブジェクト 0 と、上の性質を満たす

ような関数 succ さえ定義してやればよいということがわかります。


チャーチエンコーディング

λ計算で自然数を構成する一つの方法が チャーチエンコーディング です。

まずはチャーチエンコーディングでどのように 0, succ を定義するのか見

てみます:

     0 = \fx.x

<succ> = \nfx.f(nfx)

この定義から、実際に自然数をいくつか作ってみます。

0 = \fx.x [0 の定義より]

1 = <succ> 0
= (\nfx.f(nfx)) \fx.x [succ, 0 の定義より]
^ ^ ^^^^^
= \fx.f((\fx.x)fx)
^ ^
= \fx.f((\x.x)x)
^ ^ ^
= \fx.fx

2 = <succ> 1
= (\nfx.f(nfx)) \fx.fx
^ ^ ^^^^^^
= \fx.f((\fx.fx)fx)
^ ^ ^
= \fx.f((\x.fx)x)
^ ^ ^
= \fx.f(fx)

3 = <succ> 2
= (\nfx.f(nfx)) \fx.f(fx)
^ ^ ^^^^^^^^^
= \fx.f((\fx.f(fx))fx)
^ ^ ^ ^
= \fx.f((\x.f(fx))x)
^ ^ ^
= \fx.f(f(fx))

ここからわかるのは、チャーチエンコーディングで表現された自然数 N は、

「関数 f とオブジェクト x を受け取って、 xfN 回適用す

る関数」だということです。

0 = \fx.x

1 = \fx.fx
2 = \fx.f(fx)
3 = \fx.f(f(x))
...
N = \fx.f(f(f....(f(x))))
^^^^^^^^^^^
N 個

関数 succ が定義の性質を満たすことは、証明をしなくても何となくわかり

ますね。


自然数の計算

せっかくなので、自然数の計算をする関数をいくつか作って、これがちゃんと

自然数として使えることを確認してみます。



  • 足し算

    <add> = \nm.n<succ>m
    

    msuccn 回適用すれば結果は n + m になります。




  • 掛け算

    <mul> = \nm.n(<add> m)0
    

    0<add> mn 回適用すれば結果は n * m になります。

    関数がカリー化されているので、2引数関数である add に引数を1つだけ

    (m) 渡すと、第2引数が保留された1引数関数「与えられた自然数に m

    を足す」が得られることを思い出してください。




  • 1減らす (succ の逆)

    <pred> = \nfx.n(\gh.h(gf))(\y.x)(\y.y)
    

    これは実行例を見ないとよくわからないかもしれません。

    <pred> 3 = (\nfx.n(\gh.h(gf))(\y.x)(\y.y)) 3 [pred の定義より]
    
    ^ ^ ^
    = \fx.3(\gh.h(gf))(\y.x)(\y.y)
    = \fx.((\gh.h(gf))((\gh.h(gf))((\gh.h(gf))(\y.x))))(\y.y) [3 の性質より]
    ^ ^ ^^^^^^
    = \fx.((\gh.h(gf))((\gh.h(gf))(\h.h((\y.x)f))))(\y.y)
    ^ ^
    = \fx.((\gh.h(gf))((\gh.h(gf))(\h.hx)))(\y.y)
    ^ ^ ^^^^^^^
    = \fx.((\gh.h(gf))(\h.h((\h.hx)f)))(\y.y)
    ^ ^ ^
    = \fx.((\gh.h(gf))(\h.h(fx)))(\y.y)
    ^ ^ ^^^^^^^^^^
    = \fx.(\h.h((\h.h(fx))f))(\y.y)
    ^ ^ ^
    = \fx.(\h.h(f(fx)))(\y.y)
    ^ ^ ^^^^^^
    = \fx.(\y.y)(f(fx))
    ^ ^ ^^^^^^^
    = \fx.f(fx) [= 2]

    最後だけ h\y.y になることで f が1つ減っています。自然数の

    範囲しか考えていないので、0はそれ以上小さくなりません。




  • 引き算

    <sub> = \nm.m<pred>n
    

    pred が実装できてしまえば引き算は簡単です。 npredm

    適用すれば結果は n - m になります。 pred の仕様から、引かれる数よ

    りも引く数が大きい場合には0となりマイナスにはなりません。




リストを表現する


ペア

リストの表現を考える前に、まずは2つのオブジェクトのペア (順序対) の表

現を考えます。

ペアは、次のような性質をもったオブジェクトです:


  • ペアは、2つのオブジェクトを合体させて作ることができる


  • ペアからは、そのペアを作るために使った2つのオブジェクトをそれぞれ取

    り出すことができる


ここでは、2つのオブジェクトからペアを作る関数を cons 、ペアから1つ

目のオブジェクトを取り出す関数を car 、2つ目のオブジェクトを取り出

す関数を cdr と呼ぶことにします。

たとえばこれらの関数は、次のように使うことができます:

<car>(<cons> a b) = a [a, b のペアから1つ目を取り出す]

<cdr>(<cons> a b) = b [a, b のペアから2つ目を取り出す]
(\p.<add>(<car> p)(<cdr> p)) (<cons> 1 2) = 3 [ペア内の自然数の和を計算]

ペアを表現する一つの方法は スコットエンコーディング です。スコットエ

ンコーディングでは、これら3つの関数を次のように定義します:

<cons> = \abf.fab

<car> = \p.p(\xy.x)
<cdr> = \p.p(\xy.y)

念のため、この定義で本当にペアが作れることを確認しておきます。

<car> (<cons> a b) = <car> ((\abf.fab) a b) [cons の定義]

^^ ^^ ^^^
= <car> \f.fab
= (\p.p(\xy.x)) \f.fab [car の定義]
^ ^ ^^^^^^
= (\f.fab) \xy.x
^ ^ ^^^^^
= (\xy.x) a b
= a

<cdr> (<cons> a b) = <cdr> ((\abf.fab) a b) [cons の定義]
^^ ^^ ^^^
= <cdr> \f.fab
= (\p.p(\xy.y)) \f.fab [cdr の定義]
^ ^ ^^^^^^
= (\f.fab) \xy.y
^ ^ ^^^^^
= (\xy.y) a b
= b

チャーチエンコーディングとスコットエンコーディングの違いなどはここでは

触れません。


リスト

リストは任意の個数のオブジェクトを並べたもので、その好きな要素に自由に

アクセスすることができます。ぴったり2つの要素を持つ順序対と異なり、リ

ストにいくつの要素が含まれているかはわかりません。

自然数を次のように定義したように:


  • 0 は自然数である

  • ある自然数に1を足したものも自然数である

リストはふつう、次のように定義します:


  • 空リスト {} はリストである

  • あるリストに要素を一つ足したものもリストである

考えてみると、「リスト L に要素 x を足したリスト」オブジェクトは次

の2つの情報をロスなく保持するものです:要素を足す前のリスト L と、足

された要素 x 。これにはいかにも、上で作ったペアが使えそうです。

スコットエンコーディングでは、リストに要素を足す関数として上で作った

cons を、また空リスト {} として次の定義を使います (なぜ {} をこの

ように定義しておくと便利かは、後でわかります):

{} = \fxy.x

たとえば 1 のみからなるリストは、空リスト {} に要素 1 を追加した

ものなので次のように表現できます:

{1} = <cons> 1 {}

同様に:

      {1} =                     <cons> 1 {}

{2, 1} = <cons> 2 (<cons> 1 {})
{3, 2, 1} = <cons> 3 (<cons> 2 (<cons> 1 {}))
...

リストの実体はペアなので、 car で先頭要素を取り出すことができます。

<car> {3, 2, 1} = 3

また cdr で先頭要素を取り除いたリストを得ることができます:

<cdr> {3, 2, 1} = {2, 1}

これを利用すると、リストの好きな要素にアクセスすることができます:

  <car> {3, 2, 1}

= 3

<car> (<cdr> {3, 2, 1})
= <car> {2, 1}
= 2

<car> (<cdr> (<cdr> {3, 2, 1}))
= <car> (<cdr> {2, 1})
= <car> {1}
= 1


ついに "Hello, World!"


T[]-変換

いよいよλ計算で自然数・リストを作れるようになったので、あとはλ計算の

関数を SKI の組み合わせに直す方法さえわかれば "Hello, World!" を動かす

ことができます。

λ計算の関数は T[] と呼ばれる変換で SKI の組み合わせに直すことができま

す。 T[] は以下のように定義されます:

1.          T[x] → x (x は変数) ...変数の処理

2. T[E1 E2] → T[E1] T[E2] ...関数適用の処理
3. T[\x.E] → K T[E] (x は E の自由変数でない) ...定数関数を K に直す
4. T[\x.x] → I ...恒等関数を I に直す
5. T[\xy.E] → T[\x.T[\y.E]] ...2引数以上の関数の処理
6. T[\x.(E1 E2)] → S T[\x.E1] T[\x.E2] ...引数の分配を S に直す

試しに簡単な関数を変換してみます。

T[\xy.yx]

= T[\x.T[\y.yx]] [ルール 5]
= T[\x.S T[\y.y] T[\y.x]] [ルール 6]
= T[\x.S T[\y.y] (K T[x])] [ルール 3]
= T[\x.S T[\y.y] (K x)] [ルール 1]
= T[\x.S I (K x)] [ルール 4]
= S T[\x.S I] T[\x.K x] [ルール 6]
= S T[\x.S I] (S T[\x.K] T[\x.x]) [ルール 6]
= S T[\x.S I] (S T[\x.K] I) [ルール 4]
= S T[\x.S I] (S (K K) I) [ルール 3]
= S (K (S I)) (S (K K) I) [ルール 3]

このルールに従って、"Hello, World!":

    H   e    l    l    o    ,   W   o    r    l    d    !   \n

\x.{72, 101, 108, 108, 111, 44, 87, 111, 114, 108, 100, 33, 10}

を変換すると、次のようになります (手動で変換するのは困難なので、変換を

するプログラムを書くのがおすすめです。自分の書いた Prolog プログラムは

ここ にあります):

K(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(

K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(
I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))
(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(K(I))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(K(I))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))))))
)))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)
)))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K
(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K
))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S
(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))
(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(S(S(K(S))(K))(S(S(K(S))(K))(K(I))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)
))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))))))))))))))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))(S(S(K(S))(S(
K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(
S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(
I)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
)))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S(S(K(S))(K)
)(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(
K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(
S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))))))))
))))))))))))))))))))))))(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))(S(S(K(S))(K))(S
(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S
))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I))))))))))))(K(K))))))))))))))))

Lazy K 処理系にこのプログラムを渡せば、確かに "Hello, World!" が表示さ

れることがわかります (Lazy K プログラムの実行には、オンラインの REPL

便利です)。


条件分岐


真偽値と if 文

真偽値と if 文は、ペアとほとんど同じ考え方で作ることができます:

   <if> = \ctf.ctf

<true> = \xy.x [= <car>]
<false> = \xy.y [= <cdr>]

試してみます:

<if> <true> 1 2 = (\ctf.ctf) <true> 1 2 [if の定義]

= <true> 1 2
= (\xy.x) 1 2 [true の定義]
= 1

<if> <false> 1 2 = (\ctf.ctf) <false> 1 2 [if の定義]
= <false> 1 2
= (\xy.y) 1 2 [false の定義]
= 2

「これでは then 節と else 節が両方実行されてしまう場合がないか?」と考

えた人がいるかもしれません。実は、Lazy K はその名の通り "Lazy

Evaluation" (遅延評価) という実行の戦略を取っていて、式のうち最終結果に

影響を及ぼさない部分は計算しないようにできています。よって、これできち

んと (計算量的にも) if 文として機能します。


述語

truefalse しかないのはちょっと寂しいので、オブジェクトの性質を

調べる関数 (述語) をいくつか実装します。



  • 自然数が 0 かどうか調べる

    <iszero> = \n.n(\x.<false>)<true>
    

    引数が何であれ false を返す関数 \x.<false>truen 回適

    用します。引数が 0 であれば true がそのまま返りますが、それ以外の

    場合には1回以上 \x.<false> が適用されて false が返ります。




  • リストが空リスト {} かどうか調べる

    <isnull> = \l.l(\xy.<false>)
    

    {}\fxy.x すなわち \f.<true> と定義されていたので、

    <isnull> {} は明らかに true です。空でないリストの場合、 cons

    の定義より \f.f<第1要素><第1要素を除いたリスト> という格好をして

    いるはずなので、 <isnull> <空でないリスト> の結果は false です。




再帰呼び出し


再帰呼び出し

複雑なプログラムを書くには再帰呼び出し (またはループ) が必要不可欠です。

しかし、λ計算で再帰呼び出しを表現する方法はさほど自明ではありません

(なにしろ、λ計算の関数には名前がありません……)。

ここでは、「Y コンビネータ」と呼ばれる特別な関数を利用して再帰呼び出し

を実現してみます。


Y コンビネータ

ある関数 f に対して、

f x = x

となるような xf の不動点と言います。関数 f に対してその不動点

x を求めることができれば、次のように再帰的な構造を作ることができます:

x = f x             [x は f の不動点なので]

= f (f x) [同]
= f (f (f x)) [同]
= f (f (f (f x))) [同]
= ...

ラッキーなことに、実はどんなλ計算の関数にも不動点があることがわかって

いて、しかもそれは次の関数 (Y コンビネータ) で簡単に求めることができま

す:

<fix> = \f.(\x.f(xx))(\x.f(xx))

実際、 fix に関数 F を渡すと次の式 X が得られますが:

X = <fix>F

= (\f.(\x.f(xx))(\x.f(xx))) F [fix の定義]
^ ^ ^ ^
= (\x.F(xx))(\x.F(xx))

これは確かに F の不動点になっています:

X = (\x.F(xx))(\x.F(xx))

^ ^^ ^^^^^^^^^^
= F((\x.F(xx))(\x.F(xx)))
= FX [X の定義]
∴ FX = X

まとめると、Y コンビネータ fix には次のような性質があると言えます:

<fix> f = f (<fix> f)

^^^^^^^ ^^^^^^^^^


不動点を使った再帰呼び出し

Y コンビネータを使うと、次のように再帰的な関数をλ計算の範疇で表現する

ことができます:

/* n の階乗を求める */

<fact> = <fix> <factfn>
<factfn> = \fn.<if>(<iszero> n)1(<mul> n (f(<pred> n)))

実際に展開してみます:

  <fact> n

= <fix> <factfn> n [fact の定義]
= <factfn> (<fix> <factfn>) n [fix の性質]
= <factfn> <fact> n [fact の定義]
= (\fn.<if>(<iszero> n)1(<mul> n (f(<pred> n)))) <fact> n [factfn の定義]
^ ^ ^^^^^^
= (\n.<if>(<iszero> n)1(<mul> n (<fact> (<pred> n)))) n
^ ^ ^ ^ ^
= <if>(<iszero> n)1(<mul> n (<fact> (<pred> n)))

factfn の第1引数に再び fact が渡ることで、確かに再帰的に fact

が呼び出されています。


自然数を表示する


自然数を表示する

いよいよ色々な計算ができるようになってきたので、最後に、計算結果の自然

数を画面に表示することを考えます。

標準出力になにかを出力するためには「ASCII コードのリスト」を作らなけれ

ばならないのでした。そこで、ここでは「自然数を ASCII コードのリストに変

換する関数」を作ることにします。

目的の関数は、次のような方針で作れそうです (※48 は '0' の ASCII コー

ド):

to_str n = reverse (f n);

f n = cons (n%10+48) (if (n <= 9) then {} else f (n/10));

to_str 123 = reverse (f 123)
= reverse (cons (3+48) f(12))
= reverse (cons (3+48) (cons (2+48) f(1)))
= reverse (cons (3+48) (cons (2+48) (cons (1+48) {})))
= reverse {3+48, 2+48, 1+48}
= {1+48, 2+48, 3+48}

これを実装するために足りなさそうな reverse, <=, /, % をまずは実

装していきます。



  • リストを反転する reverse

      <reverse> = \rl.<reversefn>l{}
    
    <reversefn> = <fix>(\fab.<if> (<isnull> a) b (f (<cdr>a) (<cons> (<car>a) b)))

    reversefn が次のような動きをする補助関数で、

    <reversefn> {1, 2, 3} {} = <reversefn> {2, 3} {1}   [左の要素を右に移す]
    
    = <reversefn> {3} {2, 1} [左の要素を右に移す]
    = <reversefn> {} {3, 2, 1} [左の要素を右に移す]
    = {3, 2, 1} [左が空になったら右を返す]

    reverse が第2引数の {} を補ってこれを呼び出しています。




  • 大小比較 le (<=)

    <le> = \nm.<iszero>(<sub>nm)
    

    n <= m のとき <sub>nm0 になります。




  • 割り算 div (/)

    <div> = <fix> (\fnm.<if> (<le> m n) (<succ> (f (<sub> n m) m)) 0)
    

    割る数 m が割られる数 n より小さい (か等しい) なら割り算の結果は

    1 + (n - m) / m ですし、そうでなければ結果は 0 です。




  • 剰余 mod (%)

    <mod> = <fix> (\fnm.<if> (<le> m n) (f (<sub> n m) m) n)
    

    割る数 m が割られる数 n より小さい (か等しい) なら、割り算の余り

    n - m を割ったときの余りに等しくなります。そうでなければ n

    まるまる余ります。



これらを使って、お目当ての to_str は次のように実装できます:

<to_str> = \x.<reverse>(<to_str_1> x)

<to_str_1> = <fix> (\fx.<cons> (<add> (<mod> x 10) 48) (<if> (<le> x 9) {} (f (<div> x 10))))



ちょっとした計算をして、その結果を表示する Lazy K プログラムの例を載せ

ておきます。実際に実行できることを確認してみてください。

\x.<to_str>(<fact> 5)

SKI に変換すると

K(S(K(S(S)(K(K(K(K))))(S(S(S(K(S))(K))(K(S(I)(I))))(S(S(K(S))(K))(K(S(I)(I))))(S(K(S(S(K(S

))(S(K(I))(S(I)(K(K(K(K(I))))))))))(S(S(K(S))(S(K(S(K(S))))(S(K(S(K(K))))(S(S(K(S))(K))(K(
S(I)(K(K(I)))))))))(K(S(K(S(S(K(S))(S(K(K))(S(K(S))(S(K(S(I)))(K)))))(K(K))))(S(I)(K(K))))
))))))(S(S(S(K(S))(K))(K(S(I)(I))))(S(S(K(S))(K))(K(S(I)(I))))(S(K(S(S(K(S(S(K(S))(S(K(K))
(S(K(S))(S(K(S(I)))(K)))))(K(K))))(S(S(K(S(I)(K(S(S(K(S))(K))))))(S(S(S(S(K(S))(K))(K(S(I)
(I))))(S(S(K(S))(K))(K(S(I)(I))))(S(S(K(S))(S(K(S(K(S))))(S(K(S(S(K(S))(S(K(S(K(I))))(S(K(
S(K(S(S(I)(K(K(K(I)))))(K(K))))))(S(K(S(S(K(S(S(I)(K(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S(K
(S(K(S))))(S(K(S(K(K))))(S(S(K(S))(K))(K(S(K(S(K(S(I)))))(S(K(S(K(K))))(S(K(S(I)))(K))))))
)))(K(K(K))))))(K(K(K(I)))))))))(K))))(K)))))))(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S(K(K))(
S(K(S))(K))))(K(S(K(S(S(I)(K(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S(K(S(K(S))))(S(K(S(K(K))))
(S(S(K(S))(K))(K(S(K(S(K(S(I)))))(S(K(S(K(K))))(S(K(S(I)))(K)))))))))(K(K(K))))))(K(K(K(I)
))))))))(K))))))(K(K(I)))))))(K(K))))(K(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S)
)(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(
K(I)))))))))))))))(K(S(S(K(S))(S(S(K(S))(K))(K(S(I)(K(S(S(K(S))(K))))))))(K(K(K(I))))(S(S(
K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))(S(S(I)(I))(I)(S(S(K(S))(K))(S(S(K(S))(K))(K
(I)))))))))))(S(K(S(S(S(K(I))(S(S(K(S(S(K(S(K(S(S(I)(K(K(K(I)))))(K(K))))))(S(K(S(S(K(S(S(
I)(K(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S(K(S(K(S))))(S(K(S(K(K))))(S(S(K(S))(K))(K(S(K(S(K
(S(I)))))(S(K(S(K(K))))(S(K(S(I)))(K)))))))))(K(K(K))))))(K(K(K(I)))))))))(K))))(K)))))(K)
)(K(S(S(K(S))(S(K(S(I)))(S(K(K))(S(S(K(S))(S(S(K(S))(K))(K(S(I)(K(S(S(K(S))(K))))))))(K(K(
K(I))))))))(K(K(S(S(K(S))(K))(K(I)))))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I)))))(
S(S(K(S))(K))(S(S(K(S))(K))(K(I))))))))(K(K(K))))))(S(S(K(S))(K))(K(S(S(S(S(K(S))(K))(K(S(
I)(I))))(S(S(K(S))(K))(K(S(I)(I))))(S(S(K(S))(S(K(S(K(S))))(S(K(S(S(K(S))(S(K(S(K(I))))(S(
K(S(K(S(S(I)(K(K(K(I)))))(K(K))))))(S(K(S(S(K(S(S(I)(K(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S
(K(S(K(S))))(S(K(S(K(K))))(S(S(K(S))(K))(K(S(K(S(K(S(I)))))(S(K(S(K(K))))(S(K(S(I)))(K))))
)))))(K(K(K))))))(K(K(K(I)))))))))(K))))(K)))))))(S(K(S(K(S(K(S(S(K(S))(K))))))))(S(S(K(S)
)(S(K(S(K(S))))(S(S(K(S))(S(K(K))(S(K(S))(K))))(K(S(K(S(S(I)(K(S(S(K(S))(S(K(S(K(S))))(S(S
(K(S))(S(K(S(K(S))))(S(K(S(K(K))))(S(S(K(S))(K))(K(S(K(S(K(S(I)))))(S(K(S(K(K))))(S(K(S(I)
))(K)))))))))(K(K(K))))))(K(K(K(I)))))))))(K))))))(K(K(I))))))))(K(K(K(K(I)))))))(K(S(S(K(
S))(S(S(K(S))(K))(K(S(I)(K(S(S(K(S))(K))))))))(K(K(K(I))))(S(S(K(S))(K))(S(S(K(S))(K))(K(I
))))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(K(I))))))))))))
)))(S(S(S(K(S))(K))(K(S(I)(I))))(S(S(K(S))(K))(K(S(I)(I))))(S(K(S(S(S(K(I))(S(S(I)(K(K(K(I
)))))(K(K))))(K(S(S(K(S))(K))(K(I)))))))(S(K(S(S(S(K(S))(S(S(K(S))(K))(K(S(I)(K(S(S(K(S))(
K))))))))(K(K(K(I)))))))(S(S(K(S))(K))(K(S(S(K(S))(S(K(S(K(S))))(S(S(K(S))(S(K(S(K(S))))(S
(K(S(K(K))))(S(S(K(S))(K))(K(S(K(S(K(S(I)))))(S(K(S(K(K))))(S(K(S(I)))(K)))))))))(K(K(K)))
)))(K(K(K(I)))))))))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))(S(S(K(S))(K))
(K(I)))))))))