Went in for day surgery this morning to repair a torn tendon. I expected to have a pretty well useless right arm for a week or so until everything healed up. I hadn't expected to be conpletely fuzzy-headed.

-- hendrik

My new walker

Tuesday afternoon I tripped and fell at home. I injured my right leg. Although I could still hobble a bit then, trying to get to French class was no longer an option.

Gwen thinks it's probably soft tissue damage, and not a broken bone.

Wednesday morning, trying to go anywhere was no longer an option. Gwen went out and got me a walker. Since then, I've been able to use the walker to get to the bathroom.

I'm trapped on the second floor of the house until my leg gets better.

-- hendrik

An example why verified programming is hard.

Walking back from where I parked my car today, I realized how difficult it is to make sure specifications are satisfied, once you start looking at them formally. There are specifications with obvious meanings, and obvious algorithms to satisfy them. But ...

After passing the hospital front door, I decided to park in the first available space. The obvious way to do this is to keep driving until I see an available space, and then park in it. But, when I'm finally parking in that space, is it the first available space? Can I know that? When I walked back to the hospital, I saw another available space. It hadn't been available when I drove past it. Was it there when I entered my parking space? I have no idea.

Now this is everyday trivia. But if something like this were to happen in a computer program, and other formal reasoning depended on getting into the first available space, things might get difficult. Would I have to make the specifications weaker? Would I have to make it precise in a complicated way? Would I have to change other code that depended on the details of the spec I could not implement?

Formal verification is hard. Informal verification is impossible. We resort to debugging, and our systems are are vulnerable to attack.

(no subject)

I heard on Friday that my brother Willlem, who lived in Winnipeg, had died. So I've gone off to Winnipeg for a week to do what I can to help settle his affairs and organize a memorial service. It's keeping me pretty busy.

-- hendrik

quantum mechanics and topos theory

I can't say I understand very much of it, but The Physical Interpretation of Daseinisation seems to present a formulation of quantum mechanics in which there's a true state space for quantum systems, which provides actual states for the system to actually be in, independent of any measurements we might want to perform on them. It then identifies classical perspectives on this state space, which represent various ways they might be measured. It turns out that this new formulation gives us an ordinary constructive logic instead of the rather intractible quantum logics theoreticians have been struggling with so far. The nice thing about constructive logics is that it's actually possible to do deductions in them, which seems not to be possible in the so-called quantum logics.

For those up to some heavy mathematics, it's neat stuff.

-- hendrik

Project Xanadu

I've just encountered project Xanadu, which seems to have been the original attempt at a true hypertext system -- or at least, one of the early, visionary ones. It seems still to be alive, and its web site and its Australian affiliate have some interesting ideas and critiques of the present web.

Algol 68 compiler

About 40 years ago I had been writing an Algol 68 compiler. I started it at the University of Alberta. It wasn't finished after I spent about two and a half years on it, and I decided that was enough. I has essentially a complete, functioning front end, and a fairly incomplete draft of a code generator. The whole thing was written in Algol W.

When I moved to the Mathematical Centre in Amsterdam it didn't take long for one of its directors to get wind of the incomplete compiler. He had access to an IBM 370, which was compatible with the machine I had first implemented on, so he prevailed on me to resume work on it. I agreed. I now look at that as a mistake. The facilities available weren't as good as they had been in Alberta (TSO instead of MTS, which meant slow turnaround whether I took the train to Delft every day of stayed in Amsterdam and used a 300 bps phone line.) Over the next few years I got the compiler to the point that it correctly handled about half the test set, but it really wasn't ready for serious use.

Then funding ran out, I left the Netherlands, and after that I had essentially no opportunity to continue work on it. Perhaps I could have reimplemented Algol W and then rewrote the code generator for another machine, but in new jobs I had other responsibilities.

Still, I have spent occasional sleepless nights wondering how I *should* have gone about this project.

The first thought is that I should have *started* with the code generator and the inner run-time system (garbage collection, stack management, and the most primitive I/O). There were lots of people writing front ends for Algol 68 compilers. I might have been able to glue someone else's front end to my back end if I had gone in that direction.

The second thought is that I should have gone to complete machine-independence early, rather than late. Algol W might have been a machine-independent language (or close enough to it), but it had been implemented only on the IBM 360 (and therefore also 370), and it was a much bigger language than I needed.

But the real trick is how could I have best gone about that, given the state of the art back in the early 70's when I started the thing.

I now see there were a number of options.

