ラムダ計算におけるEta抽象化

Etaラムダ計算における抽象化は、以下を意味する。ラムダ計算におけるEta抽象化

A function `f` can be written as `\x -> f x`

ラムダ表現を減らしながらエタは任意の用途を抽象化していますか？それは特定の表現を書いている別の方法ですか？

2016-11-15 user634615

を締結することができ、ETAの変換が評価 – naomik

感謝を遅らせるために有用な方法であることができ、あなたはETAの抽象化のいくつかのユースケースがあり、いくつかのリンクまたは例に私を指すことができます。 – user634615

厳密な評価の下では、有名なYコンビネータを実装するためにη抽象化を使用することができます。 'Y：= U（λh。λf。f（λx.h h f x））'ここで 'U：=λf。 f f' - ここで 'x'ηの抽象化がなければ、厳格な評価者は無限ループに入ります。 – naomik

ETAの縮小/拡大は

f = g

与えられ、それは任意のX

f x = g x

ため、その逆もあること、でなければならないと言う法則の単なる結果です。

そこで与えられた：

f x = (\y -> f y) x

我々は右側に真でなければなりません

f x = f x

を減らすベータにより、取得します。したがって、私たちは、あなたの評価戦略によって

f = \y -> f y

2017-01-23 19:57:03 Ingo

答えて