I cannot understand why the following beta reduction is permitted in untyped lambda calculus:
(λx.x y) (u v) -> ((u v) y)
Specifically I cannot understand how one can pass two parameters u
and v
to a single parameter x
in the λx.x
part.
To permit the above shouldn't I use currying and have two parameters? Like this—
(λx.(λy.(x y))) (u v)
specifically I cannot understand how one can pass two parameters u and v
You're not passing two parameters u
and v
. You're passing (u v)
, which is a single value, or term: the value of u
applied to v
.
Compare this with ordinary arithmetic: you can apply a function such as sin
to a compound term like sin(x + 1)
because x+1
denotes a single value, even though it is the application of the function +
to two arguments x
and 1
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With