Friday, April 4, 2014

Why is beta-substitution like the Higgs boson?

"Why is a raven like a writing desk?"
"No, I give it up," Alice replied. "What's the answer?"
"I haven't the slightest idea," said the Hatter.
Alice's Adventures in Wonderland, Chapter 7, Lewis Carroll.

I'm always in the market for new models of how a system can be structured.  A wider range of models helps keep your thinking limber; the more kinds of structure you know, the more material you have to draw inspiration from when looking for alternatives to a given theory.

Several years ago, in developing vau-calculi, I noticed a superficial structural similarity between the different kinds of variable substitution I'd introduced in my calculi, and the fundamental forces of nature in physics.  (I mentioned this in an earlier blog post.)  Such observed similarities can, of course, be white noise; but it's also possible that both seemingly unrelated systems could share some deep pattern that gives rise to the observed similarity.  In the case of vau-calculi and physics, the two systems are so laughably disparate that for several years I didn't look past being bemused by it.  But just recently I was revisiting my interest in physics TOEs (that's Theory of Everything, the current preferred name, last I heard, for what colloquially used to be called Grand Unified Theory, and before that, Unified Field Theory), and I got to thinking.

This will take a bit of set-up, and the payoff may be anticlimactic; but given the apparent extreme difficulty of making progress in this area at all, I'll take what I can get.

Substitution in vau calculi
Theories of Everything
Hygienic physics
Substitution in vau calculi

Traditionally in λ-calculi, all variables are bound by a single construct, λ, and manipulated by a single operation, called substitution.  Substitution is used in two ways.

