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.