<p>Short answer: <span class="math-container">$\beta$</span>-reduction is done like crazy in any modern optimizing compiler. As you can <a href="https://godbolt.org/z/cb4M9cjYj" rel="nofollow noreferrer">easily check</a> e.g. for GHC.</p>
<p>The caveat is that <span class="math-container">$\lambda$</span>s usually serve no useful purpose in the compiled output and can be safely reduced if possible (with some consideration given to generated code size). Indeed, most <span class="math-container">$\beta$</span>-redexes appear as the result of other optimizations!</p>
<p>but that is <strong>not</strong> the case with <a href="https://en.wikipedia.org/wiki/Inline_expansion" rel="nofollow noreferrer">definition inlining</a>! The heuristics here are shockingly complex, and should be the subject of many articles and books.</p>

CC BY-SA 4.0
2023-12-23T09:25:50.207Z
That's a useful answer, thank you. Basically beta normalization is already done with some heuristics in mind.

However, I haven't understood your sentence "The caveat is that λs usually serve no useful purpose in the compiled output..." -- do you mean that beta redexes should be reduced or that unapplied lambdas should be eliminated?
hirrolot
CC BY-SA 4.0
2023-12-24T16:38:14.827Z
The former, though I guess one can do the latter via defunctionalization/lambda-lifting.
cody
CC BY-SA 4.0
2023-12-25T00:12:49.360Z
So you mean a situation like `(\x -> something) y`, which can be considered as a syntax sugar for let-expressions? Why is this a "caveat" then and what is "λs" in your answer?
hirrolot
CC BY-SA 4.0
2023-12-26T05:39:09.277Z
My use of "caveat" is awkward, I agree, and by $\lambda$s I did indeed mean $\beta$-redexes, with the further addendum that one can eliminate plain old $\lambda$s themselves via defunctionalization (but this introduces a new definition which may need to get inlined at a later stage).
cody
CC BY-SA 4.0
2023-12-27T07:31:43.943Z
Thanks for clarification.
hirrolot
CC BY-SA 4.0
2023-12-22T20:20:34.657Z
2023-12-22T20:20:34.657Z
cody
<p>Beta normalization reduces a lambda term to its <a href="https://en.wikipedia.org/wiki/Beta_normal_form" rel="nofollow noreferrer">beta normal form</a>, if it exists. The beta normal form is a computationally equivalent term with no &quot;redundant&quot; computation, in a sense; for example, <code>(\x -&gt; x + 3) 2</code> would be normalized to just <code>5</code>, which is a more &quot;efficient&quot; version of the original term.</p>
<p>Therefore, I wonder why I haven't seen any attempts to use beta normalization as a program optimization technique then. Like supercompilation, it naturally subsumes many other optimizations, such as inlining and constant propagation. One reason that it is not used this way is that most functional languages are Turing-complete (normalization will not always terminate), which is a fair point, but what about terminating languages, such as the systems of the lambda cube?</p>
<p>Of course, there is a problem of code explosion. But it doesn't seem to stop the supercompilation community from experimenting with program optimization nonetheless. In addition, since normalization works in a different way than supercompilation, code explosion might end up more controllable; e.g., usually normalization doesn't copy the whole evaluation context into each branch when reducing a case-expression blocked by a neutral variable.</p>
<p>Dependently typed languages, such as Idris/Adga/Coq, already have reasonably efficient normalization algorithms (typically variations of NbE) used to check terms during dependent type checking. This kind of languages also happen to be terminating. Implementing a full-blown supercompiler would be harder than just using this normalization mechanism to optimize code.</p>

