最初の部分では、ラムダ計算が何であるかについての理論的なアイデアを示しました。 この記事では、非公式の練習-練習-練習のヨガの戒めに従い、実際にそれを見ていきます。
教会ブール定数
すでに述べたように、純粋な純粋型のラムダ計算では、関数を除くすべてが欠落しています。 したがって、数値やブール値などの基本的なものでさえ、自分で実装する必要があります。 より正確には、必要なオブジェクトのように動作するいくつかのアクティブなエンティティを作成する必要があります。 そして、もちろん、コーディングプロセスは、対応する関数を記述することから成ります。
最も単純な
True
と
False
から始めます。 これらの定数の動作を具体化する2つの用語は次のとおりです。
tru = λt.λf.t
| 常に最初の引数を返す2つの引数を持つ関数 |
fls = λt.λf.f
| 常に2番目の引数を返す2つの引数を持つ関数 |
この
if
なブール定数の
if
は次のようになります。
if = λb. λx. λy.bxy
ここで、
b
は
tru
または
fls
、
x
は
then
、
y
は
else
。
これがどのように機能するかを見てみましょう：
if fls te
if
条件
if
false（
fls
）であるため、
else
ブランチからの式（この場合は
e
）が返されます。
(λb. λx. λy. bxy) fls
te
| 定義により |
(λx. λy. fls xy)
te
| 前の行から下線が引かれた式の縮小 |
(λy. fls ty)
e
| 前の行から下線が引かれた式の縮小 |
fls te
| 前の行から下線が引かれた式の縮小 |
(λt.λf. f) t
e
| 定義により、 fls
|
(λf. f)
e
| 前の行から下線が引かれた式の縮小 |
e
| 前の行から下線が引かれた式の縮小 |
基本的なブール演算子の定義も複雑ではありません。 たとえば、接続詞（論理「and」）は次のようになります。
and = λx. λy. xy fls
2つのブール値
x
および
y
and
取得します。 最初は
x
（通貨）です。 それが
tru
（縮小後の
tru y fls
）の場合、
y
が返され、次に真偽もチェックされます。 したがって、
x
と
y
両方
y
「true」の場合にのみ、最終的な
tru
を受け取ります。 他のすべてのオプションでは、答えは
fls
です。
運動
論理的な「どちらか」と「しない」を定義します。
答え
or = λx.λy. x tru y
not = λx. x fls tru
教会番号
自然数のみをエンコードします。自然数については、そのセットを定義するPeanoの公理を思い出してください。 実装は、ユニット、2などのような特定のコンテキストで動作する関数に基づいて継続されます。 実際、これはラムダ計算の機能の1つです。その用語で記述されたエンティティは、オブジェクトの動作を具現化するため、自給自足を持ちません。
したがって、2つの引数を取る関数が必要です。固定された初期値と、次の要素を決定する関数（ フォローアップ関数 ）です。 数は、初期値までのフォロー機能のアプリケーション数でエンコードされます。
0 ≡ λs.λz. z
| 関数s
は初期値 z
ゼロ回適用されます |
1 ≡ λs.λz. sz
| 関数s
は z
初期値に1回適用されます |
2 ≡ λs.λz. s (sz)
| 関数s
は z
初期値に2回適用されます |
| ... | などなど |
ゼロが論理Falseと同じ方法でエンコードされていることに気付くのは簡単です。 それでも、これから広範囲にわたる結論を引き出すべきではありません。これは単なる偶然です。
フォロー機能のタスクは、指定された数に1を追加することです。 つまり 引数として、増加したい値を取ります。これは2つの引数の関数でもあります。 したがって、合計で、関数
(+1)
は3つの引数があります。前の教会番号
n
、初期値に
n+1
回適用される関数、および初期値自体です。 次のようになります。
scc = λn. λs. λz. s (nsz)
ここで、
nsz
は
z
回に適用される関数
s
です。 ただし、明示的な
s (nsz)
が取得される場所から
n+1
回適用する必要があります。
“ unit”から
one = λs.λz. sz
を取得する必要があるとします
one = λs.λz. sz
one = λs.λz. sz
“ two”
two = λs.λz. s (sz)
two = λs.λz. s (sz)
。 次のようになります。
scc one s' z'
| s'
および z'
置換された値と変数名を混同しないため |
(λn. λs. λz. s (nsz)) one
s' z'
| 定義により、 scc
|
(λs. λz. s (one sz)) s'
z' | 前の行から下線付きの表現の削減 |
(λz. s' (one s' z)) z'
| 前の行から下線付きの表現の削減 |
s' (one s' z')
| 前の行から下線付きの表現の削減 |
s' (
（λs.λz.sz）s' z '） | 定義により |
s' (
(λz. s' z) z'
)
| 前の行から下線付きの表現の削減 |
s' (s' z')
| 前の行から下線付きの表現の削減 |
two s' z'
| 定義によりtwo
|
算術演算
追加
2つの教会番号を合計する関数は、
x
と
y
2つの項を取ります。これらの引数には、
s
（フォローアップ関数）と
z
（初期値）の2つの引数もあります。 追加は、最初に
s
を
z
x
回に適用してから、さらに
y
回適用することになります。
plus = λx. λy. λs. λz. xs (ysz)
例として、
one = λs.λz. sz
追加し
one = λs.λz. sz
one = λs.λz. sz
および
two = λs.λz. s (sz)
two = λs.λz. s (sz)
。 答えは次のようになります：
three = λs.λz. s (s (sz))
three = λs.λz. s (s (sz))
。
plus one two s' z'
| s'
および z'
置換された値と変数名を混同しないため |
(λx. λy. λs. λz. xs (ysz)) one two s' z'
| 定義により |
one s' (two s' z')
| 削減後 |
(λs.λz. sz) s' (two s' z')
| 定義により |
s' (two s' z')
| 削減後 |
s' (( λs.λz. s (sz) s' z')
| 定義によりtwo
|
s' (s' (s' z'))
| 削減後 |
three s' z'
| 定義three
|
乗算
乗算の関数は、加算関数を介して定義できます。 最後に、
x
に
y
掛けることは、
y
x
コピーを追加することを意味します。
times = λx. λy. x (plus y) z
plus
を使用せずに、教会番号による乗算を決定する別の方法があります。 彼の考えは、製品
x
と
y
を取得するには、関数
s
を
x
回、初期値に
x
回適用する必要があるということです。
times' = λx.λy.λs.λz. x (ys) z
たとえば、
two = λs.λz. s (sz)
を乗算し
two = λs.λz. s (sz)
two = λs.λz. s (sz)
by
three = λs.λz. s (s (sz))
three = λs.λz. s (s (sz))
。 結果は次の形式になります：
six = λs.λz. s (s (s (s (s (sz)))))
six = λs.λz. s (s (s (s (s (sz)))))
。
times' two three s' z'
| s'
および z'
置換された値と変数名を混同しないため |
(λx.λy.λs.λz. x (ys) z) two three s' z'
| 定義により |
two (three s') z'
| 削減後 |
(λs.λz. s (sz)) (three s') z'
| 定義によりtwo
|
three s' ((three s') z')
| 削減後 |
(λs.λz. s (s (sz))) s' ((three s') z')
| 定義three
|
s' (s' (s' ((three s') z')))
| 削減後 |
s' (s' (s' (((λs.λz. s (s (sz))) s') z')))
| 定義three
|
s' (s' (s' ((
(λz. s' (s' (s' z))) z'
)))
| 削減後 |
s' (s' (s' (s' (s' (s' z')))))
| 下線表現の削減 |
six s' z'
| 定義によりsix
|
運動
パワーをパワーに上げる用語を定義する
答え
の
乗：
x
の
y
乗：
power = λx.λy.λs.λz . yxsz
最後の保留中の操作は減算です-教会番号で最も些細なことではありません。 例えば、ベンジャミン・ピアースの本「Types and Programming Languages」によると、希望する人は独立して学習できます。
ラムダ計算のウィキ大要から注目を集めるための引用：「あなたが何かを理解していなくても心配しないでください。 Kleeneが親知らずを抜いたときに、減算が発明されました。 そして今、麻酔は同じではありません。」
おわりに
ご覧のとおり、ラムダ計算では技術的に複雑なものは何もありません。すべて基本的な置換と簡約に帰着します。 しかし、このような小さなツールセットは、ペア、リスト、再帰関数などのように動作するアクティブなエンティティを実装するのに十分です。 それらはやや面倒ですが、すでに述べたように、λ計算はプログラムを書くためではなく、プログラミング言語と型システムの研究と仕様のためのものです。 実際、これでうまく対処できます。