いくつかのラムダのベータ還元

私は以下のラムダ計算を持っており、ベータ還元に知りたいと思っています。いくつかのラムダのベータ還元

ラムダは、次のとおりです。

λxy.xy

私が思う、それはそこには、置換されていないと、xが体にバインドされているので、ベータ版は減らすことができないということ。

私の前提は正しいですか？

はい。あなたはここで減らすことしかできません。 – Alec

ηは何ですか？ –

[eta _conversion_]（https://en.wikipedia.org/wiki/Lambda_calculus#.CE.B7-conversion）としてよく知られているようです。 – Alec

ベータ版を適用することはできません（これはおそらくあなたが探しているものです）。ベータ版は、関数アプリケーションにのみ適用することができます（すべての場合ではなく）。

は、xがfに自由に現れないときにλx.fxをfに変換するη変換を適用します。。; xy.xy =＆ラムダ; X＆ラムダ; y.xy → _η＆ラムダ; x.x（= I）

＆ラムダ：次に、あなたの表現に変換することができます。

2017-01-26 09:40:30 Keelan

申し訳ありません私はあなたに従うことができません。 η変換は何を意味しますか？あなたは私に非常に簡単な例を教えてもらえますか？（=私）の意味は何ですか？ –

@zero_coding Eta変換は、ある抽象化が引数xに定数式fを適用する場合（つまり、\ fIがxを含まない場合は\ x.fx'）のみを抽象化すれば、その抽象化はfそのものに相当します。抽象化のみのボックスf/forwards xであるため、削除することができます。 – Keelan

おかげで多くの仲間。 –

答えて