次のラムダ式が与えられます。ここで、は次のようになり\ますlambda。
(\kf.f(\c.co)km)(\x.dox)(\le.le)
(\c.co)kに変換すると間違っていkoますか？私はそれをしました、そして明らかに、それは間違っていました。正しい方法は、最初に外部関数を評価する(\f.f(\c.co)(\x.dox)m)(\le.le)ことでした。つまり、望ましい解決策でした。
講義ノートでそれを示すルールが見つからないので、それは本当ですか？はいの場合、なぜ最初に内部関数を評価できないのですか？私はこのようにそれをしました、そしてそれにもかかわらず私の解決策は正しかったです。
よろしく。
したがって、(型指定されていない) ラムダ計算でのベータ削減は、コンフルエントな書き換え規則と呼ばれるものです。これは、ベータ削減で に書き直すAことができ、ベータ削減で書き直すことができる場合、書き直しと書き直しを行うようなものを見つけることができる場合、事実上、いくつかの共通の子孫が存在することを意味します。ラムダ計算についてこれを示す定理は、通常、BACDBD CDチャーチ・ロッサーの定理。全体的なプロパティは、ダイアグラムがダイヤモンドに似ているため、ダイヤモンド プロパティと呼ばれることもあります (2 つのルートが分岐しますが、最終的には再び一緒になります)。また、「終了」ラムダ式の最終的な結果は、ベータ削減の適用方法に関係なく同じであることも意味します。
ただし、すべてのラムダ項に 1 つの最終結果があるわけではありません。これは、型付けされていない微積分が正規化と呼ばれるものではないことを意味します。ベータ簡約で永遠に展開されるラムダ項がたくさんあります (既約または正規形に到達することはありません)。このような状況では、プログラムの評価が2つの同一のプログラムに対して同じように進行することが保証されるため、書き換えを順序付けるための何らかのシステムを用意しておくと便利です。
もちろん、ラムダのバインディング ルールを尊重していることを確認する必要があるため、間違ったラムダ変数に用語を適用しようとしないでください。
TA に尋ねたところ、アプリケーションは連想のままであるとのことでした。
(\kf.f(\c.co)km)(\x.dox)(\le.le)
と同等です
( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]
これは、 .:/kに適用できない理由を説明しています。(\c.co)
括弧/括弧は、読みやすくするためにのみ使用されます。
よろしく。