The major rearrangements of calculus terms take place in an action called β-rewriting, where a variable is completely eliminated by discarding its binding λ and replacing all references to it in the body of the old λ with some given argument.  The part about eliminating the old λ is just a local adjustment in the structure of the term; but the replacement of references is done by β-substitution, which is not localized at a particular point in the term structure but instead broadcast across the body (an entire branch of the term's syntax tree).  When you do this big β-substitution operation, you have to be careful.  A naive rule for substituting argument A for variable x in body B would be "replace every reference to x in B with A".  If you naively do that you'll get into trouble, because B might contain λs that bind either x, or some other variable that's referred to in A.  Then, by following that naive rule you would lose track of which variable reference is really meant to refer to which λ.  This sort of losing track is called bad hygiene.

To maintain hygiene during β-substitution, we apply α-renaming, which simply means that we replace the variable of a λ, and all the references to it, with some other variable that isn't being used for other purposes and so won't lead to confusion.  This is a special case of the same sort of operation as β-substitution, in which all references to a variable are replaced with something else; it just happens that the something else is another variable.  These two cases, β-substitution and α-renaming, are not perceived as separate functions, just separate uses of the same function — substitution.

It's possible to extend λ-calculus to encompass side-effectful behaviors — say, continuations and mutable storage — but to do so with well-behaved (technically, compatible) rewriting rules, you need some sort of bounding construct to define the scope of the side-effect.  In my construction of vau-calculus (a variant λ-calculus), I developed a general solution for bounding side-effects with a variable-binding construct that isn't λ, and operating the side-effects using a variable-substitution function different from β-substitution.  (Discussed here.)

I ended up with four different kinds of variables, each with its own substitution operation — or operations.  All four kinds of variables need α-renaming to maintain hygiene, though, and for the three kinds of side-effect variables, α-renaming is not a special case of operational substitution.  If you count each variable type's α-renaming as a separate kind of substitution, there are a total of nine substitution functions (one both α and operational, three purely α, and five purely operational).  λ-variables emerge as a peculiarly symmetric case, since they're the only type of variable whose substitutions (α and β) are commensurate.

This idea of multiple kinds of variables was not, btw, an unmixed blessing.  One kind of variable — environment variables — turned out to be a lot more complicated to define than the others.  Two kinds of variables (including those) each needed a second non-α substitution, falling into a sort of gray area, definitely not α-renaming but semi-related to hygiene and not altogether a full-fledged operational substitution.  The most awkward part of my dissertation was the chapter in which I developed a general theory of rewriting systems with multiple kinds of variables and substitution functions — and the need to accommodate environment variables was at the heart of the awkwardness.

Theories of Everything

Theoretical physics can be incredibly complicated; but when looking for possible strategies to tackle the subject, imho the only practical way to think about it is to step back from the details and look at the Big Picture.  So here's my take on it. 

There are, conventionally, four fundamental forces:  gravity, electromagnetism, the weak nuclear force, and the strong nuclear force.  Gravity was the first of these we got any sort of handle on, about three and a half centuries ago with Isaac Newton's law of universal gravitation.  Our understanding of electromagnetism dates to James Clerk Maxwell, about one and a half centuries ago.  We've been aware of the weak nuclear force for less than a century, and the strong nuclear force for less than half a century.

Now, a bit more than a century ago, physics was based on a fairly simple, uniform model (due, afaics, to a guy about two and a half centuries ago, Roger Joseph Boscovich).  Space had three Euclidean dimensions, changing with respect to a fourth Euclidean dimension of time; and this three-dimensional world was populated by point particles and space-filling fields.  But then in the early twentieth century, physics kind of split in two.  Two major theories arose, each of them with tremendous new explanatory power... but not really compatible with each other:  general relativity, and quantum mechanics. 

In general relativity, the geometry of space-time is curved by gravity — and gravity more-or-less is the curvature of space-time.  The other forces propagate through space-time but, unlike gravity, remain separate from it.  In quantum mechanics, waves of probability propagate through space, until observation (or something) causes the waves to collapse nondeterministically into an actuality (or something like an actuality); and various observable quantities are quantized, taking on only a discrete set of possible values.  These two theories don't obviously have anything to do with each other, and leave gravity being treated in a qualitatively different way than the other forces.

Once gravity has become integrated with the geometry of space-time — through which all the forces, including gravity, propagate — it's rather hard to imagine achieving a more coherent view of reality by undoing the integration already achieved in order to treat gravity more like the other forces.  As a straightforward alternative, various efforts have been taken to modify the geometry so as to integrate the other forces into it as well.  This is made more challenging by the various discrete-valued quantities of quantum mechanics, as the geometry in general relativity is continuous.  The phenomena for which these two theories were created are at opposite scales, and the two theories are therefore perceived as applying primarily at those scales:  general relativity to the very large, and quantum mechanics to the very small; so in attempting to integrate the other forces into the geometry, modification of the geometry tends to be at the smallest scales.  The two most recently-popular approaches to this are, to my knowledge, string theory and loop quantum gravity.

I've remarked in an earlier blog post, though, that the sequence of increasingly complex theories in physics seems to me likely symptomatic of a wrong assumption held in common by all the theories in the sequence (here).  Consequently, I'm in the market for radically different ways one might structure a TOE.  In that earlier post, I considered an alternative structure for physics, but I wasn't really looking at the TOE problem head-on; just observing that a certain alternative structure could, in a sense, eliminate one of the more perplexing features of quantum mechanics.

Hygienic physics

So here we have physics, with four fundamental forces, one of which (gravity) is somehow "special", more integrated with the fabric of things than the others are.  And we have vau-calculus, with four kinds of variables, one of which (λ-variables) is somehow "special", more integrated with the fabric of things than the others are.  Amusing, perhaps.  Not, in itself, suggestive of a way to think about physics (not even an absurd one; I'm okay with absurd, if it's different and shakes up my thinking).

Take the analogy a bit further, though.  All four forces propagate through space-time, but only gravity is integrated with it.  All four operational substitutions entail α-renaming, but only β-substitution is commensurate with it.  That's a more structural sort of analogy.  Is there a TOE strategy here?

Well, each of the operational substitutions is capable of substantially altering the calculus term, but they're all mediated by α-renaming in order to maintain hygiene.  There's really quite a lot more to term structure than the simple facets of it affected by α-renaming, with the quite a lot more being what the rewriting actions, with their operational substitutions, engage.  There is, nonetheless, for most purposes only one α-renaming operation, which has to deal with all the different kinds of variables at once, because although each operational substitution directly engages only one kind of variable, doing it naively could compromise any of the four kinds of variables.

Projecting that through the structural analogy, we envision a TOE in which the geometry serves as a sort of "hygiene" condition on the forces, but is really only a tangential facet of the reality that the forces operate on — impinging on all the forces but only, after all, a hygiene condition rather than a venue.  Gravity acts on the larger structure of reality in a way that's especially commensurate with the structure of the hygiene condition.

Suggestively, quantum mechanics, bearing on the three non-gravitational forces, is notoriously non-local in space-time; while the three kinds of non-λ variables mediate computational side-effects — which is to say, computational effects that are potentially non-local in the calculus term.

The status of gravity in the analogy suggests a weakness in the speculations of my earlier post on "metaclassical physics":  my technique for addressing determinism and locality seems to divorce all forces equally from the geometrical structure of reality, not offering any immediately obvious opportunity for gravity to be any more commensurate with the geometry than any other force.  I did mention above, that post wasn't specifically looking at TOEs; but still, I'm inclined to skepticism about an approach to fundamental physics that seeks to mitigate one outstanding problem and fails to suggest mitigation for others — that's kind of how we ended up with this bifurcated mess of relativity and quantum mechanics in the first place.  As I also remarked in that post when discussing why I suspect something awry in theoretical physics, while you can tell you're using an unnatural structure by the progression of increasingly complicated descriptions, you can also tell you've hit on the natural structure when subsidiary problems just seem to melt away, and the description practically writes itself.  Perhaps there's a way to add a hygiene condition to the metaclassical model, but I'd want to see some subsidiary problems melting.

Supposing one wants to try to construct a TOE, metaclassical or not, based on this strategy, the question that needs answering is, what is the primary structure of reality, to which the geometry serves a sort of tangential hygiene-enforcement role?  For this, I note that the vau-calculus term structure is just a syntactic representation of the information needed to support the rewriting actions, mostly (though not exclusively) to support the substitutions.  So, the analogous structure of reality in the TOE would be a representation of the information needed to support... mainly, the forces, and the particles associated with them.  What we know about this information is, thus, mainly encapsulated in the table of elementary particles.  Which one hopes would give us the wherewithal to encompass gravity — the analog to β-substitution — since it includes a mediating particle for mass:  the Higgs boson.

[Note: I've further explored the rewriting/physics analogy in a later post, here.]


  1. I've wondered about how to connect fundamental physics (TOE) to programming language theory (PLT). This is interesting.

  2. Nice post
    Get consultation, and best treatment for various neurological disorders & diseases from one of the best neurologist in Delhi Dr. Mukesh Kumar