型なしラムダ計算、コンビネータ、アンラムダおよびフィボナッチ数

以下は、私の意見では、筋金入りのプログラミング方法についての話です。
投稿の主題は簡単ではありません。パスは長くなります。最後にCookieとして、Unlambdaでフィボナッチ数を数える方法を説明します。

目利きの場合：記事は、厳密に正式な説明をするよりも、その仕組みを説明する可能性が高くなります。

λ-calculusは、アルゴリズムと計算可能性の概念を形式化するためにAlonzo Churchによって発明されました。 λ計算の関数は、このように理解する必要があります-入力データを処理する特定のアルゴリズムとして。

型なしのλ計算

単一の引数の関数があるとします。 さらに、引数と戻り値の両方が1つの引数の関数でもあります。

ここで、数学者は異議を唱えます：それ自体からそれ自体への関数のセットと一致するセットを取得します。これはセット理論にはありません（無限セットの場合でも、関数のセットは厳密に大きいです）。 しかし、これはアメリカのスコットが部分的に順序付けられたセットに特別なトポロジーを導入することでデカルト閉カテゴリーを構築することを妨げませんでした。 提示されたオブジェクトは存在しますが、これはまったく別の話です。

したがって、手元にあるこのような抽象的で無限の奇妙な関数のセットだけで何ができるのでしょうか？ そもそも、これらの関数の書き方を決めておくといいでしょう。 λ計算では、次の規則が採用されます。

• fとaをいくつかの関数とします。 次に、 faは、関数fの関数aへの適用、またはλ計算の用語ではアプリケーションです 。
• Fを 、変数xを自由に含む式、またはまったく含まない式とします。 λx.Fは、値が式Fで与えられる変数xの関数を表し、これはλ抽象化と呼ばれます。

次に、この関数は引数xを取り、値fxを返すため、 λx.fx= fです。これは、関数f自体が行うことです。 これはη変換と呼ばれます。

たとえば、 λx.x2は²乗関数であり、 （λx.x2）3はこの関数の引数3への適用です。直観では、この式の値は9であり、これはλ計算の唯一の公理であり、 β-削減 ：

• （λx.F）a = F [x：= a]

ここで、 F [x：= a]は式Fを意味し、 xの代わりにaが使用されます。 この公理とともに、 λ計算はチューリング完全なプログラミング言語になります。 任意のアルゴリズムを実装できます（アルゴリズムが何であるかの合理的な意味で）。 自然な疑問が生じます-どうやって？

引数を単に返すアイデンティティ関数をスケッチするのは簡単です： λx.x
定数関数も複雑さを引き起こしません： λx.c 、ここでcはxから独立しています。 実際、どの引数に対しても、関数はcを返します 。
それがすべてのようです。 いくつかの引数の関数を作成する方法すら知らない！ いいえ、できます。まだ知りません。

次の例を考えてみましょう： λx.λy.x+ y 。 わかりやすくするために、括弧を付けます： λx。（Λy。（X + y））は、合計を返す別の関数を返す関数です。 どのように機能しますか？ それをいくつかの引数に適用してみましょう： （λx。（Λy。（X + y）））a =λy。（A + y） 。 結果の関数は、別の引数（λy。（A + y））b = a + bに適用できます。 この手法はcurrying 、またはcurrying （Haskell Curryの後）と呼ばれ、任意の数の引数に対して機能します。 関数の形式がλx。（Λy。（Λz。（F）））の場合、 λxyz.Fと書くことに同意します。 また、 （fabc）は
（（（fa）b）c） 。 これで、多くの引数の関数は非常に簡単に記述されます： λxy.x+ y 、およびそれらのアプリケーションは（fab）です。

ちょっとした余談：この記事は型のないλ計算に関するものであるにもかかわらず、数値と算術演算を繰り返し使用しましたが、正式にはまだ数値と演算については知りません。 これは理解を深めるために行われ、すぐに両方がλ計算で実現できることがわかります。

制御構造

ここで、λ計算でサイクルを作成する方法の質問に答えます。 関数のみを扱っているため、明らかに、再帰メカニズムを使用しています。 しかし、λ計算では、関数を自分の中から呼び出すことはできないため、少し異なるアプローチが使用されます。関数は引数として自身に渡されます。

