Administrative normal form

In computer science, administrative normal form (abbreviated ANF) is a canonical form of programs, which was introduced by Flanagan et al. 1993 to serve as an intermediate representation in functional compilers to make subsequent transformations to machine code more direct.

In ANF, all arguments to a function must be trivial. That is, evaluation of each argument must halt immediately.

This article deals with the basic definition expressed in terms of the λ-calculus with weak reduction and let-expressions, where the restriction is enforced by

1. allowing only constants, λ-terms, and variables, to serve as arguments of function applications, and
2. require that the result of a non-trivial expression are captured by a let-bound variable or returned from a function.

Grammar

The following BNF grammar describes the pure λ-calculus modified to support the constraints of ANF:

EXP ::= VAL VAL
     |  let VAR = EXP in EXP

VAL ::= λ VAR . EXP
     |  VAR

Variants of ANF used in compilers or in research often allow constants, records, tuples, multiargument functions, primitive operations and conditional expressions as well.

Examples

The expression:

f(g(x),h(y))

is written in ANF as:

let v0 = g(x) in
    let v1 = h(y) in
        f(v0,v1)