Diverting trains of thought, wasting precious time

As researchers, we are naturally wary of addressing problems which don't have a well-defined end
point. We like to be able to say, “we've solved it”, or perhaps “we've solved it
for the following formally-characterized subclass of problem”. In my work, that doesn't really
make sense. Cake is a practical tool for
tackling interface diversity. No such tool can be complete, because for any nontrivial language, or
interface encoding scheme, there is no limit to the crazy encodings that could be dreamed up. When
Kent enumerated “the many forms of a single
fact”, he wasn't making a complete list, which would clearly be impossible---but he was
trying to come up with a catalogue that included a reasonably high proportion of what people
*actually do in practice*.

Although I could try to formally characterise the class of mismatch which my current Cake language is capable of reconciling, I've never seen much worth in doing so. It's hard, if not impossible, to come up with a formal characterisation that actually has practical meaning. In any such exercise, what tends to happen is that a bunch of practically meaningful cases are excluded, and a bunch of practically meaningless cases are included. One reason for this is that humans brains are messy, and don't respect the formal boundaries induced by conventional mathematical thinking. Mathematical formalisms strive to tackle complexity primarily by purposely engineered compositionality; human evolution has done so by a random walk. The point is that humans are full of specialisations, resource limitations and arbitrary cut-offs. Too often, we embrace the formal concerns and ignore the human reality. This is the formalism wagging the research, and it's something that irritates me.

One of my favourite examples of formalism-versus-reality is our use of nesting in sentences, and
in particular, what linguists call “centre-embedded” or “self-embedding”
structures. (The concepts are distinct, but the distinction is somewhat confused in the literature.)
Sentences such as “The rat the cat the dog chased ate died.” are perfectly grammatical
according to any formal grammar of English you might reasonably come up with---that is, any grammar
that could also generate the sentences we actually use in real English. If you buy that the role of
grammars is to model the languages that people actually use, then this is clearly a failure of
modelling---yet is a consequence of the recursively generative nature of grammars loved by
formalists. In practice, we humans don't work in this neatly recursive way---the complex, messy
architecture of our brains means that only *some* kinds of embedding are easily processed,
and it turns out, as expounded by Richard
Hudson, that the actual criteria are far more complex than anyone would have thought. For example,
it appears to make a difference whether the subjects of the clauses being nested are pronouns or
not.

A related and much more familiar example for most readers will be the halting problem. We know
that no tool which attempts to answer an undecidable question can be complete. Therefore, a lot of
researchers just avoid those problems. Byron Cook, who in recent years has
been doing stellar and pioneering work on proving program termination, has been known to talk about
the variety of bafflement, disdain and ridicule which his work provoked in its inception. It's
simply anathema to conventional CS research approaches to attack problems for which it's known that
there can be no *complete* solution. In fact, far too many self-professing computer
scientists don't even understand the distinction between a partial and total solution. We have to
get over this, simply because lots of important problems are in this class! I like to think my work
on Cake is doing its bit. The halting problem is somewhat different from Cake-like problems, in that
its' a formally defined, provably-undecidable problem, whereas the incompleteness of systems like
Cake lies in that we can't even completely define the problem space in any formal way. I should add
that I'm not putting my work in the same bracket as Byron's! But there is at least this small
thematic similarity in the flavour of criticism that tends to come up. Speaking of which, I could do
with remembering this argument when it's time for my viva....

*[/research]
permanent link
contact
*