For about a week, I thought my EpsonScan driver was broken: whenever I selected a folder to dump my batch scans, it would just hang there on the “Browse for Folder” dialog box.
Then I noticed the same problem in NikonScan…, Picasa… and Thunderbird.
Suspicious, huh? I rummaged around and noticed that Windows Update had installed four patches about a week ago. I bit of googling suggested KB908531 might have been the culprit. So I uninstalled KB908531 through the Add/Remove Programs feature in Control Panel and ta da! my computer is usable again.
BTW, you should read [Microsoft's knowledgebase article](http://www.microsoft.com/technet/security/Bulletin/MS06-015.mspx) before you uninstall the patch. Since those are the primary applications for my computer at home, I’ll be living (dangerously) without the patch until they fix it properly.
In his analysis of direct manipulation, Nielson says that the computational device (which reminds me of Don Norman’s ‘information appliances‘) is the “ultimate in directness”: Not only is there a direct mapping from commands to goals, but a direct mapping from physical actions to commands. Direct manipulation interfaces, such as desktop GUIs, only give the first part of this mapping.
Today’s computer input devices and today’s computer user interfaces are analogous: What you do with a mouse, or a tablet stylus, has a direct correspondence to what happens on the screen; likewise, what you do with the little pictures on your screen translates into (notionally) corresponding operations on the computer’s state. Broadly, these correlations are intended to make using a computer familiar and thereby easier. However, there is a disconnect: Although what you have in your hand behaves as a real object, what appears on screen doesn’t, and not only because interface designers make some odd decisions. There is an indirection between the input gestures (e.g., moving the mouse) and commands in the interface (deleting a file), which is that you have an avatar in the interface world—the mouse pointer—as an intermediary between syntax and semantics.
Why have a mouse pointer at all? A scene in the film Minority Report featured an operator manipulating digital objects on a screen using hand gestures (though the awkwardness of the invented gestures had geeks everywhere clutching their tendons in sympathy). Recently, a group at NYU created a working prototype of a similar system. The syntax of these interfaces is immediately accessible, and the semantics follow the syntax according to how closely the digital objects simulate real objects. The syntax is, however, strictly limited to what is simulated.
Haptic input devices like the Sensetable also obviate intermediaries. With the AudioPad, pucks with some electronic kit inside represent microphones and samples. Move a sample puck closer to the microphone puck and the sample is played louder. Now one has a command language where the physical attributes of the input device (e.g., position) are the syntax. Further, the abstract object now has the noisy analogue behaviour that real objects have, like sliding and spinning, which expands the vocabulary of commands and smears it into a continuum.
The advantage of indirection is that it provides a shield of abstraction: my mouse is always a mouse but the mouse pointer can be a cursor, a file being moved, a finger for pressing buttons. It can also be different objects, because when I set down something I’m manipulating it goes back to being just digital state and I can manipulate something else. This kind of multiplicity isn’t possible without the indirection. There is a halfway position, which is to have generic input objects that can assume the identity of particular digital objects. This is actually what AudioPad does—a puck can ‘be’ any sample at a point in time.
Here is where we meet up with consumer electronics. While in the past we’ve largely had tools that embody verbs, nowadays we have devices that embody nouns. Your iPod is your music collection. I think we’ll soon see a convergence whereby computer input devices become more specialised as their nouns are manifested as real objects (take a look at the wacky game controllers available), and consumer electronic devices shift in sympathy, and as technology allows, to having richer, nuanced vocabularies.
Prompted by Tony, I have played with ikvm, which allows you to run Java programs on .NET. Significantly it facilitates mixing and interop between Java and .NET code, i.e. Java code can call .NET libraries and .NET code can call Java libraries.
As a test, I tried running SISC under ikvm. Amazingly, “it just works”. Even calls to .NET libraries via SISC’s reflection-based Java interop interface work as expected:
There are reports that people have managed to run tomcat on .NET this way!
Spatial Logics allow one to reason about the behaviour and structure of concurrent programs. SLMC is a spatiallogic model checker for pi-calculus processes. As a little exercise I used it for reasoning about Church numerals and processes that operate on them.
In his original work on the pi calculus, Robin Milner defined an encoding of Church numerals, where the number
n is encoded as n outputs on a successor channel, followed by an output on a zero channel, e.g.
Milner also defines some handy processes for doing basic arithmetic:
Note that numbers are ephemeral – they are consumed when being processed. To do anything useful we therefore need a process to duplicate number processes:
Armed with the above we can define a process that calculates the Fibonacci function:
This probably looks incomprehensible at first. It has been optimised to avoid unnecessary copying and roughly corresponds to the following pseudocode
So far we have only defined some simple pi-calculus processes. Now let’s start reasoning about them. First would like to know whether a process represents a number. After a lot of trial-and-error, and consultation with my colleague Francis, I eventually arrived at the following SLMC predicate:
Translated into English this says
A process represents a number if it communicates on two names, symbolically denoted as
- it may do an output on
x, or perform an internal transition,
- after performing an output on
zit may only perform internal transitions and must eventually evolve to nothing,
- after performing an output on
xit must evolve to a process that represents a number,
- it cannot perform an infinite sequence of internal transitions or outputs on
- it may not perform any other actions.
Item 4 and 5 deserve some discussion. Item 4 basically excludes infinity as a number. Item 5 states that we want our processes to be just numbers and nothing else. For example, we would not want a process to behave like a number but also delete all files on our hard
drive. This point sparked some philosophical discussion with my colleague Paul. Specifically, axiomatisation in mathematics usually does not exclude additional behaviours. For example, file-deleting numbers satisfy all the Peano
axioms. Should there be an additional axiom along the lines of “Numbers must not satisfy any
axioms other than the ones stated here”?
Anyway, let’s put our
number predicate to some use:
Feeding these to SLMC all result in success, so 0,1,2,3 really are numbers – hooray! Now for some counter examples of processes that are almost numbers, but not quite:
All the checks fail, as expected.
Finally, let’s check whether the Fibonacci process produces numbers for
certain inputs – or, more precisely, whether the Fibonnaci process,
when composed with certain number processes, evolves into a process
that represents a number:
These all succeed. However, the last check – whether
fib(3) is a number – takes several hours to complete. I know the complexity of the computations performed by SLMC can be quite bad, but I am still at a loss to explain why it would perform so much more badly on
when the check for
fib(2) completes within a few milliseconds.
The reader may wonder why we selected particular examples to test the Fibonacci process, rather than checking whether it evolves to a number for any given input number. To express such a test we need the spatial logic’s guarantee operator,
|>, and then could write:
Is Fibonacci a process that when composed with a process that is a
number, is a number?
Unfortunately, SLMC does not support the guarantee operator. There is a good reason for that. The expressiveness of the logic must be finely tuned in order for model checking of interesting properties to be decidable for interesting processes. Introducing the guarantee operator makes model checking undecidable for most interesting processes.
… in at least one common scenario. Here’s a summary:
<textarea />break both Firefox and IE6.
For details and explanation, read on.
You are currently browsing the LShift Ltd. blog archives for April, 2006.