私が書いた Lambda Calculus インタープリターを、Lambda Calculus 式のかなり大きなテスト セットに対してテストしたいと思います。私が使用できる Lambda Calc 式ジェネレーターを知っている人はいますか (Google での最初の検索では何も見つかりませんでした)。これらの式は、明らかに適切に作成する必要があります。
さらに良いことに、私は自分でさまざまな例を作成し、結果を確認できるように解決策を考え出しましたが、解決策を使用して解決されたラムダ計算削減問題の適切な (そして大きな) セットを知っている人はいますか? 自分で式を入力できるので、インタープリターをテストできる、より単純な (そしてより大きな) ラムダ計算式を用意することがより重要です (現時点では、Normal Order と Call by Name の評価戦略をモデル化しています)。
ヘルプやガイダンスをいただければ幸いです。
Asperti と Guerrini (1998 年、The Optimal Implementation of Functional Programming Languages、CUP Press、特に第 5 章と第 6 章を参照) は、Jean-Jacques Levy の再帰とラベル付き簡約の族の理論から生じる、より苦痛なラムダ用語のいくつかを説明しています。衝突するベータ削減間の相互作用の複雑さの尺度。どちらかのレデックスを削減すると、もう一方の作業が作成されます。
リダクションの衝突の比較的単純な例は次のとおりです。
let D = λx(x x); F= λf.(f (f y)); and I= λx.x in
(D (F I))
これは 2 つの beta-redexes を持ち、 に還元され(y y)ます: 通常の置換によってそれらのいずれかを還元すると、2 つの新しい redexes が作成され、それぞれが元の用語の構造の一部に関連しています。
教会の数字を反復することは、同じように良いです:
let T = λfx. f(f( x)) in
λfx.(T (T (T (T T))) f x)
(これは 65 536 の教会数字を減らします)、多くの衝突する redexes を生成します。
一般に、高次の用語を相互に適用することは、それらが「適切に型付けされている」か、または明白に意味があるかに関係なく、複雑な中間構造を生成する大変な作業の良いソースです。