Showing posts with label abstractive power. Show all posts
Showing posts with label abstractive power. Show all posts

Sunday, May 17, 2015

Numberless differentiation

The method described in I.3 resulted in an analogy between the "discrete" space of index values Z=(1,2,...) and the continuous state space Ω of the mechanical system[...].  That this cannot be achieved without some violence to the formalism and to mathematics is not surprising.
John von Neumann, Mathematical Foundations of Quantum Mechanics, trans. Robert T. Beyer, 1955, §I.4.

In this post, I mean to explore a notion that arose somewhat peripherally in an earlier post.  I noted that the abstractive power of a programming language is, in a sense, the second derivative of its semantics.  I've also noted, in another post, a curious analogy between term rewriting calculi and cosmological physics, which I used to inspire some off-the-wall thinking about physics.  So I've been wondering if the abstractive power notion might be developed into a formal tool for altogether non-numeric discrete systems akin to the continuous differential calculus that plays such a central role in modern physics.

Developing a mathematical tool of this sort is something of a guessing game.  One hopes to find one's way to some natural structure in the platonic realm of the mathematics, using whatever clues one can discern, wherever one finds them (be they in the platonic realm or elsewhere).

I've a story from my mother, from when she was in graduate school, about a student asking for motivation for something in an algebraic topology class.  The professor replied, when you build a beautiful cathedral you tear down the scaffolding.  To me, honestly, this always seemed to be missing the point.  You should keep a record of where the scaffolding was.  And the architectural plans.  And, while you're at it, the draft architectural plans.

Candidly, when I started this I did not know what I was expecting to find, and the path of reasoning has taken several unexpected turns along the way.  One thing I haven't found is a purely non-numeric discrete device analogous to continuous differential calculus; but I've got a plate full of deep insights that deserve their chance to be shared, and if the non-numeric discrete device is there to discover, it seems I must be closer to it than I started.

Contents
Discrete continuous physics
Differentiation in physics
Abstractiveness in programming
Causation in term rewriting
Draft analogy
Breaking the draft analogy
Retrenching
Discrete continuous physics

Physics has been struggling with the interplay of continuous and discrete elements for centuries (arguably since ancient times).  Continuous math is a clean powerful tool and therefore popular; on the face of it, one wouldn't expect to get nearly as much useful physics done with purely discrete structures.  On the other hand, our ordinary experience includes discrete quantities as well as continuous ones (recalling Kronecker's attributed remark, God made the integers; all else is the work of man).  Nineteenth-century classical physics reconciled continuous and discrete aspects by populating space with continuous fields and point particles.

The field/particle approach collapsed with quantum mechanics, which is commonly described as saying that various things appearing continuous at a macroscopic level turn out to be discrete at a very small scale.  I'd put it almost the other way around.  Our notion of discrete things comes from our ordinary, macroscopic experience, but evidently these macroscopic discrete things can be broken up into smaller things; and if we keep pushing this ordinary notion down to a sufficiently small scale, eventually it can't be pushed any further, and we end up having to postulate an underlying (non-observable) continuous wave function which, having been so-to-speak squashed as nearly flat as it can be, smears even supposedly discrete elementary particles into a continuous complex-valued field.  Which gives rise to discrete events by means of wave-function collapse, the ultimate kludge.  Wave-function collapse is a different way of reconciling continuous and discrete aspects of the theory, but tbh it feels a bit contrived.

In this view, howsoever we wandered into it, we've assumed a continuous foundation and sought to derive discreteness from the continuous substratum.  Traditional quantum theory derives discreteness by means of wave function collapse.  Some modern theories use the concept of a standing wave to derive discreteness; string theory does this, with closed loops vibrating at some overtone of their length, and the transactional interpretation does too, with waves propagating forward and backward in time between spacetime events and summing to a standing wave.

An alternative sometimes considered is that the foundation could be discrete — so-called digital physics.  I've some doubts about this, intuitively, because — how to put this — I don't think Nature likes to be neatly classified as "discrete" or "continuous".  I remember, in a long-ago brainstorming session with my father, posing the semi-rhetorical question, "what is neither discrete nor continuous?", to which he mildly suggested, "reality".  A purely discrete foundation seems as unlikely to me as a purely continuous one; in fact, it's possible the overly continuous character of the underlying wave function in quantum theory may be one subtle reason I'm not fond of that theory.