次の関数を考えてください： w =λx.xx。 彼女は彼女に唯一の議論を適用します（私たちにとって、あなたが取るものはすべて関数であることを忘れないでください）。 この関数を自分自身に適用してみましょう： ww =（λx.xx）w =（xx）[x：= w] = ww おっと、β-還元を使用して、私たちは始めたところに来ました。 これは、λ計算における無限ループの最も単純な例の1つであり、絶対に何もしないという点で注目に値します。

別の重要な質問：条件付きステートメントを実装する方法？ ここでは、elseブランチが存在しないことを理解することが重要です。 すべてのオブジェクト、つまり値を返すために必要な関数があり、「何もしない」ことはできません。 次のオブジェクトを定義します。

• true =λxy.x
• false =λxy.y

ここで、 boolがこれらの定義の意味で論理値である場合 、 （boolの場合はbool）がまさに必要な構造です。 bool = trueの場合、結果はifステートメントになり 、そうでない場合はelseステートメントになります。

ここで、ループと再帰の古典的な問題-階乗の計算を解決してみましょう。 すでに数字、算術演算（接頭辞表記でλ計算のスタイルで記述します）、引数を1減らすdec関数、およびゼロと等しいかどうかを確認できるゼロ関数を用意しましょう。
g =λrn。（ゼロn）1（* n（rr（dec n）））
よく見てみましょう：関数はnが0に等しいかどうかをチェックし、成功した場合は1を返し、そうでない場合は（* n（rr（dec n））） - nとそれ自体とn-1からの関数rの値の積を返します 関数rとは何ですか？ これは再帰を行うための一種のハックです-rは関数g自体を渡すので、書かれた式は実際に階乗を計算します： g（n）= n * g（n-1） 。 毎回関数を自分自身に渡すのは不便なので、階乗の最終的な実装を行います。
f = gg
したがって、 gは最初の引数を 「記憶」し、残りは計算に必要な数を渡すだけです。

さらに悪い。

固定小数点コンビネーター

関数fのラムダ計算では、 fx = xのような引数xが存在することがわかります。 さらに、このxは常に見つかります！ この作業は、いわゆる固定小数点コンビネーターによって行われます。 私たちの最愛のHaskell Curryによって発明されたそのオプションの1つ：
Y =λf。（Λx.f（xx））（λx.f（xx））
仕組みを見てみましょう。
Y f =（λx.f（xx））（λx.f（xx））= f（（λx.f（xx））（λx.f（xx）））= f（Y f）
したがって、 f（Y f）= Y fであるため、 Y fは実際には関数fの固定小数点です。

数字と算術

ご想像のとおり、上記の必要なオブジェクトと構造の実装はすべて一意ではありません。λ計算の魅力は、必要な基本的なものの実装方法を決定できることです。 しかし、サイクルと条件に関して、最も単純な実装が特定されているように思える場合は、数字によって物事が異なります-数字の実用的な実装はたくさんあります。タスクごとに独自の特定のオプションを考え出すことができます。 それにもかかわらず、アロンゾ教会によって発明された数字-教会の数字の一般的に受け入れられた実装があります。

非負の数Nを、関数f 、引数x 、およびxからfの値を計算するN回を取る関数として定義します。

• 0： x
• 1： f（x）
• 2： f（f（x））
• 3： f（f（f（x））））

したがって、λ計算では、数値は次のようになります。

• 0： λfx.x
• 1： λfx.fx
• 2： λfx.f（fx）
• 3： λfx.f（f（fx））

Inc関数：
inc =λnfx.f（nfx）
関数をn回適用し、もう一度適用してn + 1を取得しました。

mとnを追加する方法は？ fを最初にxに適用し、次にn回実行する必要があります。

add =λmnfx.mf（nfx）

乗算が簡単になります。xに （nf）回適用する必要があります。

mult =λmnf.m（nf）

パワーアップ-さらに簡単：
pow =λmn.nm

引数がゼロかどうかをチェックする関数を作成します。
λn.n（λx.false）true
引数がゼロの場合、（定義から覚えているように）2番目の引数を返すだけです。 true 、そうでない場合、関数λx.falseをそこにあるものに何度も（まあ、少なくとも1回）適用します。 そのため、先ほど説明した定数が役に立ちました 。戻り値はfalseになります 。

