More than 3 years have passed since last update.

Lazy K プログラムを書く

Last updated at 2020-09-24Posted at 2015-10-03

おしらせ：長い記事は本形式になっていた方が読みやすそうなので、 Zenn にお引越ししてみました。ここにも記事は残しておきますが、最新版はあちらになります。

1. Lazy K プログラムを書く

Lazy K プログラムを書く

難読プログラミング言語 Lazy K でプログラムを書いてみたので、その時に学
んだことなどを記録しておきます。

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

前提知識

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

λ計算超入門

λ計算 is 何

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

λ計算は、簡単に言えば「めちゃめちゃシンプルな関数型言語」です。シンプ
ルすぎるので整数型もなければリスト型もありませんが、それでも十分な計算
能力があることが証明されています (あとでその片鱗を見ていきます)。

λ計算はそのシンプルさのために数学的に扱いやすく、プログラミング言語と
しては実用性がないものの、理論面の研究で利用されます。

λ計算の構文

λ計算にあるのは１引数の無名関数と関数呼び出しの２つだけです。ここでは
無名関数を次のように表現することにします：

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

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

function(x) { return x; }

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

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

たとえば、

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

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

と等価です。

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

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

ところで、この関数に登場した f の正体はこの関数の中に書かれていません。
このように、関数のどこか外で定義されている変数を 自由変数 と言います。
一方、 x は関数の引数だということが明らかになっているので、自由変数で
はありません。

２引数以上の関数を作る

λ計算には１引数関数しかないと書きましたが、次のように関数の中で関数を
作ることで、２引数関数（らしきもの）を作ることができます：

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

試しに引数を２つ与えてみます：

(\f.(\x.fx)) a b [上の関数に２つの引数 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");

２引数以上の関数を書くとき、いちいち無名関数をネストするのは面倒なので、
次のように省略して書くことにします：

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

カリー化

λ計算の面白い性質の１つは、たとえば２引数関数に引数を１つだけ渡して呼
び出してもエラーにならず、たんに引数の一つ減った関数が返ってくるところ
です (なにしろ実体は１引数関数ですから……)。

(\xy.xy) a
= \y.ay

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

(\y.ay) b
= ab

このような性質を「関数がカリー化されている」と言います。これは Haskell
Curry さんの名前からきていて、いかにも Haskell 言語の名前の由来になって
います。

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

Lazy K とは

コンビネータ計算

λ計算はそれだけでもかなりシンプルな言語ですが、実はこれもさらにシンプ
ルにできることがわかっています。というのも、λ計算で書けるすべての無名
関数は、次の３つの関数の組み合わせで作ることができることがわかっている
のです：

S = \xyz.(xy)(yz)
K = \xy.x
I = \x.x

したがって、これらの３つの関数さえあれば、λ計算からさらに無名関数の構
文を取り除くことができます。これを コンビネータ計算 と言います。

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

\xy.yx

は無名関数を使わなくとも、 SKI の組み合わせで次のように表せます (なぜそ
うなるかはさておき、まずは表せるという事実に注目してください)：

S(K(SI))K

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

Lazy K のプログラム

Lazy K のプログラムは、 SKI の組み合わせで書かれた１つの関数です。この
関数は、自然数のリストを受け取って自然数のリストを返さなければなりませ
ん (ちょっと待って、λ計算に自然数とかリストなんてあった？→あとで紹介
します)。

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 を受け取って、 x に f を N 回適用す
る関数」だということです。

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
```
m に succ を n 回適用すれば結果は n + m になります。
掛け算
```
<mul> = \nm.n(<add> m)0
```
0 に <add> m を n 回適用すれば結果は n * m になります。

関数がカリー化されているので、２引数関数である add に引数を１つだけ
(m) 渡すと、第２引数が保留された１引数関数「与えられた自然数に m
を足す」が得られることを思い出してください。

１減らす (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 が１つ減っています。自然数の
範囲しか考えていないので、０はそれ以上小さくなりません。

引き算
```
 = \nm.m<pred>n
```
pred が実装できてしまえば引き算は簡単です。 n に pred を m 回
適用すれば結果は n - m になります。 pred の仕様から、引かれる数よ
りも引く数が大きい場合には０となりマイナスにはなりません。

リストを表現する

ペア

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

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

ペアは、２つのオブジェクトを合体させて作ることができる
ペアからは、そのペアを作るために使った２つのオブジェクトをそれぞれ取
り出すことができる

ここでは、２つのオブジェクトからペアを作る関数を cons 、ペアから１つ
目のオブジェクトを取り出す関数を car 、２つ目のオブジェクトを取り出
す関数を cdr と呼ぶことにします。

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

<car>(<cons> a b) = a [a, b のペアから１つ目を取り出す]
<cdr>(<cons> a b) = b [a, b のペアから２つ目を取り出す]
(\p.<add>(<car> p)(<cdr> p)) (<cons> 1 2) = 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

チャーチエンコーディングとスコットエンコーディングの違いなどはここでは
触れません。

考えてみると、「リスト L に要素 x を足したリスト」オブジェクトは次
の２つの情報をロスなく保持するものです：要素を足す前のリスト 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]] ...２引数以上の関数の処理
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 文として機能します。

述語

true と false しかないのはちょっと寂しいので、オブジェクトの性質を
調べる関数 (述語) をいくつか実装します。

自然数が 0 かどうか調べる
```
<iszero> = \n.n(\x.<false>)<true>
```
引数が何であれ false を返す関数 \x.<false> を true に n 回適
用します。引数が 0 であれば true がそのまま返りますが、それ以外の
場合には１回以上 \x.<false> が適用されて false が返ります。
リストが空リスト {} かどうか調べる
```
<isnull> = \l.l(\xy.<false>)
```
{} が \fxy.x すなわち \f.<true> と定義されていたので、
<isnull> {} は明らかに true です。空でないリストの場合、 cons
の定義より \f.f<第１要素><第１要素を除いたリスト> という格好をして
いるはずなので、 <isnull> <空でないリスト> の結果は false です。

再帰呼び出し

複雑なプログラムを書くには再帰呼び出し (またはループ) が必要不可欠です。
しかし、λ計算で再帰呼び出しを表現する方法はさほど自明ではありません
(なにしろ、λ計算の関数には名前がありません……)。

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

Y コンビネータ

ある関数 f に対して、

f x = x

となるような x を f の不動点と言います。関数 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 の第１引数に再び 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 が第２引数の {} を補ってこれを呼び出しています。

大小比較 le (<=)
```
<le> = \nm.<iszero>(nm)
```
n <= m のとき nm は 0 になります。
割り算 div (/)
```
<div> = <fix> (\fnm.<if> (<le> m n) (<succ> (f ( n m) m)) 0)
```
割る数 m が割られる数 n より小さい (か等しい) なら割り算の結果は
1 + (n - m) / m ですし、そうでなければ結果は 0 です。
剰余 mod (%)
```
<mod> = <fix> (\fnm.<if> (<le> m n) (f ( 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)))))))))

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up

Lazy K プログラムを書く

Table of Contents

Lazy K プログラムを書く

λ計算超入門

λ計算 is 何

λ計算の構文

２引数以上の関数を作る

カリー化

Lazy K とは

コンビネータ計算

Lazy K のプログラム

自然数を表現する

そもそも自然数って何だ

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

自然数の計算

リストを表現する

ペア

リスト

ついに "Hello, World!"

T[]-変換

条件分岐

真偽値と if 文

述語

再帰呼び出し

再帰呼び出し

Y コンビネータ

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

自然数を表示する

自然数を表示する

例