I have a particular, if round-about, reason for interest in the prospects for introducing some form of discrete, nonlocal, nonquantum element into physics.  I'd actually been thinking in this direction for some time before I realized why I was tending that way, and was rather excited to figure out why because it gives me a place to start looking for what kind of role this hypothetical discrete element might play in the physics.  My reasoning comes from, broadly, Mach's principle — the idea that the way the local universe works is a function of the shape of the rest of the universe.  (Mach's principle, btw, was given its name by Albert Einstein, who drew inspiration from it for general relativity.)

Suppose we want to study a very small part of the universe; say, for example, a single elementary particle.  This requires us either to disregard the rest of the universe entirely, or to assume the influence of the rest of the universe on our single particle is neatly summarized by some simple factor in our system, such as a potential field.  But quantum mechanics starts us thinking, somewhat at least, in terms of everything affecting everything else.  Suppose this is actually more so than quantum mechanics tells us.  Suppose our single particle is interacting nonlocally with the whole rest of the universe.  We don't know anything about these interactions with the rest of the universe, so their influence on our one particle is —for us— essentially random.  If it were all local and neatly summed up, we might try to ask for it to be described by a potential field of some sort; but since we're supposing this is nonlocal interaction, and we don't have any sort of nonlocal structure in our theory by which to describe it, we really can't do anything with it other than expect it to smear our probability distribution for our one particle.

This nonlocal interaction I'm talking about is presumably not, in general, the sort of nonlocal interaction that arises in quantum mechanics.  That sort of interaction, at least when it occurs within the system one is studying, is quantum entanglement, and it's really quite fragile:  at large scales it becomes very likely to decohere, its nonlocality breaking down under interactions with the rest of the universe.  I'm hypothesizing, instead, some more robust sort of nonlocality, that can work on a large scale.  From my reasoning above, it seems that as soon as we hypothesize some such robust nonlocal interaction, we immediately expect the behavior of our single-particle system to appear nondeterministic, simply because we no longer can have an undisturbed system, unless we consider the entire universe as a whole.  In contrast to the frequent presentation of quantum nondeterminism as "strange", under this hypothesis nondeterminism at small scales is unsurprising — though not uninteresting, because we may get clues to the character of our robust nonlocal interaction by looking at how it disturbs our otherwise undisturbed small system.

Following these clues is made more challenging because we have to imagine not one new element of the theory, but two:  on one hand, some sort of robust nonlocal interaction, and on the other hand, some local behavior that our small system would have had if the robust nonlocal interaction had not been present.  We expect the familiar rules of quantum mechanics to be the sum of these two elements.  I have already implied that the local element is not itself quantum mechanics, as I suggested something of quantum nondeterminism might be ascribed to the robust nonlocal element.  One might suppose the local element is classical physics, and our robust nonlocal interaction is what's needed to sum with classical physics to produce quantum mechanics.  Or perhaps, if we subtract the robust nonlocal interaction from quantum mechanics, we get something else again.

This also raises interesting possibilities at the systemic level.  The sum of these two hypothetical elements doesn't have to be quantum mechanics exactly, it only has to be close enough for quantum mechanics to be useful when looking only at a small system; so, quantum mechanics could be a useful approximation in a special case, rather as Newtonian mechanics is.  We may expect the robust nonlocal element to be significant at cosmological scales, and we may have misread some cosmological phenomena because we were expecting effects on that scale to be local.  But just at the moment my point is that, since spacetime is apparently our primal source of continuity, and our robust nonlocal interaction is specifically bypassing that continuity, I would expect the new interaction to be at least partly discrete rather than continuous; intuitively, if it were altogether continuous one might expect it to be more naturally part of the geometry rather than remaining "nonlocal" as such.

Differentiation in physics

We want a schematic sense of the continuous device we're looking for an analogy to.

Suppose 𝓜 is a manifold (essentially, a possibly-curved n-dimensional space), and F is a field on 𝓜.  The value of the field at a point p on 𝓜, Fp, might be a scalar (an ordinary number, probably real or complex), or perhaps a vector (directed magnitude); at any rate Fp would likely be some sort of tensor — but I'm trying to assume as little as possible.  So Fp is some sort of field value at p.

The derivative of F at p is... something... that describes how F is changing on 𝓜 at p.  If you know the derivative F ' of F at every point in 𝓜, you know the whole "shape" of F, and from this shape F ' you can almost reconstruct F.  The process of doing so is integration.  The process doesn't quite reconstruct F because you only know how F changes across 𝓜, not what it changes relative to.  This absolute reference for all of F doesn't change, across the whole manifold 𝓜, so it isn't part of the information captured by F '.  So the integral of F ' is, at least conceptually, F plus a constant.

By assuming just a bit more about the values of field F, we can see how to do more with derivative F ' than merely integrate it to almost-reconstruct F.  The usual supposition is that Fp is either a number (a scalar, continuous), or a number together with a configuration relative to the manifold 𝓜.  The idea here is that the configuration is a simple relationship to the manifold, and the number gives it "depth" (more-or-less literally) by saying "how big" is the configured entity.  The simplest such configured value is a vector:  a directed magnitude, where the direction on the manifold is the configuration, and the magnitude in that direction is the number.  One can also have a bivector, where the configuration, rather than a linear direction, is a two-dimensional plane orientation.  There's a more subtle distinction between vectors and covectors (in general, multivectors and comultivectors), which has to do with integration versus differentiation.  These distinctions of "type" (scalar, vector, covector, bivector, cobivector) are relatively crude; most of the configuration information is a continuous orientation, some variant of "direction".  And ultimately, we use the configurations to guide relations between numbers.  All that information about "shape" is channeled into numerical equations.

The continuity of the manifold comes into the situation in two ways.  One, already obliquely mentioned, is that the configuration of the field is only partly discrete, the rest of it (in all but the scalar-field case) being a sort of pseudo-direction on the manifold whose value is continuous, and interacts in some continuous fashion with the numerical depth/intensity of the field.  The other insinuation of manifold continuity into the continuous derivative is more pervasive:  the derivative describes the shape of the field at a point p by taking the shape in an ε-neighborhood of p in the limit as ε approaches zero.  The very idea of this limit requires that the neighborhood size ε (as well as the field intensity and probably the pseudo-direction) be continuous.

Abstractiveness in programming

The analogy needs a similar schematic of the discrete device.  Abstractiveness, in my treatment, is a relation between programming languages, in which some programming language Q is formally as abstractive as programming language P.

The basic structure on which the treatment rests is an abstract state machine, whose states are "languages" (ostensibly, programming languages), and whose transitions are labeled by texts.  The texts are members of a set T of terms generated over a context-free grammar; each text is treated as an atomic whole, so when we consider a sequence of texts, the individual texts within the sequence remain distinct from each other, as if T were the "alphabet" in which the sequence is written (rather than all the texts in the sequence being run together as a string over a more primitive alphabet).  Some subset of the texts are designated as observables, which are used to judge equivalences between programs.  In a typical interpretation, non-observable texts are units of program code, such as module declarations, while observable texts are descriptors of program output.

Everything that matters about a state of this abstract machine is captured by the set of text sequences possible from that state (a touch of Mach's principle, there); so formally we define each language to be the set of text sequences, without introducing separate objects to represent the states.  A language P is thus a set of text sequences, P ⊆ T*, that's closed under prefixing (that is, if xy ∈ P then x ∈ P).  We write P/x for the language reached from language P by text sequence x ∈ P; that is,  P/x = { y | xy ∈ P }.

These structures are used to define formally when one language "does" at least as much as another language.  The criterion is existence of a function φ : P → Q, also written φP = Q, that maps each text sequence x ∈ P to a text sequence φx ∈ φP such that φ preserves prefixes (φx is always a prefix of φxy) and φ also preserves some property of P understood as defining what it "does".  For language expressiveness, this additional preserved property is concerned with the observables, resulting in a formal statement that Q is at least as expressive as P.  For language abstractiveness, the additional preserved property is concerned with both observables and expressiveness relations between arbitrary P/x and P/y, resulting in a formal statement that Q is at least as abstractive as P.

The function φ is understood as "rewriting" P texts as Q texts; and the less intrusive this rewriting is, the more easily Q can subsume the capabilities of P.  For expressiveness, the class of macro (aka polynomial) transformations is traditionally of interest; operations that can be eliminated by this sort of transformation are traditionally called syntactic sugar.

Causation in term rewriting

Anyone with a bit of background in computer science has probably worked both with grammars and with term-rewriting calculi (though likely not in depth at the same time).  Have you thought about the contrast between them?  I hadn't, really, until I ended up doing a master's thesis formulating a novel grammar model (pdf), followed by a doctoral dissertation formulating a novel term-rewriting calculus (here).  Since I suspect grammars tend to be thought of with less, well, gravitas than calculi, I'll explain a bit of how the grammars in my master's thesis work.

The formalism is called RAGs — Recursive Adaptive Grammars.  Where an attribute grammar would have a terminal alphabet for syntax, a nonterminal alphabet for metasyntax (that is, for specifying classes of syntax), and various domains of attribute values for semantics, a RAG has a single unified domain of answers serving all three roles (except that for metasyntax I'll use the deeper name cosemantics).  A rule form looks like

v0,p0⟩  →  t1 ⟨p1,v1⟩ ... tn ⟨pn,vn⟩ tn+1
where each tk is a syntax string, and each ⟨•,•⟩ is a cosemantics/semantics pair suitable for labeling a parent node in a parse tree.  Conceptually, cosemantics is inherited, specifying how a tree can grow downward (the cosemantics on the root node is the "start symbol"); while semantics is synthesized, specifying the resultant meaning of the parsed string.  The vk are variables, provided from other parts of the tree:  cosemantics of the parent node, provided from above; and semantics of the children, provided from below.  The pk are polynomials, determined by the current rule from these variables, hence, from the cosemantics of the parent and semantics of the children.  (If the grammar is well-behaved, each child's cosemantics pk only uses variables v0,...vk−1, so there are no circular dependencies in the parse tree.)

Playing the role of the rule set of an attribute grammar, a RAG has a rule function ρ which maps each answer a into a set of rule forms ρ(a); in selecting answers for the variables in a rule form r (producing a rule instance of r), the inherited cosemantics v0 has to be some answer a such that r ∈ ρ(a).

If the polynomials were only allowed to construct answers, our grammars could recognize somewhat more than context-free languages; but we also want to compute semantics using Turing-powerful computation.  For this, I permitted in the polynomials a non-constructive binary operator — the query operator, written as an infix colon, •:•.  Conceptually, parsing starts with cosemantics, parses syntax, and in doing so synthesizes semantics; but in the usual grammatical derivation relation, cosemantics and semantics are both on the left side of the derivation, while syntax is on the right, thus:

⟨cosemantics, semantics⟩  ⇒+  syntax
The query operator rearranges these elements, because it has the meaning "find the semantics that results from this cosemantics on this syntax":
cosemantics : syntax  ⇒+  semantics
So we can embed queries in our rule forms, hence the "recursive" in "Recursive Adaptive Grammars".  However, I meant RAGs to be based on an elementary derivation step; so I needed a set of derivation step axioms that would induce the above equivalence.  My solution was to introduce one more operator — not permitted in rule forms at all, but used during intermediate steps in derivation.  The operator:  inverse, denoted by an overbar.

Imho, the inverse operator is elegant, bizarre, and cool.  What it does is reverse the direction of derivation.  That is, for any derivation step c1 ⇒ c2, we have another step c2 ⇒ c1.  The inverse of the inverse of any term c is just the same term c back again; and every answer a is its own inverse.  So, given any three answers a1, a2, and a3, if  ⟨a1,a2⟩ ⇒+ a3  then  a3 ⇒+ a1,a2 .

The whole derivation step relation is defined by four axioms.  We've already discussed the first two of them, and the third is just the usual rewriting property of compatibility:

  • If  c1 ⇒ c2  then  c2 ⇒ c1 .
  • If  ⟨a1,a2⟩ → a3 is a rule instance of r ∈ ρ(a1), then ⟨a1,a2⟩ ⇒ a3 .
  • If  c1 ⇒ c2 and C is a context in which the missing subterm isn't inside an inverse operator, then  C[c1] ⇒ C[c2] .
The fourth axiom is the spark that makes queries come alive.
  • a1 : a1,a2 ⇒ a2 .
So now, from  ⟨a1,a2⟩ ⇒+ a3  we can deduce by the first axiom  a3 ⇒+ a1,a2 , by the third axiom  a1 : a3 ⇒+ a1 : a1,a2 , and stringing this together with the fourth axiom,  a1 : a3 ⇒+ a2 . 

The converse, that  a1 : a3 ⇒+ a2  implies  ⟨a1,a2⟩ ⇒+ a3 , can also be proven without too much fuss... if one has already proven the basic result that an answer cannot be derived from another answer.  That is, if answer a is derived from c in one or more steps,  c ⇒+ a , then c is not an answer.  This would be trivial if not for the inverse operator, which allows an answer a to be the left-hand side of infinitely many derivations (the inverses of all derivations that end with a); the theorem says that once you've derived a, further derivation from there can't reach another answer.  It took me two rather messy pages to prove this in my master's thesis (simple proofs, if they exist, can take decades to find), and I realized at the time it was a sort of analog to the Church-Rosser theorem for a calculus — an elementary well-behavedness result that one really wants to prove first because without it one has trouble proving other things.

I didn't think more of it until, years later when explaining RAGs to my dissertation committee (though in the end I didn't use RAGs in my dissertation), I got to see someone else go through a WTF moment followed by an aha! moment over the virulent un-Church-Rosser-ness of RAGs.  Somehow it hadn't registered on me just how very like a term-rewriting calculus my RAG formalism might look, to someone used to working with λ-like calculi.  Mathematical systems are routinely classified according to their formal properties, but there's something deeper going on here.  RAGs, despite being in a meaningful way Turing-powerful, don't just lack the Church-Rosser property, they don't want it.  A λ-like calculus that isn't Church-Rosser is badly behaved, likely pathological; but a grammar that is Church-Rosser is degenerate.  It's a matter of purpose, which is not covered by formal mathematical properties.

My point (approached obliquely, but I'm not sure one would appreciate it properly if one didn't follow a route that offers a good view of the thing on approach) is that the purpose of a calculus is mainly to arrive at the result of an operation, whereas the purpose of a grammar is to relate a starting point to the usually-unbounded range of destinations reachable from it.  This requires us to think carefully on what we're doing with a discrete analog to the conventional continuous notion of differentiation, because when we take a conventional derivative, the thing we're differentiating is a single-valued function, akin in purpose to a calculus meant to produce a result, whereas when we describe expressiveness/abstractiveness as derivatives of semantics, the thing we're differentiating appears, on the face of it, to be very like a grammar, describing a usually-unbounded network of roads departing from a common starting point.

Draft analogy

As foundation for a notion of discrete differentiation, we're looking for a useful correspondence between elements of these two kinds of structures, continuous and discrete.  So far, it might seem we've identified only differences, rather than similarities, between the two.  Continuous differentiation is necessarily in the "calculus" camp, abstractiveness/expressiveness necessarily in the "grammar" camp.  Continuous differentiation at a point p is fundamentally local, depending in its deepest nature on a family of ε-neighborhoods of p as ε varies continuously toward zero.  Abstractiveness/expressiveness of a language P is fundamentally global, depending in its deepest nature on a family of languages reachable from P by means of (in general, unbounded) text sequences.  The local structure of the continuous case doesn't even exist in the discrete case, where language P has a set of closest neighbors; and the global structure on which the discrete case depends is deliberately ignored by the continuous derivative.

A starting point for an analogy is hidden in plain sight (though perhaps I've given it away already, as I chose my presentation to set the stage for it).  Recall again Mach's principle, that the way the local universe works is a function of the shape of the rest of the universe.  Wikipedia offers this anecdote for it:

You are standing in a field looking at the stars. Your arms are resting freely at your side, and you see that the distant stars are not moving. Now start spinning. The stars are whirling around you and your arms are pulled away from your body. Why should your arms be pulled away when the stars are whirling? Why should they be dangling freely when the stars don't move?
(One is reminded of the esoteric principle "as above, so below".)

In our continuous and discrete cases, we have two ways to examine the properties of a global structure at a particular location (p or P), one of which draws on an unbounded family of ε-neighborhoods approaching arbitrarily close, and the other on an (in general) unbounded family of discrete structures receding arbitrarily far.  Either way, we derive our understanding of conditions at the particular location by aggregating from an unbounded, coherent structure.  One might call the two strategies "unbounded locality" and "unbounded globality".  If we accept that the way the local universe works and the global structure of the universe are two faces of the same thing, then these strategies ought to be two ways of getting at the same thing.

This strategic similarity is reassuring, but lacks tactical detail.  In the continuous case, field F gave us a value at point p, the derivative gave us another field with again a value at p, and we could keep applying the differentiation operation (if F was sufficiently well-behaved to start with) producing a series of higher-derivative fields, each providing again a value at p.  Yet in the discrete case we don't appear to have a local "value" at P, the purely local "state" being so devoid of information that we actually chose to drop the states from the formal treatment altogether; and while we may intuit that expressiveness is the derivative of semantics, and abstractiveness the derivative of expressiveness, the actual formalisms we constructed for these three things were altogether different from each other.  The semantics apparently had only the text sequences, set of observables, and a (typically, infinite) discrete structure called a "language"; expressiveness added to this picture functions between languages; and abstractiveness augmented each language with a family of functions between the different nodes within each language, then defining functions between these "languages with expressive structure".  On the face of it, this doesn't appear to be a series of structures of the same kind (as fields F, F ', F '' are of the same kind, granting we do expect them to vary their configurations in some regular, generalizable way).

In my treatment of abstractive power, though, I noted that if, in augmenting languages P and Q with "expressive structure", the family of functions we use is the degenerate family of identity functions, then the relation "〈Q,Id〉 is as abstractive as 〈P,Id〉" is equivalent to "Q is as expressive as P".  This, together with Mach's principle, gives us a tactical analogy.  The underlying "state machine", whose states are languages and whose transitions are labeled by program texts, corresponds to manifold 𝓜.  A particular state, taken together with the rest of the machine reachable from that state, corresponds to point p of the manifold.  An "expressive structure" overlain on the machine, creating a web of functions between its states, corresponds to a field F (or F ', etc.).  Differentiation is then an operation mapping a given "field" (overlying web of functions) to another.  Thus, starting with our discrete machine 𝓜, overlaying the family of identity functions gives us the semantics of 𝓜, differentiating the semantics gives 𝓜's expressive structure, differentiating again gives its abstractive structure.

This analogy provides a way for us to consider the various parts of our discrete scheme in terms of the major elements of the continuous scheme (manifold, field, point).  But on closer inspection, there are a couple of flaws in the analogy that need to be thought out carefully — and these flaws will lead us to a second philosophical difference comparable in depth to the difference between grammars and term-rewriting calculi.

Breaking the draft analogy

One mismatch in the analogy concerns the difference in substance between 𝓜 and F.  In the continuous case, manifold 𝓜 consists entirely of the oriented distances between its points (we know the distances themselves are numbers because they are the ε needed for differentiation).  If you start with a field F of uniform value across 𝓜, and take its integral, you can reconstruct 𝓜.  The key point here is that 𝓜 and F are made of the same "stuff".  In our discrete scheme, though, 𝓜 is a state machine with term-labeled transitions, while F is a family of functions between term sequences.  The discrete 𝓜 and F are concretely different structures, made of different "stuff" rather than commensurate in the manner of the continuous 𝓜 and F.  It might not be immediately obvious what the consequences would be of this analogy mismatch; but as happens, it feeds into the second mismatch, which is more directly concerned with the practical use of derivatives in physics.

The second mismatch concerns how the manifold changes over time — or, equivalently, its curvature.  Our main precedent here is general relativity.

In general relativity, mass warps the space near its position, and the resulting curvature of space guides the movement of the mass over time.  It's not apparent that abstractiveness/expressiveness has anything analogous to time in this sense.  It should be apparent, though —once one takes a moment to consider— that general relativity doesn't have absolute time either.  Observers moving relative to each other will disagree in their perceptions of time, and of space, and of which observed events are and are not simultaneous; so rather than absolute time and space, we have four-dimensional spacetime that looks different to different observers.  Thinking of spacetime as a whole, rather than trying to factor it into absolute space and time, a particle with mass traces a one-dimensional curve across the four-dimensional manifold of spacetime.  When we said, a moment ago, that the mass's position warps space while space guides the mass's movement, this mutual influence is described by mathematical equations involving the manifold 𝓜 and fields F, F ', etc.  These equations are all about numbers (which don't occur in our discrete scheme) and rely on the fact that the manifold and the fields are both made out of this same numeric stuff (which they aren't in our discrete scheme).  Evidently, the key element here which we have failed to carry across the analogy is that of equations encompassing both 𝓜 and F.

But, when we look more closely to try to find a discrete element to support an analogy with the continuous equations, we find that the omission is after all something more primal than numbers, or even commonality of substance between 𝓜 and F.  The omission is one of purpose.  In the continuous case, the purpose of those equations is to enable us to solve for 𝓜 and F.  But the discrete device has no interest in solving for 𝓜 at all.  We don't use our theories of expressiveness and abstractiveness to define a language; we only use them to study languages that we've devised by other means.

Retrenching

At this juncture in the narrative, imho we've done rather well at reducing the question of the analogy to its essence.  But we still don't have an answer, and we've exhausted our supply of insights in getting this far.  We need more ammunition.  What else do we know about these continuous and discrete schemes, to break us out of this latest impasse?

For one thing, the asymmetric presence of solving in the continuous scheme is a consequence of a difference in the practical purposes for which the two mathematical schemes were devised.  In physics, we try to set up a mathematical system that matches reality, and then use the math to translate observations into constraints and, thus, predictions.  Solving is the point of the mathematical exercise, telling us what we should expect to deduce from observations if the theory is correct.  Whereas in expressiveness/abstractiveness, we consider various possible programming languages —all of which are of our own devising— and study the different consequences of them.  Rather than trying to figure out the properties of the world we're living in, we study the properties of different invented worlds in hopes of deciding which we'd like to live in.

The difference goes deeper, though.  Even if we did want to solve for state machine 𝓜 in the discrete scheme —in effect, solve for the programming language— we wouldn't find expressiveness/abstractiveness, nor even semantics, at all adequate to the task.  Recall from the above account of the continuous scheme, when observing that 𝓜 and F are made of the same "stuff", I suggested that from F one might reconstruct 𝓜.  Strange to tell, when I wrote that, I wasn't even thinking yet in terms of this gap in the analogy over solving for 𝓜 (though, obviously, that's where my reasoning was about to take me).  There is nothing in manifold 𝓜 that's in any fundamental way more complicated than fields F etc.  In stark contrast to the discrete case.  Expressiveness/abstractiveness are constructed from families of functions over 𝓜; to the extent semantic/expressive/abstractive comparisons are anything more than directed graphs on the states of 𝓜, their complexity is an echo of a deliberately very limited part of the structural complexity latent in 𝓜 itself.  While the internal structure of a programming language —state machine 𝓜 itself— is immensely complicated; tbh, it seems way more complicated than a mere space-time manifold, which is a continuum whereas a programming language is discontinuity incarnate.

The point about discontinuity recalls a key feature of the other analogy I drew, in my earlier post, between cosmological physics and term rewriting.  Under that analogy, fundamental forces in physics corresponded to substitution functions in term-rewriting; while physical geometry, with its close relation to the gravitational force, corresponded to α-renaming, with its close relation to λ-substitution.  In our current analogy, we've been treating continuity, with its role in ε-neighborhoods, as the defining feature of the manifold, and finding nothing like it in the syntactic complexity of a programming language.  What if for purposes of solving, what we need is not so much continuity as geometry?

For this, we need to find something α-renaming-like in the discrete scheme, which is challenging because expressiveness/abstractiveness is not based on term-rewriting.  There's more to it, though.  Whatever-it-is, α-renaming-like, we mean to be the analog to the manifold.  In other words, it's the discrete 𝓜.  And since the whole programming language, or equivalently the state machine, evidently isn't α-renaming-like, 𝓜 isn't the programming language after all, but something else.  Some facet of the programming language.  And not just any facet — one that guides our discrete differentiation analogously to how the geometry of the manifold guides continuous differentiation.

Friday, December 20, 2013

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,

φ(σ(e1, ... en))  =  σφ(φ(e1), ... φ(en))
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 φ(p1) and φ(p2) would be akin to the similarities and differences between p1 and p2; 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 p1 and p2, 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, φ(t1...tn) = φ(t1)...φ(tn).
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).
ObsO = category of all morphisms that respect observables O
WObsO = category of all morphisms that weakly respect observables O
Our basic expressiveness relation is then
(D5)  For category C and languages A and BA can C-express B for observables O if there exists φ : B → A with φ ∈ C ∩ ObsO.
We say A is as C,O-expressive as B.  Weak C,O-expressiveness uses WObsO in place of ObsO.  Evidently, the as C,O-expressive as relation is transitive, as is its weak variant.  Expressiveness implies weak expressiveness (because ObsO ⊆ WObsO).

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 C1,O1-expressive as B, category C1C2, and observables O2O1, then A is as C2,O2-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 gC 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 hD 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, BA can C-express B for observables O if there exists φ : B → A with φ ∈ C ∩ ObsO.
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 WObsO in place of ObsO.  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, ObsO ⊆ WObsO).  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 L0, 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 Lpriv 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 Lpriv text sequence into a valid L0 sequence:  just remove all the "private" keywords from the field declarations.  This is a macro/polynomial transformation, and all the queries that worked in Lpriv still work and give the same results in L0.  Therefore, L0 is weakly as Macro-expressive as Lpriv.

Whether or not L0 is as Macro-expressive as Lpriv (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 ∈ Lpriv is a sequence of declarations, after which query q1 is valid but q2 attempts to query a private field.  Following u, the result of q1 is r1, and the result of q2 would be r2 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, Lpriv sequences include uq1 and uq1r1, but not uq2L0 sequences include vq1, vq1r1, vq2, and vq2r2.  But expressiveness does not object to vq2r2 ∈ L0 unless there is some x ∈ Lpriv such that φ(x)=vq2 but xr2 ∉ Lpriv.  Since there is no such x, the observable r2 in vq2r2 causes no difficulty.  Although it is true that vq2 ∈ L0 even though uq2 ∉ Lpriv, this does not interfere with expressiveness because q2 is not an observable.  The upshot is that in the techreport, L0 is as Macro-expressive as Lpriv.

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, uq2 ∈ Lpriv; the allowance of the observable r2 in L0 is then a violation of strong expressiveness, and L0 is not as Macro-expressive as Lpriv (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:  〈L0,Inc〉 and 〈Lpriv,Inc〉.  L0 ⊆ Lpriv, so using the inclusion morphism φ(x)=x from L0 to Lpriv, evidently 〈Lpriv,Inc〉 is as Inc-abstractive as 〈L0,Inc〉; and consequently, as a weaker result, 〈Lpriv,Inc〉 is as Macro-abstractive as 〈L0,Inc〉.

As for the other direction, we've already observed that L0 is as Macro-expressive as Lpriv, which is to say that 〈L0,Id〉 is as Macro-abstractive as 〈Lpriv,Id〉.  So if 〈L0,Inc〉 isn't as Macro-abstractive as 〈Lpriv,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 〈L0,Inc〉 is as Macro-abstractive as 〈Lpriv,Inc〉, we would have to demonstrate a MacroObsO morphism φ : Lpriv → L0 that preserves all of the subsetting relationships between derived languages in Lpriv.

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 Lpriv 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, Lpriv/u is a proper subset of Lpriv/v.  However, the remove-"private" transformation maps both of these languages into L0/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 Lpriv 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 L0 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 L0 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 〈Lpriv,Inc〉 is strictly more Macro-abstractive than 〈L0,Inc〉.

Saturday, June 4, 2011

Primacy of syntax

One of the most influential papers in the history of computer science is Christopher Strachey's 1967 "Fundamental Concepts in Programming" — lecture notes for the International Summer School on Computer Programming, Copenhagen.  Christopher Strachey basically created the academic subject of programming languages, and in those lecture notes you will find many core concepts laid out.  First-class objects.  Left-values and right-values.  Polymorphism.  And so on.

Although Strachey did write a finished version of the lecture notes for publication in the proceedings of the summer school, those proceedings never materialized — so copies of the lecture notes were passed from hand to hand.  (The modern name for such a phenomenon is "going viral", but it's surely been happening since before writing was invented.)  Finally, on the twenty-fifth anniversary of Strachey's untimely death, the finished paper was published.

By that time, though, I'd spent over a decade studying my cherished copy of the raw lecture notes.  The notes consist largely of abbreviated, even cryptic, non-sentences, but their pithy phrases are often more expressive than the polished prose of the published paper — and sometimes the ideas candidly expressed didn't even make it into the published paper.  A particular item from the lecture notes, that has stuck with me from the first moment I read it (about a quarter century ago, by now) is
Basic irrelevance of syntax and primacy of semantics.
This seems to me to neatly capture an attitude toward syntax that became firmly rooted in the late 1960s, and has scarcely been loosened since.  My own passion, though, within the academic subject Strachey created, is abstraction; and from my first explorations of abstraction in the late 1980s, it has seemed to me that abstraction defies the separation between syntax and semantics.  Sometime during the 1988/89 academic year, I opined to a professor that the artificial distinction between syntax and semantics had been retarding the development of abstraction technology for over twenty years — and the professor I said it to laughed, and after a moment distractedly remarked "that's funny" as they headed off to their next appointment.  Nonplussed by that response (I was still rather in awe of professors, in those days), to myself alone I thought, but I wasn't joking.

Abstraction

A source code element modifies the language in which it occurs.  Starting, say, with standard Java, one introduces a new class, and ends up with a different programming language — almost exactly like standard Java, but not quite because it now has this additional class in it.  That is abstraction, building a new language on top of an old one.
Abstraction:  Transformation of one programming language into another by means of facilities available in the former language.
What makes it abstraction, rather than just an arbitrary PL transformation, is that it uses the facilities of the pre-existing programming language.  (For those who prefer to trace their definitions back a few centuries, the key requirement that the new language be latent in the old —that it be drawn out of the old, Latin abstrahere— appears in John Locke's account of abstraction in his An Essay Concerning Human Understanding; the relevant passage is the epigraph at the top of Chapter 1 of the Wizard Book — and is also the epigraph at the top of Chapter 1 of my dissertation.)

An abstractively powerful programming language is, by my reckoning, a language from which one can abstract to a wide variety of other languages.  The precise formalization of that is a subtle thing; and worthy of a blog entry of its own, especially since my formal treatment of it, WPI-CS-TR-08-01, gets rather dense in some parts.  For the current entry, though, we don't need those details; the key point here is that the result of the abstraction is another language.  This is in contrast to the denotational approach to programming languages (which Strachey helped create, BTW, and which is visible in nascent form in the 1967 lecture notes):  denotationally, the programming language is essentially a function which, when applied to a source-code term, produces a semantic value of another sort entirely.
[Note:  I've since written an entry on abstractive power.]
The idea that semantic results are languages is a very powerful one.  The results of computations (and any other embellishment one wants) can be modeled by introducing additional sorts of terms that may occur in languages; the significance of each language is then fully represented by the possible sequences of terms that can follow from it.  But then, one doesn't really need the explicit semantics at all.  Only the sequences of terms matter, and one can define a programming language by a set of sequences of terms.  At that point, one could say that all semantics is being represented as syntax (which is a truism about semantics, anyway), or one could just as well say that semantics has vanished entirely to be replaced with pure syntax.

Lisp and syntax

Lisp has been described as a language with no syntax.  There is a sense in which that's true:  if by "syntax" one means "syntax for representing programs rather than data".  In primordial S-expression Lisp, the only syntax exclusively represents data.  (The way that happened —to remind— was that McCarthy had originally envisioned a second kind of syntax, M-expressions, representing programs, but he'd also described an algorithm for encoding M-expressions as S-expressions.  He expected to have years in which to polish details of the language since writing a compiler was then understood to be such a colossal undertaking, but in the meantime they were hand-coding specific Lisp functions — and then S.R. Russell hand-coded eval, and abruptly they had a working interpreter for S-expression Lisp.)

I believe, by the way, this is how Lisp should be taught to novices:  Teach them S-expression syntax first, set it firmly in their minds that such expressions are data, and only after that begin to teach them about evaluation.  Mike Gennert and I tried this approach with a class back in the spring semester of 1999/2000.  Over the duration of the course, we led the students through writing a Scheme interpreter in Java, starting with a level-0 "REPL" loop that was missing the "E" — it would read in an S-expression, and just write it out without evaluating it.  By the end of the term we'd added in proper tail recursion.  The experiment as a whole wasn't as successful as we'd hoped, because at the moment we tried it, the department's curriculum was in a state of flux, and many of the students didn't already know Java; but we didn't have the sorts of problems I've seen, or heard others describe, due to novice students failing to think in terms of evaluating S-expressions.

The connection to abstraction is immediate and compelling.  Abstraction is all about specifying how syntax will be used for subsequent program code, and the design of Lisp is focused on virtuoso manipulation of the very type of data structure (S-expressions) that is effectively the syntax of program code.  The more power Lisp gives the programmer to control how syntax will be interpreted, the more abstractive power accrues.  Since fexprs greatly expand the programmer's direct control over the interpretation-time behavior of the evaluator (short of the "throw everything out and start over" tactic of running a meta-circular evaluator — a tactic that lacks stability), fexprs should massively increase the (already formidable) abstractive power of Lisp.  That's why the subtitle of my dissertation is $vau: the ultimate abstraction.

Note: Polymorphism

Strachey's 1967 lecture notes are most known —and cited— for coining the term polymorphism.  Therein, he divided polymorphism into two forms:  parametric polymorphism, and ad hoc polymorphism.

The parametric/ad hoc distinction struck me as a logical bipartition of polymorphism; that is, every possible form of polymorphism would necessarily be either parametric or ad hoc.  Evidently Cardelli and Wegner did not interpret Strachey this way; their taxonomy placed "inclusion polymorphism" outside of both parametric and ad hoc.

It also strikes me that the name ad hoc reflects real disapproval.  This goes back to the "basic irrelevance of syntax" remark.  At heart, parametric polymorphism is semantic, ad hoc is syntactic; one might be tempted to call them "semantic polymorphism" and "syntactic polymorphism", or even "good polymorphism" and "bad polymorphism".  There is a close connection between my perception that parametric/ad hoc reflects semantic/syntactic, and my perception that parametric/ad hoc was meant to be exhaustive.

Although I expect parametric polymorphism should have greater abstractive power than ad hoc polymorphism, I don't like biasing terminology.  I'd like to see any formal results stand on their own merits.  So, years ago, I looked for an alternative to "ad hoc".  The best I came up with at the time:  selection polymorphism.