2
$\begingroup$

I think I get the substitution notation in lambda calculus for "simple" applications such as:

(λx.x+1)(5)=[5/x](x+1)=5+1=6

What I don't get is how that works when I pass a lambda as the "parameter". E.g. to compose functions f(x)=x+1 and f(y)=2*y:

(λy.2*y)(λx.x+1)=[λx.x+1/y](2*y)=2*(λx.x+1) (??)

This clearly makes no sense. What does it mean to multiply an abstraction by 2?

I "understand" that the above is meant to yield:

λx.2*(x+1)

But I can't see how strictly following the substitution algorithm allows one to arrive at that result.

$\endgroup$
1
$\begingroup$

Think about it: it certainly makes sense. For a function $f$, $2*f$ is the function $(2*f)(x) = 2*f(x)$. For example, in linear algebra, the linear transformations between two vector spaces form a linear algebra, and its vectors, which are functions, can be multiplied by scalars. By extensionality, functions are uniquely determined by the values they take on arguments, so if $g,h$ are functions such that $g(x) = h(x)$ for all $x$ (and one is undefined on some $x$ iff the other is), then $g=h$. Because $f = \lambda x.f(x)$, conclude $2*f = 2*\lambda x.f(x) = \lambda x.2*f(x)$.

In the second example, you're substituting a function not a number for $y$, and the result, $2*(\lambda x.x+1)$, is itself a function. To get that into the form that won't startle you, you need to convert this finally to $\lambda x.2*(x+1)$. I don't know what system, if any, you're working in; to perform that last conversion requires some rule which allows it.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ If I get the gist of your answer you are basically saying that even in "traditional" realms of mathematics it is understood that multiplying a function with a number really means applying that operation on the values of the function for a given input. So the square root of a function, is really the same function with its values squared, and I guess one can also define the factorial of a function, or the logarithm of function, etc. Do I read you right? $\endgroup$ – Marcus Junius Brutus Nov 15 '15 at 21:51
  • $\begingroup$ Yes you read me exactly right. For those operations you mention that "look like" functions, e.g. $\log_2$ or $\ln$, there's no reason (& it's confusing) to write e.g. $\log_2(f)$ because you really mean function composition. But for other operations, e.g. square, sqrt, it's quite common to see $f^2$, not uncommon to see $\sqrt f$, etc. $\endgroup$ – BrianO Nov 15 '15 at 22:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.