3
$\begingroup$

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"?

Improve this question
$\endgroup$
4
  • $\begingroup$ Isn't this called abstraction? I do not mean the syntactic category, but transformation: you "abstract over" the right summand of the sum expression. $\endgroup$ – Anton Trunov Jun 6 '16 at 10:16
  • $\begingroup$ 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. $\endgroup$ – choeger Jun 6 '16 at 10:57
  • 1
    $\begingroup$ I see what you mean. Btw, it looks like a let-expression. $\endgroup$ – Anton Trunov Jun 6 '16 at 11:11
  • $\begingroup$ Indeed. Closure conversion requires a similar transformation (the abstracted terms being the lambda-expressions with all free variables explicitly bound). $\endgroup$ – choeger Jun 6 '16 at 11:30
6
$\begingroup$

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.

Improve this answer
$\endgroup$

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.