technology from back to front

Archive for April, 2006

Windows Update broke my Thunderbird, Picasa, NikonScan and EpsonScan

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]( 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.


The missing link in direct manipulation

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.


Java on .NET

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:

C:\programs\sisc-1.13.4\sisc-1.13.4>set java=c:\programs\ikvmbin-\ikvm-\bin\ikvm
SISC (1.13.4)
#;> (import s2j)
#;> (define-java-class <java.lang.System>)
#;> (define-generic-java-method println)
#;> (define-generic-java-field-accessor :out)
#;> (println (:out (java-null <java.lang.System>)) (->jstring "Hello, world"))
Hello, world
#<jnull void>
#;> (define-java-class <cli.system.console> |cli.System.Console|)
#;> (define-generic-java-method write-line |WriteLine|)
#;> (write-line (java-null <cli.system.console>) (->jstring "Hello, world"))
Hello, world
#<jnull void>

There are reports that people have managed to run tomcat on .NET this way!


Nothing But a Number

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.

Numbers as Processes

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.

defproc N0(x,z) = z!();
defproc N1(x,z) = x!().z!();
defproc N2(x,z) = x!().x!().z!();
defproc N3(x,z) = x!().x!().x!().z!();

Milner also defines some handy processes for doing basic arithmetic:

defproc Succ(x,z,y,w) = y!().Copy(x,z,y,w)
and Copy(x,z,y,w) =
  select {

defproc Add(x1,z1,x2,z2,y,w) =
  select {

Note that numbers are ephemeral – they are consumed when being processed. To do anything useful we therefore need a process to duplicate number processes:

defproc Double(x,z,y1,w1,y2,w2) =
  select {
    x?().new y1_,w1_,y2_,w2_ in (
           Succ(y1_,w1_,y1,w1) |
           Succ(y2_,w2_,y2,w2) |
    z?().(w1!() | w2!())

Armed with the above we can define a process that calculates the Fibonacci function:

defproc Fib(x,z,y,w) =
  select {
    x?().select {
      x?().new x0,z0,x1,z1,x2,z2,y1,w1,y2,w2 in (
        Double(x,z,x0,z0,x1,z1) |
        Succ(x0,z0,x2,z2) |
        Fib(x1,z1,y1,w1) |
        Fib(x2,z2,y2,w2) |

This probably looks incomprehensible at first. It has been optimised to avoid unnecessary copying and roughly corresponds to the following pseudocode

fib(x) {
  if (x-- == 0) return 0;
  else if (x-- == 0) return 1;
  else return fib(x) + fib(x+1);

What is a Number?

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:

defprop number(x,z) =
  minfix X.((<z!>true or <x!>true or <tau>true) and
            [z!]allTau and [x!]X and [tau]X and
            forall n.(n==z or n==x or [n]false));

defprop allTau =
  minfix X.((void or <tau>true) and
            [tau]X and forall n.[n]false);

Translated into English this says

A process represents a number if it communicates on two names, symbolically denoted as x and z, s.t.

  1. it may do an output on z or x, or perform an internal transition,
  2. after performing an output on z it may only perform internal transitions and must eventually evolve to nothing,
  3. after performing an output on x it must evolve to a process that represents a number,
  4. it cannot perform an infinite sequence of internal transitions or outputs on x,
  5. 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
. 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:

check N0(x,z) |= number(x,z);
check N1(x,z) |= number(x,z);
check N2(x,z) |= number(x,z);
check N3(x,z) |= number(x,z);

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:

defproc Infinity(x,z) = x!().Infinity(x,z);
defproc ErraticNumber1(x,z) =
  select {
    x!().(e!() | ErraticNumber1(x,z));
defproc ErraticNumber2(x,z) = x!().(e!() | z!());
defproc ErraticNumber3(x,z) =
  select {
    x!().(e!() | z!());
defproc ErraticNumber4(x,z) =
  select {
    x!().(e!() | e?() | z!());
defproc ErraticNumber5(x,z) =
  select {
    z!().(e!() | e?())

check Infinity(x,z) |= number(x,z);
check ErraticNumber1(x,z) |= number(x,z);
check ErraticNumber2(x,z) |= number(x,z);
check ErraticNumber3(x,z) |= number(x,z);
check ErraticNumber4(x,z) |= number(x,z);
check ErraticNumber5(x,z) |= number(x,z);

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:

defproc Fib0 = new x,z in (N0(x,z) | Fib(x,z,y,w));
defproc Fib1 = new x,z in (N1(x,z) | Fib(x,z,y,w));
defproc Fib2 = new x,z in (N2(x,z) | Fib(x,z,y,w));
defproc Fib3 = new x,z in (N3(x,z) | Fib(x,z,y,w));

check Fib0 |= number(y,w);
check Fib1 |= number(y,w);
check Fib2 |= number(y,w);
check Fib3 |= number(y,w);

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 fib(3)
when the check for fib(2) completes within a few milliseconds.

There is no Guarantee

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:

check Fib(x,z,y,w) |= number(x,z) |> number(y,w)

which says

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.


XHTML considered harmful

… in at least one common scenario. Here’s a summary:

  • Problem: Empty textareas written <textarea /> break both Firefox[1] and IE6.
  • Solution: Remove all mention of XHTML from your documents and XSLT stylesheets, and continue using XHTML-like XML without pain.

For details and explanation, read on.
Read more…




You are currently browsing the LShift Ltd. blog archives for April, 2006.



2000-14 LShift Ltd, 1st Floor, Hoxton Point, 6 Rufus Street, London, N1 6PE, UK+44 (0)20 7729 7060   Contact us