What does it mean to be "closed" under beta reduction?

Question

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.)

Answer 1

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.

Answer 2

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

Answer 3

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.