The notion of administrative reductions comes up all over the place, even though the term is usually used when discussing continuation-passing style. Briefly, an administrative reduction is a trivial rewriting step that simplifies an expression that is easy to crank out into an equivalent expression that is natural to take in.

Here is an example from modal logic. Kripke figured out that we can translate modal logic formulas systematically into predicate logic by adding an extra “world” argument x to every proposition. For instance, whereas the formula S∧T (“snow is white and trains are late”) translates to the formula S(x)∧T(x) (“snow is white at world x and trains are late at world x”), the formula S∧◻T (“snow is white and it is necessary that trains are late”) translates to the formula

S(x) ∧ ∀y. R(x,y) → T(y).

I follow the convention that all operators associate to the right, so the above is short for S(x) ∧ (∀y. (R(x,y) → T(y))) (“snow is white at world x and, for every world y accessible from x, trains are late at y”). More formally, we can define a function f that maps a modal formula and a world variable to a predicate formula, by induction on the modal formula:

1. f(A,w) = A(w), if A is an atomic proposition.
2. f(φ∧ψ,w) = f(φ,w) ∧ f(ψ,w).
3. f(◻φ,w) = ∀wʹ. R(w,wʹ) → f(φ,wʹ), if w and wʹ are distinct world variables.

Because f takes a world variable for a second argument (so the metavariables w and wʹ stand for world variables), this definition can be a bit tricky to write and understand. For one thing, because the last case above does not pin down the choice of wʹ, the function f is only defined up to α-equivalence among predicate formulas.

We can avoid the second argument to f if we define the translation a bit differently. Let us translate S∧◻T to

S(x) ∧ ∀y. R(x,y) → ∃x. (x=y) ∧ T(x)

or

S(x) ∧ ∀y. R(x,y) → ∀x. (x=y) → T(x)

instead (it doesn’t matter which). This alternative translation is more verbose and requires equality in the target language, but it is more straightforward to define inductively:

1. g(A) = A(x), if A is an atomic proposition.
2. g(φ∧ψ) = g(φ) ∧ g(ψ).
3. g(◻φ) = ∀y. R(x,y) → ∃x. (x=y) ∧ g(φ).

To turn the output of g, which is easier to crank out, into the output of f, which is more natural to take in, we can define a second pass of processing that rewrites the use of equality away. Such a rewriting step is called an administrative reduction because it simplifies an expression into an equivalent expression in a trivial, bureaucratic way.

In general, when we build an expression generator (especially a translator), we can often choose whether to express the same meaning using facilities in the metalanguage or in the object language. Often, the generated expression is easier to understand if we use the metalanguage’s facilities, but the generation process is easier to understand if we use the object language’s facilities. Hence, the latter strategy calls for a subsequent pass of administrative reductions. The two passes of this pipeline can be merged to form a so-called one-pass translation by anticipating where administrative reductions take place.

Another example of an administrative reduction lies in flow chart connectors. We can draw a big flow chart either using a large piece of paper (the metalanguage) or using connector symbols (the object language). Having drawn a big flow chart using connector symbols, we can use scissors and glue (administrative reductions) to simplify it into a connector-free flow chart on a large piece of paper.

Yet another example: When you choose “Save as … MacWrite” in Microsoft Word, Word pipes your document in Rich Text Format to an export converter module, which in turn produces a MacWrite file. As I recall faintly (I probably have the details wrong—is it MacWrite or some other format?), the beginning of a MacWrite file must contain some kind of a count, which unfortunately the converter cannot determine until it reaches the end of its RTF input. Yet, the MacWrite converter manages to process its input and produce its output sequentially without buffering up anything, using the following hack. The MacWrite format has a “fast save” feature, which allows a document to be expressed as an old version followed by a series of patches (differences) to bring it up to date. The converter writes out a dummy count at the beginning, then appends a patch to fix the count at the end.

As far as I know, the term “administrative” was first used by Gordon Plotkin in his seminal study of continuation-passing-style translations. For example, one translation Plotkin defines (the call-by-value one) maps the term λx.xx to the term

λκ. κ λx. λκ. (λκ.κx) λα. (λκ.κx) λβ. αβκ

instead of the simpler (β-reduced) and equivalent term

λκ. κ λx. λκ. xxκ.

Plotkin introduced the term inside quotation marks, suggesting that he coined it.

Speaking of modal logic, how about this for a disappointing subtitle: “The neuroscience of belief: effects of placebo treatments on brain & body”? Reading the part before the colon, I expected to find the modal box for knowledge or belief expressed in the brain as a homunculus of a mind, tragically sandboxed from accessing variables in outer scopes.