I am reading the paper Compiling with Continuations, Continued, and in section 2.4, Comparison with ANF, the author draws attention to the fact that ANF is not closed under beta reduction. The snippet of text in question follows:

As Flanagan et al. (1993) suggest, the “back end of an A-normal form compiler can employ the same code generation techniques that a CPS compiler uses”. However, as we mentioned in the Introduction, it is not so apparent whether ANF is ideally suited to optimization. After all, it is not even closed under the usual rule for β reduction (λx.A) v → A[v/x].

What does the author mean by this last sentence? (My guess is that he means ANF beta reduction can introduce new, unbound variables into the reduced term. If that is the case, I am having a hard time visualizing when this would occur and would appreciate outside confirmation that my interpretation is correct.)


The claim is that after applying β-reduction to an expression in A-normal form you can be left with an expression no longer in A-normal form.

The only explicit definition I can find of A-normal form is not consistent with the definition Kennedy seems to be (implicitly) using in this paper. Wikipedia defines A-normal form as the subset of lambda calculus expressions where only constants, $\lambda$-terms, and variables can be arguments of function applications, and then (vaguely) says that results of non-trivial expressions must be captured by let-bound variables.

That is: f(g(x)) is not in A-normal form because the argument to the application of f is another application (g(x)) rather than a constant, $\lambda$-term, or variable. This expression in A-normal form would be something like let y=g(x) in f(y).

Kennedy uses the vague "definition"

a let construct assigns names to every intermediate computation. (Section 1.1.ANF).

But then in Section 1.2 he gives an example of an A-normal form not being preserved under β-reduction

Consider the ANF term let x = (λy.let z = a b in c) d in e. Now naïve β-reduction produces let x = (let z = a b in c) in e which is not in normal form. The ‘fix’ is to define a more complex notion of β-reduction that re-normalizes let constructs (Sabry and Wadler 1997), in this case producing the normal form let z = a b in (let x = c in e).

So apparently Kennedy's variant of A-normal form places some kind of restriction on what can be in the assignment part of a let clause, but I can't figure out what (or why) that restriction is. In addition to Kennedy's paper you linked, I looked in several of his references:

Amr Sabry; Philip Wadler: A reflection on call-by-value. ACM T. Prog. Lang. and Sys. (TOPLAS), 19(6):916-941, 1997.

Amr Sabry; Matthias Felleisen: Reasoning about Programs in Continuation-Passing Style. Lisp and Symbolic Computation 6(3-4):289-360, 1993.

Flanagan, Cormac; Sabry, Amr; Duba, Bruce F.; Felleisen, Matthias: The Essence of Compiling with Continuations. Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, (PLDI):237-247, 1993.

  • $\begingroup$ Thank you for you response and for reframing the statement I was confused about back into the examples given earlier in the paper! $\endgroup$ Apr 6 '15 at 5:54
  • 1
    $\begingroup$ (Whoops, didn't mean to press enter).... I believe I can also help you understand the restrictions on ANF. ANF aims to both name and sequence all "computations." If nested lets were admitted by ANF, then sequential ordering would not be respected -- the binder for the computation that must occur 1st (from the inner let) would syntactically appear later than the binder (of the outer let) for the dependent computation. If allowed, this presumably would complicate compiler analyses' implementations $\endgroup$ Apr 6 '15 at 6:09

A set $S$ is closed under an operation $f$ if, whenever $x\in S$, $f(x)\in S$ also.

  • $\begingroup$ I am aware of that definition but it is unclear to me how to apply this definition to the usage at hand. Would it mean that beta reduction of an A-normal form term would yield a term that is not in A-normal form? $\endgroup$ Apr 5 '15 at 18:43
  • 1
    $\begingroup$ Yes, the set is not closed if there is at least one $x\in S$ such that $f(x)\notin S$. $\endgroup$ Apr 5 '15 at 19:10

An example:

(let (x (f v))
   (g x))

is in ANF. But beta reduction of the x would yield

(g (f v))

which is not.


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.