# notation for substitution in lambda calculus

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.

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.
• 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. – BrianO Nov 15 '15 at 22:03