2
$\begingroup$

Beta normalization reduces a lambda term to its 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.

$\endgroup$
6
  • 1
    $\begingroup$ 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. $\endgroup$ Dec 22, 2023 at 8:05
  • 1
    $\begingroup$ It depends where you draw the boundary of what you count as program optimisation, but Partial Evaluation does a lot of $\beta$-reduction. $\endgroup$ Dec 22, 2023 at 17:34
  • $\begingroup$ @AndrejBauer, not quite, I've mentioned that 1) code explosion can be managed, and 2) supercompilation also has a problem of code explosion. $\endgroup$
    – Hirrolot
    Dec 23, 2023 at 9:27
  • $\begingroup$ @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. $\endgroup$
    – Hirrolot
    Dec 23, 2023 at 9:29
  • $\begingroup$ I have got to ask, what is supercompilation? $\endgroup$ Dec 23, 2023 at 10:56

1 Answer 1

4
$\begingroup$

Short answer: $\beta$-reduction is done like crazy in any modern optimizing compiler. As you can easily check 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! The heuristics here are shockingly complex, and should be the subject of many articles and books.

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Hirrolot
    Dec 23, 2023 at 9:25
  • $\begingroup$ The former, though I guess one can do the latter via defunctionalization/lambda-lifting. $\endgroup$
    – cody
    Dec 24, 2023 at 16:38
  • $\begingroup$ 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? $\endgroup$
    – Hirrolot
    Dec 25, 2023 at 0:12
  • $\begingroup$ 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). $\endgroup$
    – cody
    Dec 26, 2023 at 5:39
  • $\begingroup$ Thanks for clarification. $\endgroup$
    – Hirrolot
    Dec 27, 2023 at 7:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.