First start in Algol W, as I had, but implementing a small language, possibly a very small Algol 68 sublanguage, that had just the features necessary for writing a compiler. Then rewrite that compiler in its own language, taking care to produce a suitable intermediate code.

(Moving that to a new machine would involve writing a new code generator from the intermediate code, using whatever tools were available on the target machine. Ideally, the intermediate code would have enough redundancy that it could be interpreted as easily as compiled. Ideally, the intermediate code would be word-size-independent, but even if it weren't, it would still be possible to interpret it.).

The small language would have as data types unions, structs, integers, characters, references, and procedures. Most coercions would have to be explicitly coded. There would be no operator or priority declarations, There would probably be other restrictions like this in the direction of explicitness, including a few extra keywords to simplify parsing in places where the Algol 68 is almost, but not quite, ambiguous.

Full type-checking would still be done.

Making these restrictions would cut out a moderate amount of lexical scanner, vastly simplify the context-free parser, wipe out most of the coercion pass, and leave much of the final code-generator and the run-time garbage-collector intact. And this would probably have cut a year or more off total development time (measured in terms of MTS development time, not TSO development time). The system might very well have been machine-independent within two years. Although it wouldn't have been an Algol 68 compiler, it would have been well on the way, and development could have continued on almost any machine. No long-distance phone calls to Delft's computer would have been needed.

There are quite a few techniques I can know of now that might have further accelerated development if they had been known back then. But none of what I've described above involved any technologies I was unfamiliar way back in the early 70's. I could have made the decisions I've just described way back then, except for one important fact:

Back then I lacked the wisdom to go about it this way. The wisdom to get something usable working as soon as possible as opposed to the complete thing sometime later.

-- hendrik

cancelled TV

I wonder if the propensity of networks to cancel potentially long-running, coherently plotted series during the first season is inhibiting people from starting to watch them, thereby exacerbating the problem.

Multidimensional time

Multidimensional time

In which the author probably reveals his ignorance about quantum mechanics,


A little knowledge is a dangerous thing

So it turns out, in Kaluza-Klein theory, it's quite easy to unify electromagnetics and gravity relativistically. And the math is beautiful. So beautiful as to be quite convincing, except for one detail. The theory needs five-dimensional space-time. Where's the extra dimension? Did it go AWOL on a binge in the local bar? I can't really point to a fourth spatial dimension sitting here in my dining room, and, as one physicist put it, he "can't imagine what a universe with two temporal dimensions would be like."

Not only that, but the string theorists have expanded the number of dimensions to ten, or eleven. Didn't I once hear twenty-four? Not only are string-theoretical calculations impossibly difficult for the current generation of mathematicians, but the string theorists have also got to explain away the extra dimensions.

Now maybe the way out is to figure out how multidimensional time could manifest itself.

When you perform a measurement, you can have multiple outcomes. Quantum mechanics teaches us that the outcome is indeterminate. Each different outcome can create a different future. Each different future would have its own single arrow of time with its own series of future events. And from the point of view of someone who has not yet performed the measurement, all of these arrows of time are possible. How many time dimensions do we need to accomodate all these arrows?

In Feynman diagrams, the arrow of time is irrelevant. You have an initial state, a final state, and the particles perform all possible dances getting from the initial state to the final state. What you get to observe is a kind of superposition, a kind of statistical composite (but with complex probabilities) of all the ways of getting from one to the other. How do you fit all those alternatives into one time dimension? Do we even need to? The mathematics is just as happy figuring the probabilities of the initial state given the final state as the other way around.

Perhaps the extra dimensions of Kaluza-Klein and string theories are temporal, and provide room for all these futures.

Perhaps the limitations to two, or seven, or eight, or twenty-one time dimensions aren't even the real constraint on dimensions, but just the minimum number needed for the mathematics.

Foe example, if we take a two-dimensional curved surface, it's cleanly embeddable (locally, at least) in a three-dimensional Euclidean space, faithfully preserving the intrinsic curvature. There's nothing stopping it from being embedded faithfully in a higher dimensional space, but from the viewpoint of the math, three is all that one can derive from the surface geometry.

And I seem to remember hearing of a theorem that if you start with a three (or was it four) dimensional curved hypersurface, it was locally embeddable in a ten-dimensional space.

Perhaps the restriction of, say, ten dimensions is akin to this -- it may only the number of dimensions that actually make a difference, locally.

Perhaps there are an infinite number of these temporal dimensions (whatever "there are" means in sentences like this). But if that is so, we'd have to consider an infinite number of spatial dimensions, too.