patternMinor
Common name for inverse of beta reduction
Viewed 0 times
inversebetanameforreductioncommon
Problem
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) (34)$
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"?
i.e. $\textbf{transform}(42 + 3 4) = (\lambda x. 42 + x) (34)$
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"?
Solution
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.
Similarly $M \to (\lambda x. M \, x)$ (the converse of eta reduction) is called eta expansion, and so on.
Context
StackExchange Computer Science Q#59307, answer score: 7
Revisions (0)
No revisions yet.