The A Means A

I have argued about the definition of “ANF” many times. I have looked at the history and origins, and studied the translation, and spoken to the authors. And yet people insist I’m “quacking” because I insist that “ANF” means “A-normal form”, where the “A” only means “A”.

Here, I write down the best version of my perspective so far, so I can just point people to it.

I want to answer three question: what does the A mean, why does the A matter, and where does the A come from.

What does the A mean?

The “A” in “A-normal form” refers to a particular formal object, named “A” (not “administrative”), with respect to which there is a normal form with certain useful properties. This form is “A normal”—none of the A reductions apply to terms in this form—hence, A-normal form.

While it’s true that the history of ANF is concerned with “administrative reductions” in CPS, this is an informal concept, modeled by the formal object “A”.

In truth, “A” is several formal objects, defined somewhat differently in at least 3 different papers. Only one of these is arguably called “administrative”, but is about CPS, and not what we now call ANF.

“A” appears in “The Essence of Compiling with Continuations”, page 5. Under the discussion of the CPS, optimization, and un-CPS diagram, the authors observe that this diagram begs for a completion, some direct process, “A”, that simply normalizes a term within the same language. This diagram is reproduced below: They ask, what are some set of reductions, call this set A, such that normalizing with respect to A would produce a normal form, A-normal form, that characterizes the use of CPS in practice.

The same pattern appears in "Reasoning about Programs in Continuation-Passing Style, page 1:

Thus, we refine this question as follows: Is there a set of axioms, A, that extend the call-by-value λ-calculus such that: …

The authors go on to define the set A, never naming it by some administrative reductions, but deriving A instead from the inverse CPS translation.

We could argue that Sabry’s thesis, Chapter 3, Section 1, “Administrative Source Reduction: The A-Reductions”, names the A-reductions “administrative”. He goes on to analyse those reductions considered to be the administrative ones, defining βlift and βflat in terms of CPS. He then defines in Definition 3.1, the administrative source reduction (A-reductions). However, these refer to reductions over CPS terms, and are distinct from the reductions considered for ANF. While they are the origin of ANF, they do not produce terms in what we now call ANF. A term in “administrative normal form” with respect to that set of reductions would actually be in CPS. That’s not what we mean when we say ANF; we mean normal with respect to the set A defined in “The Essence of Compiling with Continuations”.

Maintaining this distinction between the formal object A and the informal notion of administrative reductions is important for two reasons. First, it helps remind us that ANF is a form ultimately about normalizing a specific set of reductions, not the output of a particular translation, which is important in practice. Implementations often relax ANF until code generation, by omitting some of the A reductions, typically, A2 in “The Essence of Compiling with Continuations”—even that paper relaxes A2 in their implementation in the appendix, because A2 leads to exponential code duplication or requires object-language continuations (“join points”). It’s hard to even formally discuss this relaxation if we do not have the set of normalized reductions in mind. Second, the idea that ANF is free of “administrative” redexes is absurd, since the idea of the administrative redex is an informal concept: a reduction that isn’t really necessary but merely an artifact of the translation. It is easy to introduce such administrative redexes in ANF; e.g., let x = y in x contains an extra unnecessary ζ redex, but it is in ANF. It is, however, free of A reductions.

Why does the A matter?

I don’t actually care what the “A” means, or what the authors intended it to mean. I care that we think about ANF as a normal form, normal with respect to a specific set of reductions.

This most recent rant was triggered by a conversation with a reviewer, who, after observing that the “A” actually stood for “administrative”, asked whether our ANF translation could be decomposed into two translations, one that did everything but normalize the ifs (handling if is annoying in ANF, as it either requires being clever or causes code duplication), and then separately handle if.

The answer is completely obvious… if you think about ANF in terms of a normal form with respect to a set of reductions, and not as merely the output of some translation process, nor “CPS but like without adminsitrative redexes”. Since ANF is a normal form with respect to “A”, we can easily decompose it into multiple normal forms, thus deriving several decomposed translations: remove the A reduction that normalizes if, and you get another normal form. Remove the rules that normalize if and nested let, and you get monadic form.

But all of this is much more complicated to explain if you think of ANF as a particular translation or particular syntactic form, and not a normal form with respect to the set A. And this seems to be very likely how you will think of you think A means administrative.

Where does the A come from??

Incidentally, I spoke with Amr after he read this blog post. The origin of the “A” comes from a result by Curry, who proves some theorems about any combinatory logic extended by a set A of ground equations: https://staff.fnwi.uva.nl/p.h.rodenburg/Varia/RelCLlam.pdf

This led Matthias to ask Amr to create a set A, such that bla bla bla.

Amr admits he may have intended a pun between A and administrative, but doesn’t remember.