# Common name for inverse of beta reduction

For some transformation, I am currently working on, it is useful to "pull out" subexpressions and replacing them with variables.

i.e. $\textbf{transform}(42 + 3 * 4) = (\lambda x. 42 + x) (3*4)$

This has, of course, the same result (if it does not extract bound variables and is correct only modulo evaluation order, i.e. termination properties might change).

Such a basic operation probably has an established name, but I never heard it. Is it "beta-expansion"?

• Isn't this called abstraction? I do not mean the syntactic category, but transformation: you "abstract over" the right summand of the sum expression. – Anton Trunov Jun 6 '16 at 10:16
• Wouldn't "abstraction" mean to leave the concrete value of x open? I agree that what I am doing with the left-hand side is an abstraction, but I think that applying the argument immediately makes it something different. – choeger Jun 6 '16 at 10:57
• I see what you mean. Btw, it looks like a let-expression. – Anton Trunov Jun 6 '16 at 11:11
• Indeed. Closure conversion requires a similar transformation (the abstracted terms being the lambda-expressions with all free variables explicitly bound). – choeger Jun 6 '16 at 11:30

Yes, it's called beta expansion. Usage examples: Horwitz, Miller, Galbiati and Talcott, Coq manual, …

Similarly $M \to (\lambda x. M \, x)$ (the converse of eta reduction) is called eta expansion, and so on.