α-変換

この規則によれば、式 λx. (λx. x) x が λy. (λx. x) y に変換されることがわかる。

1:47 PM

https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97#%E8%AB%96%E7%90%86%E8%A8%98%E5%8F%B7%E3%81%A8%E8%BF%B0%E8%AA%9E

%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97

1:47 PM

例えば、 λx. x と λy. y は同じ関数を表している。

1:49 PM

((λx.M) E) → (M[x := E]) β-reduction Replacing the bound variables with the argument expression in the body of the abstraction.

1:49 PM

https://en.wikipedia.org/wiki/Lambda_calculus

Lambda calculus

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turin...