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
# allowing only constants, λ-terms, and variables, to serve as arguments of function applications, and
# 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)

References

* cite conference
id = Flanagan93
first = Cormac
last = Flanagan
coauthors = Sabry, Amr; Duba, Bruce F.;Felleisen, Matthias
title = The Essence of Compiling with Continuations
booktitle = Proceedings ACM SIGPLAN 1993 Conf. on Programming Language Design and Implementation, PLDI'93
location = Albuquerque, NM, USA
url = http://citeseer.ist.psu.edu/flanagan-essence.html
accessdate = 2007-06-05