The Universe of Discourse

Mark Dominus (陶敏修)
mjd@plover.com

Archive:

2007: J F M A M J
J A S O
2006: J F M A M J
JAS O N D
2005: O N D

Wed, 21 Jun 2006

Will not appear in live blog

Many people know that Lisp's lambda form for constructing functions takes its name from the similar use of the letter λ in Alonzo Church's λ-calculus.

Fewer know that Lisp's "quasiquotation" technique was invented by W. V. O. Quine in 1940.

Normally, in the Lisp programming language, expressions are evaluated; an expresion such as (+ 2 3) is evaluated by looking up the function binding of the symbol +, which is the addition function, then evaluating the subexpressions 2 and 3, which yields the numbers 2 and 3, then passing the 2 and the 3 as arguments to the addition function, which returns the number 5, which is the value of the expression.

Sometimes you want to suppress evaluation, which you do by prepending a quote mark to an expresion. The value of the expression '(+ 2 3) is not the number 5, but rather a list of three elements, of which the first is the symbol +.

Lisp has a notation, particularly useful in macro definitions, called "quasiquotation", that is partway between these. In a macro, you want to generate some Lisp code that will then be inserted into your program at the appropriate place. For example, suppose you are writing a program that frequently needs to calculate x² + y² for various expressions x and y. You could, of course, write a function to do it:

   
        (define sum-of-squares (x y)
          (+ (* x x) (* y y)))

But you might want to avoid the overhead of the function calls, and get the Lisp compiler to expand all the functions inline. One way to do this is with a macro. You would write a macro that took expresions x and y and returned a new expression (+ (* x x) (* y y))) with x and y replaced appropriately. Since the new expresion is a list, you might use Lisp's built-in list function, which manufactures lists:

   
        (defmacro sum-of-squares (x y)
          (list '+ 
            (list '* x x)
            (list '* y y)))

This says to make a list of the symbol *, the value of x, and the value of x; to make another list similarly from the symbol *, the value of y, and the value of y; and then to build a third list from the symbol + and the first two lists.

This is not very easy to read or understand, and code that generates more code is already difficult enough, so Lisp has a special notation, optimized for this purpose, called quasiquotation. The idea is that one provides a quoted expression that is a template for the value that will be produced. Certain parts of the quoted expression represent blanks that can be filled in in the template, and are replaced with calculated values before the template is returned. Quasiquotation in Lisp is denoted by a backquote `. A backquoted expression such as `(+ 2 3) is processed exactly the same as a quoted expression, except that any subexpressions that are marked with commas are evaluated. So, for example, the value of `(+ a b) is a list of three symbols: the symbol +, symbol a, and symbol b. But the value of `(+ ,a b) is a different list: its second element is not the symbol a, but rather is replaced with whatever the value of the symbol a is.

Using the quasiquotation notation, we can rewrite the macro above as:

   
        (defmacro sum-of-squares (x y)
          `(+ (* ,x ,x) (* ,y ,y)))

Which is considerably easier to read, because the code looks just like the value that it is producing.

You might think that the problem that's being solved here would arise only in programming languages, but it arises in mathematical logic as well. Here's an example. Suppose you are a logician, and you are trying to define the syntax of a logical formula. Logical formulas, like programming language expressions, are strings, in a particular syntax. Examples of logical formulas are P, (P ∧ Q), and ((P ∧ Q) → ((P ∧ Q) ∨ R)). So you start off like this:

A logical formula is a string of one of the five following forms:

The strings P, Q, and R are logical formulas.

If x and y are logical formulas, then the string composed of the symbol "(", followed by x, followed by the symbol "∧", followed by y, followed by the symbol ")", is a logical formula.
...

Already #2 is difficult to read and understand, and circumlocutory. We would like to abbreviate it. Perhaps we could say this instead:

If x and y are logical formulas, then the string "( x ∧ y )" is a logical formula.

But no, that is wrong. It asserts that only one particular string, one that is five symbols long, including the symbols "x" and "y", is a logical formula. Oops! Perhaps we meant to say this instead:

If x and y are logical formulas, then ( x ∧ y ) is a logical formula.

No, that is not what we want either. It asserts that the result of applying the as-yet-undefined ∧ operation to the formulas x and y is a logical formula. But ∧ is still undefined, and even once it is defined, it will be an operation on truth values, not on formulas. So this is wrong.

Order
General Topology

with kickback
no kickback

No, you have to use some kind of circuitous language, as I did originally. This problem appears in almost any mathematical discussion that needs to define the syntax of anything. To take an example from a different branch of mathematics, here is a quotation from John Kelley's 1995 book General Topology:

The result of replacing `α' and `β' by variables is, for each of the following, a formula.

α = β α ∈ β

Kelley then has a footnote: "This circuitous sort of language is unfortunately necessary...this sort of circumlocution can be avoided by using Quine's corner convention." What's the corner convention?

Order
Mathematical Logic

with kickback
no kickback

The "corner convention" is simply a new kind of quotation mark, introduced in Quine's 1940 book Mathematical Logic. It works just like the ordinary kind, except that certain expressions are understood to be substituted inside it. My typewriter will not generate the special corner quotation marks that Quine used, so I will content myself with "«" and "»". In Quine's corner convention, the expression "« ( Φ ∧ Ψ ) »" denotes the string composed of the symbols written between "«" and "»", but with the symbols "Φ" and "Ψ" replaced with the values of the variables Φ and Ψ.

And, more generally, any sequence of symbols written between between "«" and "»" is understood to represent that string, but with any occurrences of capital Greek letters replaced with the values of the corresponding values.

With this convention, the circumlocution in the definition of a logical expression can be avoided; it simply becomes:

If Φ and Ψ are logical formulas, then the string «( Φ ∧ Ψ )» is a logical formula.

And similarly Kelley's circumlocution turns into simply "If Φ and Ψ are variables, then «Φ = &Psi» and «Φ ∈ &Psi» are formulas."

So we have here the invention, in 1940, of a mechanism for expressing the computation of strings by substition into templates, and the purpose is the same as it is in Lisp: to avoid the lengthy circumlocutions that would otherwise be required in describing how to build up those strings from their components. The mechanism is the same as with Lisp's quasiquotation and the purpose is the same as with Lisp's quasiquotation.

And finally, what did Quine call this technique? "Quasiquotation"! Case closed.

[Other articles in category /math] permanent link