Continuations and term-rewriting calculi

Thinking is most mysterious, and by far the greatest light upon it that we have is thrown by the study of language.

— Benjamin Lee Whorf.

In this post, I hope to defuse the pervasive myth that continuations are intrinsically a whole-computation device.  They aren't.  I'd originally meant to write about the relationship between continuations and delimited continuations, but find that defusing the myth is prerequisite to the larger discussion, and will fill up a post by itself.

To defuse the myth, I'll look at how continuations are handled in the vau-control-calculus.  Explaining that calculus involves explaining the unconventional way vau-calculi handle variables.  So, tracing back through the tangle of ideas to find a starting point, I'll begin with some remarks on the use of variables in term-rewriting calculi.

While I'm extracting this high-level insight from the lower-level math of the situation, I'll also defuse a second common misapprehension about continuations, that they are essentially function-like.  This is a subtle point:  continuations are invoked as if they were functions, and traditionally appear in the form of first-class functions, but their control-flow behavior is orthogonal to function application.  This point is (as I've just demonstrated) difficult even to articulate without appealing to lower-level math; but it arises from the same lower-level math as the point about whole-computation, so I'll extract it here with essentially no additional effort.

Contents
Partial-evaluation variables
Continuations by global rewrite
Control variables
Insights

Partial-evaluation variables

From the lasting evidence, Alonzo Church had a thing about variables.  Not as much of a thing as Haskell Curry, who developed a combinatorial calculus with no variables at all; but Church did feel, apparently, that a meaningful logical proposition should not have unbound variables in it.  He had an elegant insight into how this could be accomplished:  have a single binding construct —which for some reason he called λ— for the variable parameter in a function definition, and then —I quite enjoyed this— you don't need additional binding constructs for the existential and universal quantifiers, because you can simply make them higher-order functions and leave the binding to their arguments.  For his quantifiers Π and Σ, Π(F,G) meant for all values v such that F(v) is true, G(v) is true; and Σ(F) meant there exists some value v such that F(v) is true.  The full elegance of this was lost because only the computational subset of his logic survived, under the name λ-calculus, so the quantifiers fell by the wayside; but the habit of a single binding construct has remained.

In computation, though, I suggest that the useful purpose of λ-bound variables is partial evaluation.  This notion dawned on me when working out the details of elementary vau-calculus.  Although I've blogged about elementary vau-calculus in an earlier post, there I was looking at a different issue (explicit evaluation), and took variables for granted.  Suppose, though, that one were centrally concerned only with capturing the operational semantics of Lisp (with fexprs) in a term-rewriting calculus at all, rather than capturing it in a calculus that looks as similar as possible to λ-calculus.  One might end up with something like this:

T   ::=   S | s | (T . T) | [wrap T] | A
A   ::=   [eval T T] | [combine T T T]
S   ::=   d | () | e | [operative T T T T]
e   ::=   ⟪ B^* ⟫
B   ::=   s ← T

Most of this is the same as in my earlier post (explicit evaluation), but there are three differences:  the internal structure of environments (e) is described; operatives have a different structure, which is fully described; and there are no variables.

Wait.  No variables?

Here, a term (T) is either a self-evaluating term (S), a symbol (s), a pair, an applicative ([wrap T], where T is the underlying combiner), or an active term (A).  An active term is the only kind of term that can be the left-hand side of a rewrite rule: it is either a plan to evaluate something in an environment, or a plan to invoke a combiner with some operands in an environment.  A self-evaluating term is either an atomic datum such as a number (d), or nil, or an environment (e), or an operative — where an operative consists of a parameter tree, an environment parameter, a body, and a static environment.  An environment is a delimited list of bindings (B), and a binding associates a symbol (s) with an assigned value (T).

The rewrite rules with eval on the left-hand side are essentially just the top-level logic of a Lisp evaluator:

[eval S e]   →   S
[eval s e]   →   lookup(s,e)     if lookup(s,e) is defined
[eval (T₁ . T₂) e]   →   [combine [eval T₁ e] T₂ e]
[eval [wrap T] e]   →   [wrap [eval T e]]

That leaves two rules with combine on the left-hand side:  one for combining an applicative, and one for combining an operative.  Combining applicatives is easy:

[combine [wrap T₀] (T₁ ... T_n) e]   →   [combine T₀ ([eval T₁ e] ... [eval T_n e]) e]

Combining operatives is a bit more complicated.  (It will help if you're familiar with how Kernel's $vau  works; see here.)  The combination is rewritten as an evaluation of the body of the operative (its third element) in a local environment.  The local environment starts as the static environment of the operative (its fourth element); then the ordinary parameters of the operative (its first element) are locally bound to the operands of the combination; and the environment parameter of the operative (its second element) is locally bound to the dynamic environment of the combination.

[combine [operative T₁ T₂ T₃ T₄] V e]   →   [eval  T₃  match(T₁,V) · match(T₂,e) · T₄]     if the latter is defined

where match(X,Y) constructs an environment binding the symbols in definiend X to the corresponding subterms in Y;  e_child · e_parent  concatenates two environments, producing an environment that tries to look up symbols in e_child, and failing that looks for them in e_parent;  and a value (V) is a term such that every active subterm is inside a self-evaluating subterm.

Sure enough, there are no variables here.  This calculus behaves correctly.  However, it has a weak equational theory.  Consider evaluating the following two expressions in a standard environment e₀.

[eval  ($lambda (x) (+ 0 x))  e₀]
[eval  ($lambda (x) (* 1 x))  e₀]

Clearly, these two expressions are equivalent; we can see that they are interchangeable.  They both construct an applicative that takes one numerical argument and returns it unchanged.  However, the rewriting rules of the calculus can't tell us this.  These terms reduce to

[wrap [operative  (x)  #ignore  (+ 0 x)  e₀]]
[wrap [operative  (x)  #ignore  (* 1 x)  e₀]]

and both of these terms are irreducible!  Whenever we call either of these combiners, its body is evaluated in a local environment that's almost like e₀; but within the calculus, we can't even talk about what will happen when the body is evaluated.  To do so we would have to construct an active evaluation term for the body; to build the active term we'd need to build a term for the local environment of the call; and to build a term for that local environment, we'd need to bind x to some sort of placeholder, meaning "some term, but we don't know what it is yet".

A variable is just the sort of placeholder we're looking for.  So let's add some syntax.  First, a primitive domain of variables.  We call this domain x_p, where the "p" stands for "partial evaluation", since that's what we want these variables for (and because, it turns out, we're going to want other variables that are for other purposes).  We can't put this primitive domain under nonterminal S because, when we find out later what a variable stands for, what it stands for might not be self-evaluating; nor under nonterminal A because what it stands for might not be active.  So x_p has to go directly under nonterminal T.

T   ::=   x_p

We also need a binding construct for these variables.  It's best to use elementary devices in the calculus, to give lots of opportunities for provable equivalences, rather than big monolithic devices that we'd then be hard-put to analyze.  So we'll use a traditional one-variable construct, and expect to introduce other devices to parse the compound definiends that were handled, in the variable-less calculus, by function match.

S   ::=   ⟨λ x_p.T⟩

governed by, essentially, the usual β-rule of λ-calculus:

[combine ⟨λ x_p.T⟩ V e]   →   T[x_p ← V]

That is, combine a λ-expression by substituting its operand (V) for its parameter (x_p) in its body (T).  Having decided to bind our variables x_p one at a time, we use three additional operative structures to deliver the various parts of the combination one at a time (a somewhat souped-up version of currying):  one structure for processing a null list of operands, one for splitting a dotted-pair operand into its two halves, and one for capturing the dynamic environment of the combination.

S   ::=   ⟨λ₀.T⟩ | ⟨λ₂.T⟩ | ⟨ε.T⟩

The corresponding rewrite rules are

[combine ⟨λ₀.T⟩ () e]   →   T
[combine ⟨λ₂.T₀⟩ (T₁ . T₂) e]   →   [combine [combine T₀ T₁ e] T₂ e]
[combine ⟨ε.T₀⟩ T₁ e]   →   [combine [combine T₀ e ⟪⟫] T₁ e]

Unlike the variable-less calculus, where the combine rewrite rule initiated evaluation of the body of an operative, here evaluation of the body must be built into the body when the operative is constructed.  This would be handled by the δ-rules (specialized operative-call rewrite rules) for evaluating function definitions.  For example, for variables x,y and standard environment e₀,

[eval ($lambda (x) (+ 0 x)) e₀]   →⁺   [wrap ⟨ε.⟨λy.⟨λ₂.⟨λx.⟨λ₀.[eval  (+ 0 x)  ⟪x ← x⟫ · e₀]⟩⟩⟩⟩⟩]

Variable y is a dummy-variable used to discard the dynamic environment of the call, which is not used by ordinary functions.  Variable x is our placeholder, in the constructed term to evaluate the body, for the unknown operand to be provided later.

The innermost redex (reducible expression) here, [eval  (+ 0 x)  ⟪x ← x⟫ · e₀], can be rewritten through a series of steps,

[eval  (+ 0 x)  ⟪x ← x⟫ · e₀]
    →   [combine  [eval  +  ⟪x ← x⟫ · e₀]  (0 x)  ⟪x ← x⟫ · e₀]
    →   [combine  [wrap +]  (0 x)  ⟪x ← x⟫ · e₀]
    →⁺ [combine  +  (0 x)  ⟪x ← x⟫ · e₀]

Where we can go from here depends on additional information of one or another kind.  We may have a rule that tells us the addition operative + doesn't use its dynamic environment, so that we can garbage-collect the environment,

    →   [combine  +  (0 x)  ⟪⟫]

If we have some contextual information that the value of x will be numeric, and a rule that zero plus any number is that number back again, we'd have

    →   x

At any rate, we only have the opportunity to even start the partial evaluation of the body, and contemplate these possible further steps, because the introduction of variables allowed us to write a term for the partial evaluation in the first place.

[edit:  I'd goofed, in this post, on the combination rule for λ₀; it does not of course induce evaluation of T.  Fixed now.]

Continuations by global rewrite

The idea of using λ-calculus to model programming language semantics goes back at least to Peter Landin in the early 1960s, but there are a variety of programming language features that don't fit well with λ-calculus.  In 1975, Gordon Plotkin proposed a remedy for one of these features — eager argument evaluation, whereas ordinary λ-calculus allows lazy argument evaluation and thereby has different termination properties.  Plotkin designed a variant calculus, the λ_v-calculus, and proved that on one hand λ_v-calculus correctly models the semantics of a programming language with eager argument evaluation, while on the other hand it is comparably well-behaved to traditional λ-calculus.  Particularly, the calculus rewriting relation is compatible and Church-Rosser, and satisfies soundness and completeness theorems relative to the intended operational semantics.  (I covered those properties and theorems a bit more in an earlier post.)

In the late 1980s, Matthias Felleisen showed that a technique similar to Plotkin's could be applied to other, more unruly kinds of programming-language behavior traditionally described as "side-effects":  sequential control (continuations), and sequential state (mutable variables).  This bold plan didn't quite work, in that he had to slightly weaken the well-behavedness properties of the calculus.  In both cases (control and state), the problem is to distribute the consequences of a side-effect to everywhere it needs to be known; and Felleisen did this by having special constructs that would "bubble up" through the term, carrying the side-effect with them, until they encompassed the whole term, at which point there would be a whole-term rewriting rule to distribute the side-effect to everywhere it needed to go.  The whole-term rewriting rules were the measure by which the well-behavedness of the calculus would fail, as whole-term rewriting isn't compatible.

For sequential control (our central interest here), Felleisen added two operators, C and A, to λ_v-calculus.  The syntax of λ_v-calculus, before the addition, is just that of λ-calculus:

T   ::=   x | (λx.T) | (TT)

In place of the classic β-rule of λ-calculus, λ_v-calculus has β_v, which differs in that the operand in the rule is a value (redexes have to be inside λ-terms):

((λx.T)V)   →   T[x ← V]

The operational semantics, which acts only on whole terms, uses (per Felleisen) an evaluation context E to uniquely determine which subterm is reduced:

E   ::=   ⎕ | (ET) | ((λx.T)E)

E[((λx.T)V)]   ↦   E[T[x ← V]]

For the control calculus, the term syntax adds A and C,

T   ::=   x | (λx.T) | (TT) | (AT) | (CT)

Neither of these operators has the semantics of call-with-current-continuation.  Instead, (AT) means "abort the surrounding computation and just do T", while (CT) means "abort the surrounding computation and apply T to the (aborted) continuation".  Although it's possible to build conventional call-with-current-continuation out of these primitive operators, the primitives themselves are obviously intrinsically whole-term operators.  Operationally, evaluation contexts don't change at all, and the operational semantics has additional rules

E[(AT)]   ↦   T
E[(CT)]   ↦   T(λx.(AE[x]))    for unused variable x

The compatible rewrite relation, →, has rules to move the new operators upward through a term until they reach its top level.  The compatible rules for A are dead easy:

(AT₁)T₂   →   AT₁
V(AT)   →   AT

Evidently, though, once the A operator reaches the top of the term, the only way to get rid of it, so that computation can proceed, is a whole-term rewrite rule,

AT   ᐅ   T

The whole-term rule for C is easy too,

CT   ᐅ   T(λx.(Ax))

but the compatible rewrite rules for C are, truthfully, just a bit frightening:

(CT₁)T₂   →   C(λx₁.(T₁(λx₂.(A(x₁(x₂T₂))))))    for unused x_k
V(CT)   →   C(λx₁.(T(λx₂.(A(x₁(Vx₂))))))    for unused x_k

This does produce the right behavior (unless I've written it out wrong!), but it powerfully perturbs the term structure; Felleisen's description of this as "bubbling up" is apt.  Imho, it's quite a marvelous achievement, especially given the prior expectation that nothing of the kind would be possible — an achievement in no way lessened by what can now be done with a great deal of hindsight.

The perturbation effect appears to me, in retrospect, to be a consequence of describing the control flow of continuations using function-application structure.  My own approach makes no attempt to imitate function-application and, seemingly as a result, its constructs move upward without the dramatic perturbation of Felleisen's C.

Various constraints can be tampered with to produce more well-behaved results.  Felleisen later proposed to adjust the target behavior — the operational semantics — to facilitate well-behavedness, in work considered formative for the later notion of delimited continuations.  The constraint I've tampered with isn't a formal condition, but rather a self-imposed limitation on what sort of answers can be considered:  I introduce a new binding construct whose form doesn't resemble λ, and whose rewriting rules use a different substitution function than the β-rule.

Control variables

Consider the following Scheme expression:

(call/cc (lambda (c) (c 3)))

Presuming this is evaluated in an environment with the expected binding for call/cc, we can easily see it is operationally equivalent to 3.  Moreover, our reasoning to deduce this is evidently local to the expression; so why should our formalism have to rewrite the whole surrounding term (perturbing it in the process) in order to deduce this?

Suppose, instead of Felleisen's strategy of bubbling-up a side-effect to the top level of a term and then distributing it from there, we were to bubble-up (or, at least, migrate up) a side-effect to some sort of variable-binding construct, and then distribute it from there by some sort of substitution function to all free occurrences of the variable within the binding scope.  The only problem, then, would be what happens if the side-effect has to be distributed more widely than the given scope — such as if a first-class continuation gets carried out of the subterm in which it was originally bound — and that can be solved by allowing the binding construct itself to migrate upward in the term, expanding its scope as much as necessary to encompass all instances of the continuation.

I did this originally in vau-calculus, of course, but for comparison with Felleisen's A/C, let's use λ_v-calculus instead.  Introduce a second domain of control variables, x_c, disjoint from x_p, and "catch" and "throw" term structures (κx.T) and (τx.T).

T   ::=   x_p | (TT) | (λx_p.T) | (κx_c.T) | (τx_c.T)

Partial-evaluation variables are bound by λ, control variables are bound by κ (catch).  Control variables aren't terms; they can only occur free in τ-expressions, where they identify the destination continuation for the throw.  κ and τ are evaluation contexts; that is,

E   ::=   ... | (κx.E) | (τx.E)

The rewrite rules for τ are pretty much the same as for Felleisen's A, except that there is now a compatible rewrite rule for what to do once the throw reaches its matching catch, rather than a whole-term rewrite for eliminating the A once it reaches the top of the term.

(τx.T₁)T₂   →   τx.T₁
V(τx.T)   →   τx.T
κx.(τx.T)   →   κx.T

What about rewrite rules for κ?  One simple rule we need, in order to relate expressions with κ to expression without, is "garbage collection":

κx.T   →   T    if x does not occur free in T

We also want rules for κ to migrate upward —non-destructively— when it occurs in an evaluation context; but κ may be the target of matching τ expressions, and if we move the κ without informing a matching τ, that τ will no longer do what it was meant to.  Consider a κ, poised to move upward, with a matching τ somewhere in its body (embedded in some context C that doesn't capture the control variable).

V(κx.C[τx.T])

If C happens to be an evaluation context, then it is possible for the τ to move upward to meet the κ and disappear; and, supposing x doesn't occur free in T, we'd have (VT).  Even if C isn't an evaluation context, (τx.T) thus represents the potential to form (VT).  If we move the κ over the V, then, in order for the τ to still represent the same potential it did before, we'd have to change it to (τx.(VT)).  And this has to happen for every matching τ.  So let's fashion a substitution function for control variables, T[x ← C] where C doesn't capture any variables:

y[x ← C]   →   y
(T₁T₂)[x ← C]   →   ((T₁[x ← C])(T₂[x ← C]))
(λy.T)[x ← C]   →   (λy.(T[x ← C]))    where y isn't free in C
(κy.T)[x ← C]   →   (κy.(T[x ← C]))    where y isn't x or free in C
(τy.T)[x ← C]   →   (τy.(T[x ← C]))    if y isn't x
(τx.T)[x ← C]   →   (τx.C[T[x ← C]])

The "where" conditions are met by α-renaming as needed.  Now we're ready to write our rewrite rules for moving κ upward:

(κx.T₁)T₂   →   κx.(T₁[x ← ⎕T₂] T₂)    where x isn't free in T₂
V(κx.T)   →   κx.(V(T[x ← V⎕]))    where x isn't free in V
κy.(κx.T)   →   κy.(T[x ← y])

As advertised, κ moves upward without perturbing the term structure (contrast with the bubbling-up rules for C).  If we need a first-class continuation, we can simply wrap τ in λ:  (λy.(τx.y)).  The δ-rule for call/cc would be

(call/cc T)   →   κx.(T(λy.(τx.y)))    for unused x

If this occurs in some larger context, and the first-class continuation escapes into that larger context, then the matching κ will have had to move outward before it over some evaluation context E, and substitutions will have transformed the continuation to (λy.(τx.E[y])).

Insights

The orthogonality of continuation control-flow to function application is, in the lower-level math, rather explicitly demonstrated by the way κ moves smoothly upward through the term, in contrast to the perturbations of the bubbling-up rules for C as it forcibly interacts with function-application structure.  The encapsulation of a τ within a λ to form a first-class continuation seals the deal.

The notion that continuations are a whole-term phenomenon —or, indeed, that any side-effect is a whole-term phenomenon— breaks down under the use of floating binding-constructs such as κ, which doesn't require the side-effect to remain encapsulated within a particular subterm, but does allow it to do so and thus allows local reasoning about it to whatever extent its actual behavior remains local.  Whether or not that makes traditional continuations "undelimited" is a question of word usage:  the κ binding-construct is a delimiter, but a movable one.

As a matter of tangential interest here, the vau-calculus handling of sequential state involves two new kinds of variables and four new syntactic constructs (two of which are binders, one for each of the new kinds of variables).  Here's a sketch:  Mutable data is contained in symbol-value assignments, which in turn are attached to environments; the identity of an environment is a variable, and its binding construct defines the region of the term over which that environment may be accessible.  Assignments are a separate, non-binding syntactic construct, which floats upward toward its matching environment-binding.  When a symbol is evaluated in an environment, a pair of syntax elements are created at the point of evaluation:  a query construct to seek an assignment for the given symbol in the given environment, which binds a query-variable, and within it a matching result construct with a free occurrence of the query-variable.  The result construct is an indivisible term.  The query is a compound, which migrates upward through the term looking for an assignment for the symbol in the environment.  When the query encounters a matching assignment, the query is annihilated (rather as a τ meeting its matching κ), while performing a substitution that replaces all matching result-constructs with the assigned value (there may by this time be any number of matching result-constructs, since the result of the original lookup may have been passed about in anticipation of eventually finding out what its value is).

As a final, bemusing note, there's a curious analogy (which I footnoted in my dissertation) between variables in the full side-effectful vau-calculus, and fundamental forces in physics.  The four forces of nature traditionally are gravity, electromagnetism, strong nuclear force, and weak nuclear force; one of these —gravity— is quite different from the others, with a peculiar sort of uniformity that the others lack (gravity is only attractive).  Whilst in vau-calculus we have four kinds of variables (partial-evaluation, control, environment, and query), of which one —partial-evaluation— is quite different from the others, with a peculiar sort of uniformity that the others lack (each of the other kinds of variable has an α-renaming substitution to maintain hygiene, and one or more separate kinds of substitution to aid its purpose in rewriting; but partial-evaluation variables have only one kind of substitution, of which α-renaming is a special case).

[Note: I later explored the physics analogy in a separate post, here.]

Lamlosuo — eliminating grammatical nouns and verbs

Language is a by-product of general properties of human cognition [...] in conjunction with the constraints on communication that are common to evolved primates [...] and the overarching constraints of human cultures on the languages that evolve from them.

— Daniel L. Everett, Don't Sleep, There are Snakes, 2009, Chapter 15.

This post is about a conlang that seeks to completely undermine the grammatical notions of noun and verb — but leaves the lexical noun/verb distinction more-or-less intact.

In the pipeline, I'm assembling some thoughts on continuations; but this material is ready to run.  I find various insights from Lamlosuo apply to programming language design, since both centrally concern the way the mind processes language — but conlanging is, to me at least (and it seems I'm not the only programming language person who thinks so), a pleasure worth savoring for its own sake.  This also relates to my ideas on the role of fiction in science, briefly mentioned in an earlier post.

Lamlosuo is an exploratory prototype; it's designed to explore the practical consequences of the grammatical premise of a project I've been working on since about the turn of the century (early 2000), in preparation for more naturalistic conlangs to be developed for the project later.  Consequently, the prototype's coverage of different areas of conlang design is spotty; and my account of it here will spotlight particular areas where the exploration has produced interesting results, while inevitably shortchanging, at least for the moment, other areas that don't bear on those particular results.  So don't be surprised by the uneven coverage.

Here's a quick list of some interestingly unexpected developments in Lamlosuo — most of which, alas, will end up deferred to a later blog post (a full description of even a modest conlang is a fairly large beast).

• I'd first imagined that since Lamlosuo isn't trying to be naturalistic, it would have no reason for irregularities.  That seems very naive to me now, but of course my view of it now includes the insights Lamlosuo has given me into the nature of linguistic irregularity.
• I deliberately omitted conjugation; but a different sort of morphosyntactic variation arose, with curious similarities and differences to conjugation.
• I'd planned to eventually include an analog to the copular verb, if only to demonstrate that it just wasn't all that important — that it wouldn't be used even though it was there.  When I finally tried to implement that plan, the grammar rejected the addition.
• I really meant the language to be isolating.  Eventually the structural integrity of the language pushed me to add a stiff dose of incorporation.
• As alluded to above:  While I eliminated the noun/verb distinction from the grammatical structure of the language, a distinction still naturally arose between lexical nouns and verbs, though the distinction lacks grammatical import.  Moreover, my work on this conlang project spun off a second project that eliminated both lexical nouns and lexical verbs while leaving grammatical nouns/verbs intact.

Since I can only find room in this post to cover one major item from this list, I've chosen incorporation.  Pseudo-conjugation was tempting, but is probably best appreciated when one is already acclimated to the grammatical structure; and tracing through the route to incorporation is a good way to acclimate.

Contents
Preliminaries: Nouns, verbs, and thought
Phonology and phonotactics
Vectors
Role alignment
Gender
Prefixes
Subordinate content particles
Provectors
Incorporation

Preliminaries: Nouns, verbs, and thought

Nouns and verbs play a central role in the grammar of, afaics, all human natlangs, and most (arguably all the naturalistic) conlangs I've seen.  I'm not talking about lexical nouns and verbs; there are North American languages that subvert the traditional distinction between the lexical categories of nouns and verbs, and of course there's Kēlen that subverts lexical verbs.  However, I see all these languages (including Kēlen) retaining nouns and verbs at the grammatical level:  a simple clause is still constructed from a verb with noun arguments, which information can then be distributed amongst words in various ways.

This conlang project undertakes to demonstrate a naturalistic class of languages that do not use the verb-with-noun-arguments grammatical construct.  That is, I'm trying to build the conlangs and describe a species of conspeakers whose thought processes naturally give rise to these languages.  On the face of it, this sounds like some sort of investigation of either Whorfianism, or Chomskyism, or both; but it isn't either by intent.

I was first struck by the grammatical centrality of nouns and verbs when contemplating the extreme non-centrality of English prepositions, whose meanings can be wildly context-dependent (and accordingly very difficult to translate to/from other languages).  I mused on the possibility of a language in which pairwise relations between nouns/verbs are more grammatically important, while nouns/verbs themselves are more context-dependent.  Meditating on this idea for a dozen years or so, I settled on the notion that while we evolved on land, where survival favored structuring our thoughts in terms of an activity and its participants, the conspeakers evolved in the open ocean where survival favored structuring their thoughts in terms of navigation.  I'd been inspired here by a claim, in the context of a discussion of the fact that dolphins and whales have bigger brains than we do, that while their brains are bigger, most of that extra wetware is oriented toward navigation; and, drawing further inspiration from the prototype of a treasure map —so many paces that way, then turn to face that thing and go till you come to such-and-such, then etc. etc.— I figured a simple clause for the conspeakers would be an arbitrarily long chain of content words, each with a specified semantic connection to the next in the chain.

Why the emphasis on how the grammatical structure arises from the conspeakers' thought processes?  Because I don't buy in to the incomprehensible aliens motif; I didn't think humans would naturally develop languages with this sort of grammar (insert anadew disclaimer here), therefore I wouldn't consider it plausible unless I could explain why some alien species would do so.  I am inclined to believe there is a principle for general-purpose intelligence analogous to computation's Church-Turing conjecture:  just as any two sufficiently powerful computation engines are capable of simulating each other, any two minds with general-purpose intelligence are capable of comprehending each other — in principle.  Intelligent minds can easily fail to figure each other out —last I heard, we still weren't even sure whether or not rongorongo is writing, let alone what it means— but this is quite different from supposing some fundamental limitation of thought processes that would inherently prevent them from comprehending each other.  I consider the incomprehensible-aliens gambit a bad tactic in science fiction, because I think the reader can feel the difference if they're reading fiction with no coherent framework behind what they can see.  The author should know how the aliens think.  (I'm similarly skeptical about the religious motif of things beyond mortal comprehension.)

The project wasn't meant to explore Chomskyan ideas because, to be brutally honest, I've never taken the universal grammar idea seriously enough even to try to refute it.  When I first read the technical papers in which Chomsky defined the Chomsky hierarchy (my first exposure to his work, as the hierarchy bears on programming-language parsing technology), I was turned off by the apparent suggestion that we have string rewriting engines in our heads; to me, a hypothesis both unnecessary and — because it felt, for lack of a better term, digital — implausible.  At any rate, there is no universal grammar consciously behind my conlangs; and, regardless of whether the universal grammar hypothesis is right or wrong, I doubt an attempt to explicitly address it would do anything for the project except bog things down.

Since the project aspires to naturalism, to my mind this requires at least one diachronic family tree of languages, recalling my earlier remark that plausible fiction has a coherent framework behind it.  The tree has to be sketched out before elaborating the languages in it (or they wouldn't be affected by it, defeating the purpose).  At the start of the project, though, I had no clue how to sketch out such a tree because I'd already merrily invalidated the basic classifications I knew of for human languages:  (1) neutral order of the basic sentence elements subject, object, and verb (VSO, SVO, etc.); in this project, a sentence doesn't have these elements; and  (2) alignment system, nominative ergative or whatever; but alignment is all about coordinating the arguments to a verb, and again, in this project a sentence has no such elements.

It seemed, then, that in order to learn the things I'd need to know to sketch out a family tree of these languages, I would have to have already constructed one, to learn how such languages can work in practice.  So the prototype language would be optimized for use as an exploratory vehicle, merrily disregarding naturalism unless, of course, in some particular instance a facet of naturalism were the thing being explored.  Conlangers are often advised to deliberately add irregularities to their languages for naturalistic feel, and from this advice I'd picked up the sense that naturalism would be the only reason for irregularity in a conlang; so I had the unconsidered expectation that the non-naturalistic prototype would have no irregularities.  I was gradually disabused of this expectation.  The prototype is unnaturally regular, though, so keep in mind that this isn't a design flaw.

Phonology and phonotactics

The phonology is the first of many areas of linguistics that the prototype language mostly doesn't explore (the better, hopefully, to focus on other areas).  The larger project design discusses phonetics and phonology extensively.  The conspeakers vocalize in pure tones; the phones (speech sounds) are notes, but the phonemes are the musical intervals from one note to the next (which meshes rather well, imho, with the vectorial/navigational mindset behind the languages).  The conspeakers, realizing they were somewhat isolated by the unpronounceability of their speech sounds to most species that speak with their mouths, constructed a standard orthophony for transdicting their speech into sequences of "oral phonemes", chosen to be manageable by most other species.  There's some good fun there, but in the prototype it would only get in the way.  The prototype phonology needs to be easily constructed and easy (for me) to pronounce, so not to discourage exploration.

I started out designing a thoroughly bland phonology.  For vowels I made a simple neutral choice:

	front	back
close	i	u
mid	e	o
open	a

I gave syllables the general form consonant-vowel-consonant, where the onset and coda would both be optional depending on context; the coda could only be a nasal — either n or m — and nasals would only be allowed in syllable codas.  The rhotic consonant r would be omitted.  These are simple generic choices.

At this point, though, it became clear that the phonology was apt to become so boring it would discourage use.  So I slipped in an experiment I'd been curious about, bearing no relation to the project at all except that it seemed to me to belong in a language that doesn't care about naturalism.  I'd wondered how well one could put together a phonology with neither plosives nor fricatives.

Unfortunately, since I was going for ease of pronunciation, and I'd already excluded onset-nasals and r, excluding plosives and fricatives left me with simply too few consonants to choose from.  I adopted three approximants — l j w, as in lore, yore, wore — but still had fewer onset consonants than vowels, which seemed wrong so I added in, after all, two unvoiced fricatives — f and s, as in fore, sore.  (Why unvoiced?  It felt right, phonaesthetically.)

	labial	labio- dental	alveolar	palatal	velar
nasal	m		n
fricative		f	s
approximant			l (lateral)	j	w (labialized)

The arrangement of five onsets and five vowels interacted with the artificial regularity of the language, to produce a great many features of the language coming in groups of five.  The high sonority also gives the language an odd, somewhat fluid phonaesthetic.

Eventually a plosive found its way into the language, by a circuitous route; but I'll get to that.

In theory, a phonotactic rule forbids two consecutive vowels in a word.  However, in some cases, two vowels with an approximant between them sound the same as if the vowels were adjacent — for example, ije sounds like ie — and if one of these vowel-consonant-vowel sequences occurs in a word, the consonant is elided when spelling the word.  So the word is constructed without consecutive vowel phonemes, but it's spelled with consecutive vowel letters.  Precisely:  if a front vowel (i or e) is followed by j and another vowel, or if a back vowel (u or o) is followed by w and another vowel, the consonant between those vowels is elided.  For example, lamlosuwo would be shortened to lamlosuo.  Why introduce these elision rules?  Because I found I was pronouncing the phoneme sequences that way anyhow, and it made the orthography (spelling) less uniform and therefore easier to get one's bearings in (like the bumps on the letters F and J on a qwerty keyboard, that help touch typists feel when their fingers are in the right place).

Vectors

All the conspeakers' content words are vectors, a single grammatical function alternative to grammatical nouns or verbs (hence, the entire phylum of languages are vector languages).  Each vector describes a sort of travel, so might be thought of as a variant on the verb to go.  To identify participants in the action of a vector, any given vector may recognize a series of available vector roles, in poetic similarity to noun cases of human natlangs.  (Imagine conspeaker linguists being frustrated to encounter a language, culturally distant from theirs, in which vectors don't have fixed sets of roles, and struggling to rescue their cherished theory of grammar.)

The prototype language has five roles:

	abbr	description
cursor	CUR	the thing that goes.
start	STR	from which it goes.
end	END	to which it goes.
path	PTH	by which it goes.
pivot	PIV	catch-all role; a participant not belonging to any of the other four.

Some roles of a given vector may be unoccupied, but there is always a cursor.

Enumerating the roles of a vector turns out to be a very good way of defining the vector.  My first vector definition was for a vector meaning roughly speak. 

cursor	what is said.
start	who says it.
end	who it is said to.
path	unoccupied.  (Several things might go here, but I've not yet chosen one.)
pivot	the language in which it is said.

A vector word has an invariant stem, and a mandatory class suffix.  A vector stem is two or more consonant-vowel syllables.  (Put the accent on the first syllable of the stem, btw.)  There are eleven classes — the neutral class, and ten genders.  The neutral suffix depends on the final vowel of the stem:  after a back vowel it's -wa, after a front or open vowel it's -ja (this is chosen so that the consonant on the neutral suffix is elided except when the stem ends with a).

An engendered vector is sort-of-like a noun.  The suffix has the form consonant-vowel, where the consonant determines one of the five roles to be emphasized — making it noun-like — and the vowel determines whether the occupant of that role is volitional or nonvolitional:  a back vowel for volitional, front vowel for nonvolitional.  I'll hold off on enumerating the gender suffixes for a moment, though, because they make much more sense after seeing the role particles, which I'm about to explain.

Role alignment

As one way to orchestrate a connection between consecutive vectors, the prototype specifies a role of each vector, at which they intersect (I imagined something vaguely like tinkertoy knobs, with a choice of sockets to plug into).  There's scope for some good fun in devising alternative ways that vector languages might connect consecutive vectors, but I figured this would do nicely to explore the vector-language concept.

I figured on inserting role particles between consecutive vectors to specify their connection.  I also figured a role particle would be a single consonant-vowel syllable, making these particles immediately distinguishable from vectors; but this presented a problem.  With five roles in each vector, there are twenty five ways to choose a role of the first vector and a role of the second vector; and there are only twenty five consonant-vowel syllables.  So one would have to use every possible syllable, and there would be some very dense way of packing the two role-choices into that one syllable (such as, the consonant determines the first role and the vowel determines the second), with no repeated patterns to aid memorization, and no redundant information to allow for transmission errors.  So instead of a single role particle, put two particles between each pair of vectors:  first a dominant role particle specifying a role of the first vector, then a subordinate role particle specifying a role of the second vector.  The consonant in a role particle indicates the role, and the vowel is back for dominant, front for subordinate.  The particles are easier to memorize, and the pairing of close or mid vowels with the consonants provides redundancy against transmission errors.  This arrangement also left available five possible role particles using the open vowel, so I made these combined role particles, indicating in a single particle that that role was being selected for both vectors.

	a  (open)	e  (front  mid)	i  (front   close)	o  (back  mid)	u (back  close)
l	la		li		lu		cursor
f	fa		fi		fu		start
s	sa	se		so			end
j	ja	je		jo			path
w	wa	we		wo			pivot
	comb.	subordinate		dominant

This table has changed a couple of times since creation.  Originally the start and end both used close vowels, which turned out to be a mistake because one really wants redundant contrasts between start and end.  Also, originally the path used a close vowel for the subordinate and mid for dominant, which had been naively intended to enhance redundant contrasts but instead turned out to be confusing since each of the other consonants used a predictable pair of vowels, and path seems to be, in practice, the least often used of the five roles.

Usually, aligning specified roles of two consecutive vectors means that the same participant occupies both roles; however, in general the meaning of the alignment is determined by role-alignment conventions of the dominant (i.e., first) vector.  In theory, the "usual" meaning of role alignment is simply the convention most vectors adopt.  Each vector has its own unique semantic "shape" that may call for non-generic role-alignment conventions.

For example, combining losua meaning speak with a second vector susua meaning sleep one could say

losua	fu	li	susua
NEUT   speak	DOM   STR	SUB   CUR	NEUT   sleep

Since the start of losua is the speaker, and the cursor of susua is the sleeper, and losua has generic role alignment, this means that some party speaks and sleeps.  One might ask whether the participant does these things simultaneously or sequentially; losua prefers to align sequentially (rather than in parallel), so the participant speaks and then sleeps.  (Note, in passing, that there would be no way in English to say this without a subject for the verbs, such as "someone", whereas our prototype sentence has no word corresponding to the subject.)

Combined particles turned out to be highly useful, but not for their original purpose.  In practice, it seems, one rarely wants to align the same role of two consecutive vectors.  However, occasionally it is necessary or convenient for a vector to connect with other vectors in a way that doesn't fit within the usual two-particle model.  Exactly because the combined particles aren't much needed for their regular function, they can be conveniently repurposed for irregular functions; and this has rapidly become a usual practice.  Just as a vector's pivot role and two-particle role-alignment conventions absorb its low-grade idiosyncrasies, its use of combined role particles absorbs medium-grade idiosyncrasies.

After some initial fumbling in the design, neutral vectors were also allowed to occur consecutively with no intervening particles.  The two vectors fuse semantically, so that they interact with the rest of the sentence as if they were a single vector.  The alignment preference of the dominant vector determines whether they fuse in parallel, a single act of travel that is both things at once; or in sequence, a single act of travel that is the first and then the second.  This serves two commonly wanted patterns:  the parallel case is essentially adverbial (advectorial), while the second supports compound navigational paths (as in the treasure-map metaphor).

Gender

The dominant and subordinate role particles are reused as gender suffixes — dominant for volitional genders, subordinate for nonvolitional genders — with one caveat.  The labio-dental fricative f has an allophone used only in start-gender suffixes:  the dental fricative, as in thin, written as t.  Use of this allophone provides redundant information to help filter out transmission errors, which is a solid justification for it; causally, I like the unvoiced dental fricative.

	NV	V
CUR	-li	-lu
STR	-ti	-tu
END	-se	-so
PTH	-je	-jo
PIV	-we	-wo

For example, here are the (usual) engendered forms of losua and susua.  Grammatically, of course, these aren't actually nouns, even though the following list describes the engendered participants:  grammatically they're vectors, so it's still possible to align with any of their non-engendered roles.

losuli	NV.CUR	message
losutu	V.STR	speaker
losuso	V.END	audience
losuo	V.PIV	living natural language
losue	NV.PIV	dead or artificial language

susulu	V.CUR	sleeper
susuti	NV.STR	falling asleep
sususo	V.END	waking
susuje	NV.PTH	sleeping
susue	NV.PIV	dreaming

Semantically, most vectors when engendered take on habitual aspect; so, for example, losutu is a sometime-speaker, rather than the speaker on a particular occasion.  Syntactically, if you are role-aligning on the engendered role of a vector, you can omit the role particle that says so.  Thus,

losutu   li   susua   V.STR   speak   SUB   CUR   NEUT   sleep

the sometime-speaker sleeps

losua   fu   susulu   NEUT   speak   DOM   STR   V.CUR   sleep

the sometime-sleeper speaks

losutu   susulu   V.STR   speak   V.CUR   sleep

the sometime-speaker (is a) sometime-sleeper

Prefixes

A vector can be modified by one or more prefixes of the form consonant-vowel-nasal.  To provide redundancy, I'd like to avoid using two prefixes that differ only by n-versus-m, leaving only twenty five possible prefixes; naturally, I'm trying to reserve them for elemental functions.  I revise the prefix set from time to time, as my ideas evolve about what is most useful.

An especially elemental, and stable, prefix is lam-, which has deictic effect, causing the vector to refer to the immediate situation.  This is notably used with engendered forms of losua:

lamlosuli	what is now being said (the utterance in which the word lamlosuli occurs).
lamlosutu	the party now speaking (first person).
lamlosuso	the party now being spoken to (second person).
lamlosuo	the language now being spoken.

It was rather cool to get the name of the conlang for free (choosing to assume it would be imported into English as a proper noun, so it would still mean the conlang when used in an English sentence); but lamlosutu and lamlosuso seemed excessively clumsy ways to express something as basic as the first and second persons.  Such clumsiness didn't match the exploratory mission of the language; so I posited there would be contractions for those words — latu for first person, laso for second.

laso   fi   losua   V.END   this   speech   SUB   STR     NEUT   speak

you speak

Subordinate content particles

As part of its exploratory mission, the prototype is meant to have a minimalist grammar.  The theory is that an exploratory design has to be changed, and then the revised version has to be relearned — and vocabulary is (says the theory) easier to change, and easier to relearn, than grammar.  In particular, I didn't want to conjugate vectors, because that weighs down the grammar.  How, then, to express something like past tense?

First I crafted a vector for the purpose:  silea, meaning age.  The cursor silelu would be the party who ages, start siletu the time they came from, etc.; but deictic lamsilea seemed so much more useful than silea itself that I figured in ordinary usage one would let the prefix be understood and simply say "siletu" for "the past", and so on.  (Notice how little irregularities are piling up?)

To relate an arbitrary sentence to this time-sense vector, I crafted a new set of grammatical words — subordinate content particles, each of which is just a single vowel.

Siletu a laso fi losua.

The subordinate content particle initiates a subclause, here laso fi losua, and then packages up that clause as if it were the occupant of the subordinate role in a role alignment.  The vowel in the content particle determines the mood of the subclause, here indicative.  The alignment with siletu is understood to specify location of the subclause (here, location in time) — so, "you spoke".  (Is this really a practical way to handle tense?  I don't claim to know; this is a game of gradual exploration.)

siletu   a   laso   fi   losua   V.STR   this   aging   INDIC       V.END   this   speech   SUB   STR     NEUT   speak

in the past: you speak

To assign mood to an entire sentence, simply place the appropriate-mood subordinate content particle at its start.  Using the invitational particle i,

i   laso   fi   losua   INVIT       V.END   this   speech   SUB   STR     NEUT   speak

please, you speak

When an invitational or imperative clause starts with laso which is then aligned with the agent of a neutral vector, the laso and its associated particle are usually left implicit, unless one wants to emphasize the second-person.  (Yes, this is very like English, where one says "please, speak" or "please, you speak"; although ordinarily one would avoid imitating English, here it's potentially interesting that some things aren't necessarily affected by the switch from verb-noun to vector grammar.)  Agents, and one or two other logical roles in a vector, pop up from time to time as the prototype develops; their use in the invitational/imperative elision convention wasn't a novelty.  The agent is a participant understood as causing the action, and if there is an agent it's usually either the cursor, the start, or the pivot.

I losua. — Please speak.
I losua so latu. — Please speak to me.
I losua wo lamlosuo. — Please speak in Lamlosuo.

Here's the complete set of subordinate content particles.

	front	back
close	i invitational	u  imperative
mid	e  noncommittal	o tentative
open	a indicative

Provectors

What if one wanted to say "please speak to me in Lamlosuo"?  The linear simple clause structure only allows aligning a vector with two others:  the one before it, and the one after it.  In our examples, the one before losua is the elided second person.  The one after it could be pivot lamlosuo or end latu.  We don't have any way to align all three with losua at once.

In my earliest sketch of the grammar, I provided for occasionally non-linear structure by means of a device called a recollective provector.  Provectors have a stem of the form vowel-nasal, and take a class suffix agreeing with their antecedent.

	front	back
close	in-  interrogative	um-  recollective
mid	en- indefinite	on- relative
open	an- demonstrative

The recollective provector um- refers to an antecedent that occurred earlier in the same clause.  What makes it recollective is that it doesn't align with its syntactic predecessor.

i   losua   so   latu   uma   wo   lamlosuo   INVIT       NEUT   speak     DOM   END     V.STR   this   speech   REC   NEUT     DOM   PIV     V.PIV   this   speech

please speak to me, that in Lamlosuo

From losua, one starts building a linear clause, but then stops when one discovers the next word is a recollective provector (losua so latu), goes back to the antecedent losua, and begins building another linear clause from there (losua wo lamlosuo). As mentioned, the recollective provector device was created early, in anticipation of later need.  Its actual use didn't begin to arise for some time, until the vocabulary became sufficiently diverse to support a significant number of sentences with more than three vectors in them.  So only then did it become apparent that there were two problems with the recollective provector.

Incorporation

The whole point of the vector-languages concept is that the conspeakers, in fluent speech, are liable to produce long chains of vectors.  Of course we've been translating small, simple English test sentences, so it's to be expected that our vector sentences don't have long simple clauses; but sooner or later, for the project to succeed, fluent vector speech will have to be demonstrated with long vector chains in it.  And both problems with recollective provectors, as originally designed, are related to long simple clauses.

The simpler problem is that in a long simple clause, we expect to find a number of neutral vectors — so that class agreement may be simply not adequate to identify the antecedent of a recollective provector.  This isn't too worrisome; it's a technical problem, but doesn't seem foundational.

There is a deeper problem, though.  Aware from the start that I would eventually have to learn to phrase things fluently — with long simple clauses — my initial plan was to concentrate on creating a language that would support fluent phrasing, and then see if I couldn't ease myself into using more fluent phrasing later on.  The above example, though — i losua so latu uma wo lamlosuo — suggests that the language I'd created might not be able to support long simple clauses:  that any complex sentence would have nonlinear structure requiring use of recollective provectors, and the recollective provectors would chop everything up into very short simple clauses (the longest simple clause in the example is one neutral vector surrounded by two engendered vectors, which might as well be SVO).

Where I'd originally meant to ease into fluent phrasing by means of the prototype, suddenly it looked needful to come up with an example of fluent vector phrasing independent of the prototype.  I've a story, second-hand, of a native German speaker discovering to his pleasure the English term coffee table book; there is something really very German about it (though in German such a thing would likely be one word, coffeetablebook), and one can see how it might strike a German speaker as a breath of air from home.  That is what I wanted:  a (metaphorical) coffee table book for vector speakers.

My test sentence:  "Over the river and through the woods to grandmother's house we go." It does seem rather navigational.  The basic structure (not worrying about specific vocabulary since that's not what we're exploring atm) might be

---lu   li   ---a   ---a   so   ---we   lu   ---tu   V.CUR   group   travel   SUB   CUR     NEUT   over     NEUT   through     DOM   END     NV.PIV   reside     DOM   CUR     V.STR   lineage

we go over-and-then-through to the residence of an ancestor

It seems unlikely the language would have a special vocabulary primitive for over-the-river, or for through-the-woods; more plausibly these would be formed by attaching pivots, respectively river and woods, to more generic primitives for go-over-something and go-through-something.  Extrapolating from the example, I conjecture that any time you have a long chain of vectors offering an opportunity for a long simple vector clause, it's likely that key elements of the chain are too specific to have vocabulary primitives.  And if the only way we have to attach modifiers is using a recollective provector, we're forced to either chop up the longer structure in order to splice in modifiers, or put all the modifiers at the end of the sentence.  Imho, putting all the modifiers at the end doesn't seem like a very navigational organization (although I think there may be some human languages that do weird stuff like that — anadew again).

This is a much narrower problem than the big, general problem addressed by recollective provectors, which are good for building almost arbitrarily complex sentences.  We just need to be able to glide over a few modifiers here and there without disrupting the simple clause structure; and for that I crafted a simple incorporation device.  Any simple clause can be fused into a single word by putting a dab of morphosyntactic glue between each pair of consecutive words; the entire word then behaves, toward the rest of the sentence, as its leading vector — as if a recollective provector had been used, but without disrupting the flow of the clause in which it occurs.  The dab of morphosyntactic glue should be something not found elsewhere; so I used a plosive — unvoiced alveolar, as in tore — pronounced as part of the onset of the following syllable, and written as an apostrophe (both to make its partitioning of the word visually prominent, and to distinguish it from the t allophone of f).

I losua'so'latu wo lamlosuo. — Please speak-to-me in Lamlosuo.

While we're at it, this also offers a possible solution to the problem of ambiguous recollective provectors.  Simply incorporate into the provector a repetition of the antecedent word; in our (admittedly trivial) example,

I losua so latu uma'losua wo lamlosuo. — please speak to me, that speaking in Lamlosuo

Abstractive power

each extensible language is surrounded by an envelope of possible extensions reachable by modest amounts of labor by unsophisticated users.

Thomas A. Standish, "Extensibility in Programming Language Design", SIGPLAN Notices 10 no. 7 (July 1975) [Special Issue on Programming Language Design], p. 20.

I said in an earlier post I should blog about abstractive power "eventually".  This is it.

This material is very much a work in progress.  Throughout this post I'll emphasize insight and intuition — but while the post starts out non-technical, it will get more mathematical by increments as it goes along.  The relation between the math and the insights works both ways:  insights into abstraction guide the mathematical development, and the mathematical development is pursued partly in hopes of eventual further insights into abstraction.  I also hope, by presenting the mathematical development in an intuitive form (as opposed to the much drier form in my 2008 techreport) to get insights into the mathematical development.  The post ends, as does the current state of the work, with an elementary test case to show feasibility.

Contents
The idea
The goal
There is no semantics
The second derivative of semantics
Recasting expressiveness
Abstractiveness
Test case

The idea

The extensible languages movement peaked around 1970, and was on its way out when Standish wrote the above.  Extensibility enthusiasts had hoped, frankly, that by means of language-extension mechanisms it would become possible for everyone to use a single base language and transform it into anything anyone needed for any particular purpose.  Standish was noting that the extension mechanisms primarily used by the movement — macro preprocessors and perhaps the ability to add new syntax rules — had a limited range, after which it became quite difficult to extend the language further.

Macro preprocessing, in particular, cannot easily be used to build a series of extensions, one on top of another, because as extension follows extension, the programmer is rapidly overcome by accumulating complexity.  In order to use a macro, you have to be able to see whatever underlying facility the macro uses.  Thus, to add a second layer of macros to a base language, you have to understand and account for the base language and all of its first layer of macros; to add a third layer of macros, you have to understand the base language, the first layer of macros, and the second layer of macros; and so on.  The visibility of the underlying layers also limits how different the extended language can be from the base language.

The extensibility movement was supplanted by the abstraction movement, which had a more semantic focus, and came to be dominated — at least for a while — by the Object-Oriented Paradigm.  Something of the spirit of the new movement is visible in this remark on lexical scoping from Steele and Sussman's 1978 The Art of the Interpreter; or, The Modularity Complex (p. 24):

What is interesting about this is that we can write procedures which construct other procedures.  This is not to be confused with the ability to construct S-expression representations of procedures; that ability is shared by all of the interpreters we have examined.  The ability to construct procedures was not available in the dynamically scoped interpreter.  In solving the violation of referential transparency we seem to have stumbled across a source of additional abstractive power.

Abstraction helps with the problem of accumulating complexity, because you can — at least, ideally — use an extension without having to worry about all the details of what underlies it.  There is still some accumulated complexity, though.  I noted this in my earlier blog post on types:

In mathematics, there may be several different views of things any one of which could be used as a foundation from which to build the others.  That's essentially perfect abstraction, in that from any one of these levels, you not only get to ignore what's under the hood, but you can't even tell whether there is anything under the hood.  Going from one level to the next leaves no residue of unhidden details: you could build B from A, C from B, and A from C, and you've really gotten back to A, not some flawed approximation of it that's either more complicated than the original, more brittle than the original, or both.

The central point of that blog post is that typing, which is evidently meant to help us manage complexity, can easily become itself a source of complexity.  The same danger applies to other tools we use to manage complexity; the tools become effectively part of the language, and are thus added complexity and subject to accumulation of further complexity.

Another four decades of experience (since Standish's post-mortem on the extensible languages movement) suggests that all programming languages have their own envelopes of reachable extensions.  However, some languages have much bigger, or smaller, envelopes than others.  What factors determine the size, and shape, of the envelope?  What, in particular, can a programming language designer do to maximize this envelope, and what are the implications of doing so?

As a useful metaphor, I call the breadth of a language's envelope its radius of abstraction.  Why "abstraction"?  Well, consider how the languages in this envelope are reached.  Starting from the base language, you incrementally modify the language by using facilities provided within the language.  That is, the new (extended) language is drawn out from the old (base) language, in which the new language had been latently present.  (Latin abs-, "out", and trahere, "pull/draw")  The terminology of layers of abstraction, in programming, goes back to the 1970s.  One also finds this use of abstraction in philosophy, for drawing out something latently present; here's a passage from Locke's 1689 An Essay Concerning Human Understanding (you may recognize this, as it's quoted at the front of the Wizard Book):

The acts of the mind, wherein it exerts its power over its simple ideas, are chiefly these three :  (1) Combining several simple ideas into one compound one ; and thus all complex ideas are made.  (2) The second is bringing two ideas, whether simple or complex, together, and setting them by one another, so as to take a view of them at once, without uniting them into one ; by which way it gets all its ideas of relations.  (3) The third is separating them from all other ideas that accompany them in their real existence : this is called abstraction : and thus all its general ideas are made.

Our programming-language use of the term abstraction does take a bit of getting used to, because we usually expect something abstracted to be smaller than what it was abstracted from.  The abstract of a paper is a short summary of it.  An abstract thought has left behind the details of concrete instances — though it seems the abstract thought may be somehow "bigger" than the more concrete thoughts from which it was drawn.  In our case, the extended language is probably equi-powerful with the base language, and therefore, even if some specific implementation details are hidden during extension, the two languages still feel as if they're the same size.  This is not really strange; recall Cantor's definition of an infinite set — a set whose elements can be put in one-to-one correspondence with those of a proper subset of itself.  Since we rarely work with finite languages, it shouldn't surprise us if we abstract from one language another language just as "big".

Ironically, though, the reason we're discussing this at all is that, despite our best efforts, the extended language is smaller than the base in the sense that its "envelope" of reachable extensions is smaller.  We'd really rather it weren't smaller.

What general principles govern radius of abstraction?  My first candidate is smoothness, a term I borrowed from M. D. McIlroy, one of the founders of the extensible languages movement.  I mean by it the property of a language that its abstractive facilities apply to the language in a free and uniform way.  This concept is also close kin to Strachey's first-class objects, and van Wijngaarden's orthogonality.  I proposed the following principle in my dissertation:

(Smoothness Conjecture)  Every roughness (violation of smoothness) in a language design ultimately bounds its radius of abstraction.

When a base language contains a defect of smoothness, I suggest, successive extensions magnify the defect, creating unbounded complexity that drags down the programmer.

The goal

The Smoothness Conjecture is a neat expression of a design priority shared by a number of programming language designers; but, looking at programming language designs over the decades, clearly many designers either don't share the priority, or don't agree on how to pursue it.

What, though, if we could develop a mathematical framework for studying the abstractive power of programming languages — a theory of abstraction.  One might then have an objective basis for discussing design principles such as the Smoothness Conjecture, that to date have always been largely a matter of taste.  I wouldn't expect the Smoothness Conjecture itself to be subject to formalization, let alone proof, at least not until the study of the subject reached quite a mature phase; but the Conjecture may inspire any number of more specific claims that could then be weighed objectively.

This, in my humble opinion, would be very cool and, as an added bonus, immensely useful.

It is not, however, a short-term goal.  For a ballpark estimate, say people have been pursuing abstractive power (under whatever name) since the founding of the extensible languages movement, circa 1960.  When I got into the game, it had already been going on for about three decades.  The more extreme OOP advocates were making claims for it that could have been lifted nearly verbatim from the more extreme extensibility advocates of two decades earlier, and by my assessment then (understandably unpopular with the OOP advocates) there was still more we didn't know than that we did.  I didn't expect to tie it all up quickly; but I'm still excited about the prospects, because every few years my thinking on it has moved (forward, I hope) slightly — and by my estimate of the difficulty, any progress at all is a very encouraging sign.

There is no semantics

Shortly after I started thinking on abstractive power, Matthias Felleisen's classic paper "On the Expressive Power of Programming Languages" was published (in the proceedings of ESOP '90), and I was encouraged by this evidence that I wasn't the only person in the world crazy enough to try to mathematize traditionally informal aspects of language design.  Felleisen's treatment has been quite a successful meme in the years since, and has some features of interest for abstraction theory — both features that apply to abstractive power, and features that offer insight because of why they don't apply to abstractive power.

Felleisen's expressiveness works roughly thus:  A programming language is a set of programs together with a partial mapping from programs to semantic values.  Language A can express language B if there is a simple way to rewrite B-programs as A-programs that preserves the overall pattern of semantics of programs — not only the semantic values of valid programs, but which programs are valid, i.e., halt and which are not valid/don't halt.  (In this case, the overall pattern of behavior is sufficiently captured by the pattern of halting/not-halting, so one might as well say there is just a single semantic value, or technically replace the "partial mapping from programs to semantic values" with a "subset of programs designated as halting".)

That is, A can express B when there exists a decidable function φ mapping each B-program p to an A-program φ(p) such that φ(p) halts iff p halts.  A can weakly express B when φ(p) halts if p halts (but not necessarily only if p halts).

How readily A can express B depends on how disruptively φ is allowed to rearrange the internal structure of p.  Felleisen's paper particularly focuses on the class of "macro", a.k.a. "polynomial", transformations φ, which correspond to Landin's notion of syntactic sugar.  Each syntactic operator σ in language B is replaced by a polynomial (a "macro", or "template") σ_φ in language A; thus,

φ(σ(e₁, ... e_n))  =  σ_φ(φ(e₁), ... φ(e_n))

When φ is of this form, one says A can macro-express B.

I described the criterion for A can express B as preserving the "overall pattern of semantics of programs".  I meant to suggest that this is more than each individual mapping p ↦ φ(p) preserving semantics; it involves preserving, across mapping φ, how the shape of program texts affects their semantics.  This preservation-of-shape is more apparent when considering macro-expressiveness, which demands similarities of program shape between p and φ(p), because this implies that the similarities and differences between φ(p₁) and φ(p₂) would be akin to the similarities and differences between p₁ and p₂; but it's not clear that polynomial/macro rewriting would be the only useful measure of similarity of program shape.  (Cf. Steele and Sussman's 1976 Lambda: The Ultimate Imperative.)  To explore more general aspects of expressiveness, one might parameterize the theory by what class of transformations are allowed.

In preparing for an analogous treatment of abstractiveness, the first thing to recognize is that while expressiveness views each program as inducing a semantic value, abstractiveness views each program as inducing a programming language.  When comparing two B-programs p₁ and p₂, we don't just ask whether they induce the same programming language, because they almost certainly do not.  Rather, we want to compare the induced programming languages to each other, probably using some measurement at least as sophisticated as expressiveness.

Consider what this means for the definition of programming language.  Picture a base language as the center of a web of languages connected by directed arrows —abstractions— each arrow labeled by a program text.  The whole thing is a sort of state machine, where the states are languages, the state transitions are abstractions, and the input "alphabet" is the set of program texts.  We could also integrate semantics into this model, by adding transitions labeled with reserved "observable" terms — and then there isn't really any need for the states of the machine at all.  Everything we could ever want to know about a given programming language is contained in the set of all possible sequences of labels on paths starting from that language; so we might as well define a language to be that set of sequences.  That is,

(D1)  A programming language over set of terms T is a set of sequences of terms P ⊆ T^* such that for all sequences of terms x and y, if xy ∈ P then x ∈ P.

This approach also appeals to the recognition that although computation theory tends to look only at computations that halt, a great many of our software processes are open-ended.

This purely syntactic, unbounded view of programming languages is foundational.  The expectation of halting — what one might call the terminal-semantic assumption — is ubiquitous:  the assumption, hardwired into one's core definitions, that a computation is meant to get an answer and stop.  Denotational semantics is a terminal-semantic model.  Theory of computation, and complexity theory, are founded on the terminal-semantic assumption.

To my mind, an essential difficulty with the terminal-semantic approach is that, patently, it prefers to disregard properties that relate to unbounded sequences of future developments.  Abstractive power is directly concerned with such sequences, but one suspects all computation really should take them into account, as most macroscopic software processes are interactive (in one or another sense) and open-ended rather than self-contained and merely producing a final result.  (Cf. Dina Goldin et al.)

The unbounded-syntax approach does not, of course, really "eliminate" semantics; but it does cause semantics to become a dependent concept, grounded in syntax.  For abstraction theory as I'm currently developing, semantics is a set of sequences of terms; in RAGs (from my master's thesis), semantics is a nonterminal symbol of a grammar.  (In a modern treatment of RAGs I'd be inclined to replace the term "metasyntax" with "co-semantics"; but I digress... sort-of.)

Note:  I've described RAGs in a later blog post, here.

The second derivative of semantics

The expressiveness of a programming language —what we ask φ to conserve when mapping B to A— is about the contours of the overall pattern of semantics of programs.  That is, it's about how variations in the text of a program change the semantics induced by the program; in short, expressiveness is the first derivative of semantics.

The abstractiveness of a programming language —which we will want conserved when we assert that one language is "as abstractively powerful" as another— is about how variations in the text of a program change the expressiveness of the language induced by the program.  Thus, as expressiveness looks at variations in semantics, and is in this sense the first derivative of semantics, abstractiveness looks at variations in expressiveness, and is thus the second derivative of semantics.

As I've set out to mathematize this, I've found the treatment becomes rather off-putting-ly elaborate (a trend I mean to minimize in this post).  I observe a lesser degree of the same effect even in Felleisen's paper, which was apparently trying to stick to just a few simple ideas and yet somehow got progressively harder to keep track of.  Some of this sort of thing is a natural result of breaking new ground:  appropriate simplifications may be recognized later.  I omitted one substantial complication from my description of Felleisen's treatment, that I suspect was simply a consequence of techniques he'd inherited from other purposes.  However, I've also introduced one new complication into expressiveness, namely parameterization by the class of transformations allowed — and I'm about to introduce a second complication, as I adapt Felleisen's treatment to my unbounded-syntax strategy.

Recasting expressiveness

In adapting expressiveness to the unbounded-syntax definition of programming language (D1), the first consideration is that a mapping φ between two languages of this sort has to respect the all-important prefix structure of the languages:

(D2)  For programming languages P and Q, a morphism from P to Q is a function φ : P → Q that preserves prefixes.

That is, for every xy ∈ P, there exists z such that φ(xy) = φ(x)z.  We write P/x for the language reached from language P by text sequence x ∈ P; and similarly, when φ : P → Q, we write φ/x for the corresponding morphism from P/x to Q/φ(x).  Thus,  P/x = { y | xy ∈ P }  and  φ(xy) = φ(x) (φ/x)(y).

As remarked earlier, we parameterize expressiveness relationships by the class of allowable morphisms.  We won't allow arbitrary classes of morphisms, though.

(D3)  A category (over programming languages with terms T) is a set C of morphisms between languages over T, closed under composition and including the identity morphism of each language over T.

For given terms T, some useful categories:

Any = category of all morphisms.
Map = category of morphisms that perform a term transformation uniformly, φ(t₁...t_n) = φ(t₁)...φ(t_n).
Macro = category of map morphisms whose term transformation is macro/polynomial.
Inc = category of inclusion morphisms, φ : P → Q with φ(x)=x
Id = category of identity morphisms, φ : P → P with φ(x)=x

Where Felleisen could avoid complicated semantic values by relying on halting behavior, we need a set of observable terms, O ⊆ T.

(D4)  Morphism φ : P → Q respects observables O if

• φ maps observables, and nothing else, into those same observables — that is, (φ/x)y=o iff y=o — and
• φ transforms each derived language into a language with exactly the same observables — that is, o∈(P/x) iff o∈(Q/φ(x)).

Morphism φ : P → Q weakly respects observables O if it satisfies all the conditions for respecting observables O except that o∈(P/x) implies o∈(Q/φ(x))  (rather than implication going both ways).

Obs_O = category of all morphisms that respect observables O
WObs_O = category of all morphisms that weakly respect observables O

Our basic expressiveness relation is then

(D5)  For category C and languages A and B,  A can C-express B for observables O if there exists φ : B → A with φ ∈ C ∩ Obs_O.

We say A is as C,O-expressive as B.  Weak C,O-expressiveness uses WObs_O in place of Obs_O.  Evidently, the as C,O-expressive as relation is transitive, as is its weak variant.  Expressiveness implies weak expressiveness (because Obs_O ⊆ WObs_O).

There is a simple theorem that the expressiveness relation is preserved if the category is made bigger, and if the set of observables is made smaller.  That is, if A is as C₁,O₁-expressive as B, category C₁⊆C₂, and observables O₂⊆O₁, then A is as C₂,O₂-expressive as B.

Note:  Although the notation here is simplified from the techreport, it still poorly handles the codomain of a derived morphism, producing such un-self-explanatory expressions as Q/φ(x).  Belatedly I see that by adopting for φ: P → Q the additional notation φ(P)=Q, one would have the more mnemonic φ/x : P/x → φ(P)/φ(x).

Abstractiveness

As expressiveness depends on φ : B → A preserving the semantic landscape of B, abstractiveness should depend on φ preserving the expressive landscape of B.  A semantic landscape for B arose from specifying a set of observables.  An expressive landscape for B arises from specifying a category of expressiveness morphisms by which to compare different languages B/x.

If it wasn't entirely certain what category to use when comparing expressiveness (hence the introduction of parameter C into the expressiveness relation, where Felleisen's treatment only looked at two choices of C), the choice of expressiveness category becomes much more obscure when considering abstractiveness.  Note in Standish's remark the phrase by modest amounts of labor; dmbarbour has remarked that multiple degrees of difficulty are of interest, and this suggests that no one choice of category will give us a full picture.  One might even imagine that a φ : B → A of one category would map expressive relations on B of a second category onto expressive relations on A of yet a third category.  The point is that, without prior experience with this mathematics, we have no clear notion which of the myriad imaginable relations we want to look at.  We hope that experience working with it may give us insight into what special case we really want, but meanwhile the endeavor seems to require a lot of parameters.  It would look rather silly to have an abstractiveness relation with, say, four parameters, so we redistribute the parameters by bundling the choice of expressive category with the language.

(D6)  A programming language with expressive structure over terms T is a pair A=〈S,C〉 of a programming language S over T with a category C over programming languages with terms T.

We call these expressive languages for short.  We may write seq(A) and cat(A) for the components of expressive language A.

For φ to preserve the expressive landscape from B to A is more involved than preserving the semantic landscape.  The expressive landscape of B=〈S,C〉 is a web of relations between languages derived from S.  Suppose g∈C with g : S/x → S/y.  Through φ : 〈S,C〉 → 〈R,D〉, derived languages S/x and S/y correspond to R/φ(x) and R/φ(y).  Moreover, we already have three morphisms between these four derived languages:

g : S/x → S/y
φ/x : S/x → R/φ(x)
φ/y : S/y → R/φ(y)

If only we had a fourth morphism h∈D with h : R/φ(x) → R/φ(y), we could ask these four morphisms to commute, h ∘ φ/x = φ/y ∘ g.

(D7)  For expressive languages P and Q,  a morphism from P to Q is a morphism φ : seq(P) → seq(Q) such that

• for all g ∈ cat(P) with g : seq(P)/x → seq(P)/y, there exists h ∈ cat(Q) with h ∘ φ/x = φ/y ∘ g, and
• for all x,y ∈ seq(P), if there is no g ∈ cat(P) with g : seq(P)/x → seq(P)/y, then there is no h ∈ cat(Q) with h : seq(Q)/φ(x) → seq(Q)/φ(y).

For category C and expressive languages A, B,  A can C-express B for observables O if there exists φ : B → A with φ ∈ C ∩ Obs_O.

Note:  I've corrected a typo in this definition:  the second condition read for all x,y ∈ seq(Q) rather than seq(P). (24 April 2014)

We say A is as C,O-abstractive as B; and weak C,O-abstractiveness uses WObs_O in place of Obs_O.  The as C,O-abstractive as relation (and its weak variant) is transitive, and is preserved by making C bigger or O smaller.  Abstractiveness implies weak abstractiveness (because, again, Obs_O ⊆ WObs_O).  The techreport proves several other rather generic theorems; for example, if A is as C,O-abstractive as B, and cat(A) respects observables O, then cat(B) respects observables O.

When the expressive languages get their expressive structure from the identity category, C,O-abstractiveness devolves to C,O-expressiveness.  That is, for all languages A and B, category C, and observables O,  〈A,Id〉 is as C,O-abstractive as 〈B,Id〉  iff  A is as C,O-expressive as B.

Test case

An obvious question at this point is, now that we've got this thing put together, does it work?  In the techreport, my sanity check was a test suite of toy languages, chosen to minimally capture the difference between a language in which local declarations are globally visible, and one in which local declarations can be private.  The wish list at the end of the techreport, of results to try for, was much more impressive — I targeted encapsulation of procedures; hygienic macros; fexprs; and strong typing — but the sanity check, as the only example thus far actually worked out in full detail, has some facets of interest.

In language L₀, records are declared with constant fields, and the fields can then be queried.  When a query occurs in a text sequence, the next text in the sequence reports the value contained in the queried field; these reports are the observable terms.  Language L_priv is identical except that individual fields may be declared "private"; private fields cannot be queried, though they can be used when specifying the value of another field in the same record.

It's easy to transform an L_priv text sequence into a valid L₀ sequence:  just remove all the "private" keywords from the field declarations.  This is a macro/polynomial transformation, and all the queries that worked in L_priv still work and give the same results in L₀.  Therefore, L₀ is weakly as Macro-expressive as L_priv.

Whether or not L₀ is as Macro-expressive as L_priv (without the "weakly" qualifier) depends on just how one sets up the languages.  Each query is a separate text in the sequence, and the only text that can follow a query is a report of the result from the query.  Expressiveness hinges on whether or not it is permissible to query a field that is not visible; and the reason this matters is that although strong expressiveness requires each derived language B/x map into a derived language A/φ(x) that has no extra observable terms, it does not require that there be no extra non-observable terms.  To see how this works, suppose u ∈ L_priv is a sequence of declarations, after which query q₁ is valid but q₂ attempts to query a private field.  Following u, the result of q₁ is r₁, and the result of q₂ would be r₂ if the field were made public.  Let v be the result of removing all "private" keywords from u.

In the techreport, a query is not permitted unless its target is visible.  Therefore, L_priv sequences include uq₁ and uq₁r₁, but not uq₂.  L₀ sequences include vq₁, vq₁r₁, vq₂, and vq₂r₂.  But expressiveness does not object to vq₂r₂ ∈ L₀ unless there is some x ∈ L_priv such that φ(x)=vq₂ but xr₂ ∉ L_priv.  Since there is no such x, the observable r₂ in vq₂r₂ causes no difficulty.  Although it is true that vq₂ ∈ L₀ even though uq₂ ∉ L_priv, this does not interfere with expressiveness because q₂ is not an observable.  The upshot is that in the techreport, L₀ is as Macro-expressive as L_priv.

Alternatively, one could allow queries regardless of whether they're valid; this is essentially a "dynamic typing" approach, where errors are detected lazily.  In that case, uq₂ ∈ L_priv; the allowance of the observable r₂ in L₀ is then a violation of strong expressiveness, and L₀ is not as Macro-expressive as L_priv (although it's still weakly as Macro-expressive).

What about Macro-abstractiveness?  Given the relative triviality of the languages, I chose to use weak category Inc for the expressive structure of the languages:  〈L₀,Inc〉 and 〈L_priv,Inc〉.  L₀ ⊆ L_priv, so using the inclusion morphism φ(x)=x from L₀ to L_priv, evidently 〈L_priv,Inc〉 is as Inc-abstractive as 〈L₀,Inc〉; and consequently, as a weaker result, 〈L_priv,Inc〉 is as Macro-abstractive as 〈L₀,Inc〉.

As for the other direction, we've already observed that L₀ is as Macro-expressive as L_priv, which is to say that 〈L₀,Id〉 is as Macro-abstractive as 〈L_priv,Id〉.  So if 〈L₀,Inc〉 isn't as Macro-abstractive as 〈L_priv,Inc〉, the difference has to be in the additional expressive structure.  This expressive structure gives us a g : L/x → L/y when, and only when, L/x ⊆ L/y.  Therefore, in order to establish (contrary to our intention) that 〈L₀,Inc〉 is as Macro-abstractive as 〈L_priv,Inc〉, we would have to demonstrate a Macro∩Obs_O morphism φ : L_priv → L₀ that preserves all of the subsetting relationships between derived languages in L_priv.

For example, the transformation remove-all-"private"-keywords, which gave us Macro-expressiveness, will not work for Macro-abstractiveness, because it washes out subsetting relationships.  Suppose u is a sequence of declarations in L_priv that contains some private fields, and v is the result of removing the "private" keywords from u.  Since v can be followed by some things that u cannot, L_priv/u is a proper subset of L_priv/v.  However, the remove-"private" transformation maps both of these languages into L₀/v, which evidently isn't a proper subset of itself; so remove-"private" doesn't preserve the expressive structure.

In fact, no Macro morphism will preserve the expressive structure.  Consider a particular private field declaration, call it d.  When d occurs within a record declaration in an L_priv sequence, it can affect later expansions of the sequence, through its use in defining other, non-private fields of the same record, changing the results of queries on those non-private fields.  The only thing that can affect later queries in L₀ is a field declaration; therefore, a Macro morphism φ must map d into one or more field declarations.  But if d is embedded in a record declaration that doesn't use it, it won't have any effect at all on later queries — and the only way that can be true in L₀ is if φ(d) doesn't declare any fields at all.  So there is no choice of φ that preserves the expressive structure (which is to say, the subsetting structure) in all cases.

So 〈L_priv,Inc〉 is strictly more Macro-abstractive than 〈L₀,Inc〉.