A-normal form

Last updated

In computer science, A-normal form (abbreviated ANF, sometimes expanded as administrative normal form) is an intermediate representation of programs in functional programming language compilers. In ANF, all arguments to a function must be trivial (constants or variables). That is, evaluation of each argument must halt immediately.

Contents

ANF was introduced by Sabry and Felleisen in 1992 [1] as a simpler alternative to continuation-passing style (CPS). Some of the advantages of using CPS as an intermediate representation are that optimizations are easier to perform on programs in CPS than in the source language, and that it is also easier for compilers to generate machine code for programs in CPS. Flanagan et al. [2] showed how compilers could use ANF to achieve those same benefits with one source-level transformation; in contrast, for realistic compilers the CPS transformation typically involves additional phases, for example, to simplify CPS terms.

Grammar

Consider the pure λ-calculus with constants and let-expressions. The ANF restriction is enforced by

  1. allowing only values (variables, constants, and λ-terms), to serve as operands of function applications, and
  2. requiring that the result of a non-trivial expression (such as a function application) be immediately captured in a let-bound variable.

The following BNF grammars show how one would modify the syntax of λ-expressions to implement the constraints of ANF:

OriginalANF
EXP ::= λ VAR . EXP       | EXP EXP       | VAR       | CONST       | let VAR = EXP in EXP  CONST ::= f | g | h 
EXP ::= VAL        | let VAR = VAL in EXP       | let VAR = VAL VAL in EXP  VAL ::= VAR       | CONST       | λ VAR . EXP  CONST ::= f | g | h 

Variants of ANF used in compilers or in research often allow 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)

By imagining the sort of assembly this function call would produce:

;; let v0 = g(x) move x into args[0] call g move result into temp[0] ;; let v1 = h(y) move y into args[0] call h move result into temp[1] ;; f(v0, v1) move temp[0] into args[0] move temp[1] into args[1] call f

One can see the immediate similarities between ANF and the compiled form of a function; this property is a part of what makes ANF a good intermediate representation for optimisations in compilers.

See also

Related Research Articles

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

<span class="mw-page-title-main">Scheme (programming language)</span> Dialect of Lisp

Scheme is a dialect of the Lisp family of programming languages. Scheme was created during the 1970s at the MIT Computer Science and Artificial Intelligence Laboratory and released by its developers, Guy L. Steele and Gerald Jay Sussman, via a series of memos now known as the Lambda Papers. It was the first dialect of Lisp to choose lexical scope and the first to require implementations to perform tail-call optimization, giving stronger support for functional programming and associated techniques such as recursive algorithms. It was also one of the first programming languages to support first-class continuations. It had a significant influence on the effort that led to the development of Common Lisp.

In computer science, syntactic sugar is syntax within a programming language that is designed to make things easier to read or to express. It makes the language "sweeter" for human use: things can be expressed more clearly, more concisely, or in an alternative style that some may prefer. Syntactic sugar is usually a shorthand for a common operation that could also be expressed in an alternate, more verbose, form: The programmer has a choice of whether to use the shorter form or the longer form, but will usually use the shorter form since it is shorter and easier to type and read.

In programming languages, a closure, also lexical closure or function closure, is a technique for implementing lexically scoped name binding in a language with first-class functions. Operationally, a closure is a record storing a function together with an environment. The environment is a mapping associating each free variable of the function with the value or reference to which the name was bound when the closure was created. Unlike a plain function, a closure allows the function to access those captured variables through the closure's copies of their values or references, even when the function is invoked outside their scope.

In combinatory logic for computer science, a fixed-point combinator, is a higher-order function that returns some fixed point of its argument function, if one exists.

In compiler design, static single assignment form is a property of an intermediate representation (IR) that requires each variable to be assigned exactly once and defined before it is used. Existing variables in the original IR are split into versions, new variables typically indicated by the original name with a subscript in textbooks, so that every definition gets its own version. In SSA form, use-def chains are explicit and each contains a single element.

<span class="mw-page-title-main">Conditional (computer programming)</span> Control flow statement that executes code according to some condition(s)

In computer science, conditionals are programming language commands for handling decisions. Specifically, conditionals perform different computations or actions depending on whether a programmer-defined Boolean condition evaluates to true or false. In terms of control flow, the decision is always achieved by selectively altering the control flow based on some condition . Although dynamic dispatch is not usually classified as a conditional construct, it is another way to select between alternatives at runtime. Conditional statements are the checkpoints in the programme that determines behaviour according to situation.

In functional programming, continuation-passing style (CPS) is a style of programming in which control is passed explicitly in the form of a continuation. This is contrasted with direct style, which is the usual style of programming. Gerald Jay Sussman and Guy L. Steele, Jr. coined the phrase in AI Memo 349 (1975), which sets out the first version of the Scheme programming language. John C. Reynolds gives a detailed account of the numerous discoveries of continuations.

Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of;

In computer science, higher-order abstract syntax is a technique for the representation of abstract syntax trees for languages with variable binders.

<span class="mw-page-title-main">Matthias Felleisen</span> German-American computer science professor and author

Matthias Felleisen is a German-American computer science professor and author. He grew up in Germany and immigrated to the US in his twenties. He received his PhD from Indiana University under the direction of Daniel P. Friedman.

<span class="mw-page-title-main">Racket (programming language)</span> Lisp dialect