今、もっと難しいのは減算です。 最初に、1より小さい数値（または引数が0の場合は何か）を返す関数を作成します。 ここにあります：
dec =λnfx.n（λgh.h（gf））（λu.x）（λu.u）
「地獄はどのように機能するのか？」という質問に関連して、今では最も永続的なものでさえ神経を失っていると思います。 理解してみましょう。

まず、ピースn（λgh.h（gf））（λu.x）を見てみましょう-未知の何かがn （λu.x） n回適用されます。 教会の番号のようになり、適用してみましょう。

• 初回： （λgh.h（gf））（λu.x）=λh.h（（λu.x）f）=λh.hx=λh.h（0 fx） （ゼロの定義による）
• 2回目： （λgh.h（gf））（λh.hx）=λh.h（（λh.hx）f）=λh.h（fx）=λh.h（1 fx） （ここで、 h中括弧とh外側-異なる変数）
• 3回目： （λgh.h（gf））（λh.h（fx））=λh.h（（λh.h（fx））f）=λh.h（f（fx））=λh.h（2 fx）

したがって、 n回のアプリケーションの後、式は次の形式になります。
dec n =λfx。（λh.h（（n-1）fx））（（λu.u））=λfx。（λu.u）（（n-1）fx）=λfx。（n-1）fx =（n-1）
利益！
しかし、ゼロの場合、関数は何を返しますか？
dec 0 =λfx。（λu.x）（λu.u）=λfx.x= 0

定義の0とfalseは同じであることに注意してください。

これで、簡単に記述および減算できます。
sub =λmn。（n dec）m

コンビネーター

コンビネータは、自由変数を含まないλ関数です。 それらの変数はすべて、λ-抽象化によって接続されます。
非コンビネーターの例：

• λx.y
• λxyz.y（zt）

コンビネーターの例：

• I =λx.x-引数を返す関数
• K =λxy.x-定数ジェネレーター
• S =λxyz。（Xz）（yz）
• Y =λf。（Λx.f（xx））（λx.f（xx）） -これでコンビネーターと呼ばれた理由がわかりました
• B =λxyz.x（yz）
• C =λxyz.xzy
• W =λxy.xyy

そしてもう1つの興味深い事実：他のλ関数を表現できる有限の組み合わせの組み合わせを選択することができます！ このようなキットは、たとえば、 SKIおよびBCKWです。

ウンラムダ

Unlambdaは、組み合わせロジックを使用した純粋な関数型プログラミング言語です。 つまり、関数を作成するために、SKIセットを使用します。 関数Fを関数Gに適用することは `FGとして書かれており、 不必要な括弧から私たちを救います。 複数の引数を連続して適用する： `` fxyz 。 組み込み関数s、k、iに加えて、言語には画面に表示する機能があります（ .xはiと同様の機能を示しますが、副作用として文字xが画面に表示されます）。また、入力および保留中の計算のメカニズムがあります。行かない

むかしむかし、遠く、遠くの銀河で、次のようなもので終わるアンラムダチュートリアルを見つけました。

今、私はこの言語でフィボナッチ数を計算するサイクルを書くことができる方法を説明したかったのですが、すでにここで私は無力です：
`` `s``s``sii`ki
`k。*` `s``s`ks
`` s`k`s`ks``s``s`ks``s`k`s`kr``s`k`sikk
`k``s`ksk

さて、試してみましょう。
ちなみに、プログラムは、画面にフィボナッチ数を星の対応する数の形で表示します。

サイクルについて説明します。

1. N個の星を表示
2. 翻訳を新しい行に出力します（ublambdaでは、 r関数がこれを行います）
3. 記憶されている以前のフィボナッチ数にNを追加します

とりあえず、私たちは（すでに）馴染みのあるλ計算のスタイルですべてを書きます。

N個の星を印刷 ： N個の印刷i-同じ関数に印刷をN回適用し、同時にN個の星を印刷します。 その結果、同一の機能が得られます。 それを何かに適用しましょう！ （（N print i）newline）（cycle（+ NM）N） 、ここでMは前のフィボナッチ数です。 そのため、サイクルの1パスの関数を取得しました。
cycle =λcnm。（（n print i）newline）（c（+ nm）n）
パラメータとしてループに自分自身を渡し、1と0で初期化します。
fib =サイクルサイクル1 0

