Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

lambda calculus: passing two values to a single parameter without currying

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)
like image 409
dendini Avatar asked Dec 07 '11 14:12

dendini


1 Answers

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.

like image 100
Fred Foo Avatar answered Nov 16 '22 17:11

Fred Foo