Racket is a general-purpose, multi-paradigm programming language and a multi-platform distribution that includes the Racket language, compiler, large standard library, integrated development environment (IDE), development tools, and a set of additional languages including Typed Racket, Swindle, FrTime, Lazy Racket, R5RS & R6RS Scheme, Scribble, Datalog, Racklog, ALGOL 60 and several teaching languages.

In computing, a meta-circular evaluator (MCE) or meta-circular interpreter (MCI) is an interpreter which defines each feature of the interpreted language using a similar facility of the interpreter's host language. For example, interpreting a lambda application may be implemented using function application. Meta-circular evaluation is most prominent in the context of Lisp. A self-interpreter is a meta-circular interpreter where the interpreted language is nearly identical to the host language; the two terms are often used synonymously.

In computer programming, an anonymous function is a function definition that is not bound to an identifier. Anonymous functions are often arguments being passed to higher-order functions or used for constructing the result of a higher-order function that needs to return a function. If the function is only used once, or a limited number of times, an anonymous function may be syntactically lighter than using a named function. Anonymous functions are ubiquitous in functional programming languages and other languages with first-class functions, where they fulfil the same role for the function type as literals do for other data types.

In programming languages, a delimited continuation, composable continuation or partial continuation, is a "slice" of a continuation frame that has been reified into a function. Unlike regular continuations, delimited continuations return a value, and thus may be reused and composed. Control delimiters, the basis of delimited continuations, were introduced by Matthias Felleisen in 1988 though early allusions to composable and delimited continuations can be found in Carolyn Talcott's Stanford 1984 dissertation, Felleisen et al., Felleisen's 1987 dissertation, and algorithms for functional backtracking, e.g., for pattern matching, for parsing, in the Algebraic Logic Functional programming language, and in the functional implementations of Prolog where the failure continuation is often kept implicit and the reason of being for the success continuation is that it is composable.

In mathematics and computer science, apply is a function that applies a function to arguments. It is central to programming languages derived from lambda calculus, such as LISP and Scheme, and also in functional languages. It has a role in the study of the denotational semantics of computer programs, because it is a continuous function on complete partial orders. Apply is also a continuous function in homotopy theory, and, indeed underpins the entire theory: it allows a homotopy deformation to be viewed as a continuous path in the space of functions. Likewise, valid mutations (refactorings) of computer programs can be seen as those that are "continuous" in the Scott topology.

In mathematics, a zonal spherical function or often just spherical function is a function on a locally compact group G with compact subgroup K (often a maximal compact subgroup) that arises as the matrix coefficient of a K-invariant vector in an irreducible representation of G. The key examples are the matrix coefficients of the spherical principal series, the irreducible representations appearing in the decomposition of the unitary representation of G on L2(G/K). In this case the commutant of G is generated by the algebra of biinvariant functions on G with respect to K acting by right convolution. It is commutative if in addition G/K is a symmetric space, for example when G is a connected semisimple Lie group with finite centre and K is a maximal compact subgroup. The matrix coefficients of the spherical principal series describe precisely the spectrum of the corresponding C* algebra generated by the biinvariant functions of compact support, often called a Hecke algebra. The spectrum of the commutative Banach *-algebra of biinvariant L1 functions is larger; when G is a semisimple Lie group with maximal compact subgroup K, additional characters come from matrix coefficients of the complementary series, obtained by analytic continuation of the spherical principal series.

In mathematics, a uniformly bounded representation of a locally compact group on a Hilbert space is a homomorphism into the bounded invertible operators which is continuous for the strong operator topology, and such that is finite. In 1947 Béla Szőkefalvi-Nagy established that any uniformly bounded representation of the integers or the real numbers is unitarizable, i.e. conjugate by an invertible operator to a unitary representation. For the integers this gives a criterion for an invertible operator to be similar to a unitary operator: the operator norms of all the positive and negative powers must be uniformly bounded. The result on unitarizability of uniformly bounded representations was extended in 1950 by Dixmier, Day and Nakamura-Takeda to all locally compact amenable groups, following essentially the method of proof of Sz-Nagy. The result is known to fail for non-amenable groups such as SL(2,R) and the free group on two generators. Dixmier (1950) conjectured that a locally compact group is amenable if and only if every uniformly bounded representation is unitarizable.

In computer science, a "let" expression associates a function definition with a restricted scope.

A CEK Machine is an abstract machine invented by Matthias Felleisen and Daniel P. Friedman that implements left-to-right call by value. It is generally implemented as an interpreter for functional programming languages, but can also be used to implement simple imperative programming languages. A state in a CEK machine includes a control statement, environment and continuation. The control statement is the term being evaluated at that moment, the environment is (usually) a map from variable names to values, and the continuation stores another state, or a special halt case. It is a simplified form of another abstract machine called the SECD machine.

References

  1. Sabry, Amr; Felleisen, Matthias. "Reasoning about Programs in Continuation-Passing Style". Proceedings of the 1992 ACM Conference on LISP and Functional Programming, LFP'92. San Francisco, CA, USA. CiteSeerX   10.1.1.22.7509 . Sabry92.
  2. Flanagan, Cormac; Sabry, Amr; Duba, Bruce F.; Felleisen, Matthias. "The Essence of Compiling with Continuations" (PDF). Proceedings ACM SIGPLAN 1993 Conf. on Programming Language Design and Implementation, PLDI'93. Albuquerque, NM, USA. Flanagan93. Retrieved 2012-11-16.