私が約束したように、これをunlambdaに変換することは残っています。 おお

式をλ計算からSKIセットに変換するためのアルゴリズムを読者に紹介していただければ幸いです（偶然、任意の関数がSKIで表現できることを示しています）。 したがって、アルゴリズム自体：

• λx.F 、ここでFはxから独立しています-Fの値を持つ定数関数が必要です。これは、 KFであることを意味します
• λx.xは定義によりI
• λx.FG。ここで、 FとGは（おそらく） xを自由に含む式です。 両方の式でxの値を置き換えてから、最初の値を2番目の式に適用する必要があります。 これは、 S ： SFGコンビネーターが行うことです。

最後を除いて、すべてが多かれ少なかれ明白です。 コンビナトリアルSの定義を見てみましょう。
S =λxyz。（Xz）（yz）
Fに適用し、次にGに適用します。
SFG =（λyz。（F z）（yz））G =λz。（F z）（G z）
実際、これが必要なものです。

変換アルゴリズムλx.Fは、次のアクションになります。

• `置換する` `s
• xはiに置き換えます
• Xはxに依存せず、 `kGに置き換えます

次に、必要な「ブリック」をアンラムダに変換します。
0 = `ki
1 = i
追加：

`` s''s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks `` s``s`ks``s`kk`ks``
s''s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s` ks``s``s`ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s `ks``s`kk`kk``s`kk`kk
`` s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk `kk``s``s`ks``s`kk`k
k`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk`` s''s`ks``s`kk`kk``s`
kki

サイクル：

`` s''s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk`` s''ks`s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s `ks``s`kk`kk``s`kk`k。*
`` s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s` `s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk `` s`kk`kk``s``s`s`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s` kk`kk``s``s`ks``s`kk
「kk」s「kki」s「s」ks「s」s「ks」s「kk」ks「s」s「ks」s「kk」kk「s」kk `kk``s``s`ks``s`kk`
っっっきー

そして、完成したプログラム：

`` ``
`` s''s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk`` s''ks`s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s `ks``s`kk`kk``s`kk`k。*
`` s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s` `s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk `` s`kk`kk``s``s`s`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s` kk`kk``s``s`ks``s`kk
「kk」s「kki」s「s」ks「s」s「ks」s「kk」ks「s」s「ks」s「kk」kk「s」kk `kk``s``s`ks``s`kk`kk`ki
`` s''s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk`` s''ks`s`kk`kk`ki`
`s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s``s `ks``s`kk`kk``s`kk`k。*
`` s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s`` s`ks``s`kk`kk``s`kk`k
i``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk``s` `s`ks``s`kk`kk``s`kk`
kr``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk
`ks``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s''s`ks``s`kk`kk``s`k
k`ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s`
kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks`` s``s`ks``s``s`ks``s
`kk`ks``s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks` `s``s`ks``s`kk`kk``
s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk `` s`kk`kk``s``s`s`
`s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s` kk`kk``s``s`ks``s`kk
「kk」s「kki」s「s」ks「s」s「ks」s「kk」ks「s」s「ks」s「kk」kk「s」kk `kk``s``s`ks``s`kk`kk`ki
`` s''s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk`k
s``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s `` s`ks``s`kk`kk``s`kk`
ks``s``s`ks``s`kk`kk``s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s` `s`ks``s`kk`kk``s`kk
`kk``s``s`ks``s`kk`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks `` s``s`ks``s`kk`ks``
s''s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s` ks``s``s`ks``s`kk`ks`
`s``s`ks``s`kk`kk``s`kk`ks``s``s`ks``s``s`ks``s`kk`ks``s``s `ks``s`kk`kk``s`kk`kk
`` s`kk`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk `kk``s``s`ks``s`kk`k
k`ki``s``s`ks``s``s`ks``s`kk`ks``s``s`ks``s`kk`kk``s`kk`kk`` s''s`ks``s`kk`kk``s`kki
私は

はい、はい、私自身はとても怖いです。 ちなみに、プログラムのアンラムダコレクションでは、 同様のコードはそれほど多くのスペースを必要としません。 どうやら、言語の作者は、極小で最適化されたλ計算からunlambdaへの翻訳の秘密の古代技術を所有しています。 それにもかかわらず、私は約束を守った。 最後まで読んでくれた人に感謝します。