lambda - 関数適用を実装したラムダ計算式

Question

次のラムダ計算式を見つけました。

(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))

つまり、これは引数 f を取り、引数 x を取り、x を f に適用した結果を生成する別の関数を返す関数です。上記の式の結果は (λ b . b) になります。

これは部分適用とカリー化を思い起こさせますが、「インサイド アウト」関数適用 (fx) が私の興味をそそりました。

その表現には、より深い理論的な意味がありますか?

Answer 1

この表現は、非常に単純な操作ですが、実際には非常にクールです。所詮、関数はただの関数適用ですよね？

それが興味深いところです。ラムダ計算では、アプリケーションは構文規則であり、「が式であり、式である場合、式である」という単純なf規則xですf x。アプリケーションは、いかなる種類の関数でもありません。これは残念なことです: ラムダ計算はすべて関数に関するものなので、関数ではないものに大きく依存しなければならないのはうんざりです!

あなたの例は、これに対する一種の救済策です。アプリケーションを取り除くことはできませんが、少なくともアプリケーションに対応するものを定義することはできます。その対応物は、ラムダ関数(λ f . (λ x . (f x)))(または、より慣用的にはλfx.f x) です。これは関数なので、他の関数と同じように推論して使用できます。引数として他の関数に渡すことも、関数の結果として使用することもできます。突然、関数アプリケーションがはるかに使いやすくなりました。

ラムダ計算に関する限り、私が持っているのはこれだけですが、この関数や他の同様の関数は、実生活でも非常に役立ちます。関数型プログラミング言語 F# では、この関数には「パイプ後方演算子」という名前さえあり、中置演算子を持つと書きます<|。f (x)そのため、 where xis some 式を書く代わりに、 と書くことができますf <| x。多くの煩わしい括弧を書く必要がなくなるので、これは素晴らしいことです。ここで私が言おうとしている重要な点は、あなたの例は一見アカデミックに見えたり、あまり役に立たないように見えますが、実際にはいくつかの主流のプログラミング言語に採用されているということです。