CC BY-SA 4.0
2023-12-22T08:05:55.263Z
Didn't you answer your own question? Code explosion. Also, people write fewer redices than one migth expect. Take a piece of standard code, say a module in Agda, and try to find some.
Andrej Bauer
CC BY-SA 4.0
2023-12-22T17:34:05.117Z
It depends where you draw the boundary of what you count as program optimisation, but [Partial Evaluation](https://en.wikipedia.org/wiki/Partial_evaluation) does a lot of $\beta$-reduction.
Martin Berger
CC BY-SA 4.0
2023-12-23T09:27:02.893Z
@AndrejBauer, not quite, I've mentioned that 1) code explosion can be managed, and 2) supercompilation also has a problem of code explosion.
hirrolot
CC BY-SA 4.0
2023-12-23T09:29:42.810Z
@MartinBerger, yes, partial evaluation also exploits inlining heavily. If I remember correctly, Futamura mentioned that beta normalization in the lambda calculus is conceptually a partial evaluation mechanism. Although these two approaches are done rather differently -- partial evaluation is not required to reach normal forms.
hirrolot
CC BY-SA 4.0
2023-12-23T10:56:05.703Z
I have got to ask, what is supercompilation?
Andrej Bauer
CC BY-SA 4.0
2023-12-23T12:42:32.437Z
Supercompilation is a program transformation technique that builds a graph of all possible execution states, removes redundancy from the graph, and outputs a residual program, which is an optimized version of the initial one. It builds the graph by unfolding definitions and case-splitting when necessary.

There is [some research](https://www.researchgate.net/publication/48991563_Supercompilation_and_Normalisation_by_Evaluation) studying a connection between supercompilation and NbE. A good introduction can be found [here](https://themonadreader.files.wordpress.com/2014/04/super-final.pdf).
hirrolot
<optimization><lambda-calculus><dependent-type><compilers>
Is beta normalization used for program optimization?
hirrolot
# Is beta normalization used for program optimization?

(Asked by: username_0 on 2023-12-22)

Beta normalization reduces a lambda term to its [beta normal form](https://en.wikipedia.org/wiki/Beta_normal_form), if it exists. The beta normal form is a computationally equivalent term with no "redundant" computation, in a sense; for example, `(\x -> x + 3) 2` would be normalized to just `5`, which is a more "efficient" version of the original term.

Therefore, I wonder why I haven't seen any attempts to use beta normalization as a program optimization technique then. Like supercompilation, it naturally subsumes many other optimizations, such as inlining and constant propagation. One reason that it is not used this way is that most functional languages are Turing-complete (normalization will not always terminate), which is a fair point, but what about terminating languages, such as the systems of the lambda cube?

Of course, there is a problem of code explosion. But it doesn't seem to stop the supercompilation community from experimenting with program optimization nonetheless. In addition, since normalization works in a different way than supercompilation, code explosion might end up more controllable; e.g., usually normalization doesn't copy the whole evaluation context into each branch when reducing a case-expression blocked by a neutral variable.

Dependently typed languages, such as Idris/Adga/Coq, already have reasonably efficient normalization algorithms (typically variations of NbE) used to check terms during dependent type checking. This kind of languages also happen to be terminating. Implementing a full-blown supercompiler would be harder than just using this normalization mechanism to optimize code.

**Tags:** optimization, lambda-calculus, dependent-type, compilers

> **Comments:**
> **username_1**: Didn't you answer your own question? Code explosion. Also, people write fewer redices than one migth expect. Take a piece of standard code, say a module in Agda, and try to find some.  
> **username_2**: It depends where you draw the boundary of what you count as program optimisation, but [Partial Evaluation](https://en.wikipedia.org/wiki/Partial_evaluation) does a lot of $\beta$-reduction.  
> **username_0**: @AndrejBauer, not quite, I've mentioned that 1) code explosion can be managed, and 2) supercompilation also has a problem of code explosion.  
> **username_0**: @MartinBerger, yes, partial evaluation also exploits inlining heavily. If I remember correctly, Futamura mentioned that beta normalization in the lambda calculus is conceptually a partial evaluation mechanism. Although these two approaches are done rather differently -- partial evaluation is not required to reach normal forms.  
> **username_1**: I have got to ask, what is supercompilation?  
> **username_0**: Supercompilation is a program transformation technique that builds a graph of all possible execution states, removes redundancy from the graph, and outputs a residual program, which is an optimized version of the initial one. It builds the graph by unfolding definitions and case-splitting when necessary.  There is [some research](https://www.researchgate.net/publication/48991563_Supercompilation_and_Normalisation_by_Evaluation) studying a connection between supercompilation and NbE. A good introduction can be found [here](https://themonadreader.files.wordpress.com/2014/04/super-final.pdf).  

---

## 1 answers

### Answer by username_3 on 2023-12-22. Score: 4 | Accepted answer

Short answer: $\beta$-reduction is done like crazy in any modern optimizing compiler. As you can [easily check](https://godbolt.org/z/cb4M9cjYj) e.g. for GHC.

The caveat is that $\lambda$s usually serve no useful purpose in the compiled output and can be safely reduced if possible (with some consideration given to generated code size). Indeed, most $\beta$-redexes appear as the result of other optimizations!

but that is **not** the case with [definition inlining](https://en.wikipedia.org/wiki/Inline_expansion)! The heuristics here are shockingly complex, and should be the subject of many articles and books.

> **Comments:**
> **username_0**: That's a useful answer, thank you. Basically beta normalization is already done with some heuristics in mind.  However, I haven't understood your sentence "The caveat is that λs usually serve no useful purpose in the compiled output..." -- do you mean that beta redexes should be reduced or that unapplied lambdas should be eliminated?  
> **username_3**: The former, though I guess one can do the latter via defunctionalization/lambda-lifting.  
> **username_0**: So you mean a situation like `(\x -> something) y`, which can be considered as a syntax sugar for let-expressions? Why is this a "caveat" then and what is "λs" in your answer?  
> **username_3**: My use of "caveat" is awkward, I agree, and by $\lambda$s I did indeed mean $\beta$-redexes, with the further addendum that one can eliminate plain old $\lambda$s themselves via defunctionalization (but this introduces a new definition which may need to get inlined at a later stage).  
> **username_0**: Thanks for clarification.  

---

