全て、
以下は、削減するのが難しいと感じているラムダ式です。つまり、この問題の対処方法を理解できません。
(λm λn λa λb . m (nab) b) (λ f x. x) (λ f x. fx)
これは私が試したものですが、行き詰まっています：
上記の式を : (λm.E) M は
E= (λn λa λb. m (nab) b)
M = (λf x. x)(λ f x. fx) と等しくなります。
=> (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)
上記の式を (λn.E)M と考えると、
E = (λa λb. (λ f x. x) (λ f x. fx) (nab) b)
M = ??
..そして私は迷子になりました!!
任意のラムダ計算式の場合、リダクションを実行する手順はどうあるべきかを理解するのを手伝ってもらえますか?
次の手順に従って、ラムダ式を削減できます。
(λX. e1) e2あるパターンの出現を見つけます。Xe1e2(λx. e1) e2で置き換えて関数を適用します。は、 inの自由出現を で置き換えた結果e1'です。e1'xe1e2あなたの例では、式から始めます
((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x)))
ここで、部分式は、 、(λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))のパターンに適合します。したがって、置換後に が得られ、式全体が次のようになります。X = me1 = (λn. (λa. (λb. (m ((n a) b)) b))))e2 = (λf. (λx. x))(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)))
(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x)))
X = nこれで、 、 、e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))を使用して式全体にパターンを適用できますe2 = (λf. (λx. (f x)))。したがって、置換後、次のようになります。
(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b))
((λf. (λx. (f x))) a)これでパターンに適合し、 になり(λx. (a x))、次のようになります。
(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b))
今回は、パターンを に適用できます((λx. (a x)) b)。これは に減少し(a b)、次のようになります。
(λa. (λb. ((λf. (λx. x)) (a b)) b))
にパターンを適用すると((λf. (λx. x)) (a b))、 に還元されて次のように(λx. x)なります。
(λa. (λb. b))
これで完了です。
あなたが間違っているところは、最初のステップでは、
M = (λf x. x)(λ f x. f x)
元の式にはその適用式が含まれていないためです。これを明確にするために、アプリケーションは左結合であるという規則に従って、暗黙の括弧を入れることができます (新しい括弧に [ と ] を使用し、欠落している "." を挿入します)。
[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x)
ここから、(λv.E) Msome where inside という形式の式を見つけて、 in に置き換えて簡約しvます。これは実際には M への関数の適用であることに注意してください: のようなものがある場合はそうではありません
。なぜなら、N が関数に適用され、M が 2 つの引数として適用されるからです。MEN (λv.E) M
それでも問題が解決しない場合は、各ラムダに括弧を追加してみてください。基本的には、各「.」の後に新しい「(」を追加し、一致する「)」を可能な限り右に配置します。 ("。例として、ここで 1 つ実行しました ([ と ] を使用してそれらを目立たせます):
( (λm . λn . λa . [λb . m (n a b) b]) (λ f x. x) ) (λ f x. f x)