Sandwich proofs and odd orders

Revisiting an old piece of work I reflect on the processes that led to it: intuition and formalism, incubation and insight, publish or perish, and a malaise at the heart of current computer science.

A couple of weeks ago I received an email requesting an old technical report, “Finding fixed points in non-trivial domains: proofs of pending analysis and related algorithms” [Dx88].  This report was from nearly 30 years ago, when I was at York and before the time when everything was digital and online. This was one of my all time favourite pieces of work, and one of the few times I’ve done ‘real maths’ in computer science.

As well as tackling a real problem, it required new theoretical concepts and methods of proof that were generally applicable. In addition it arose through an interesting story that exposes many of the changes in academia.

[Aside, for those of more formal bent.] This involved proving the correctness of an algorithm ‘Pending Analysis’ for efficiently finding fixed points over finite lattices, which had been developed for use when optimising functional programs. Doing this led me to perform proofs where some of the intermediate functions were not monotonic, and to develop forms of partial order that enabled reasoning over these. Of particular importance was the concept of a pseudo-monotonic functional, one that preserved an ordering between functions even if one of them is not itself monotonic. This then led to the ability to perform sandwich proofs, where a potentially non-monotonic function of interest is bracketed between two monotonic functions, which eventually converge to the same function sandwiching the function of interest between them as they go.

Oddly while it was one my favourite pieces of work, it was at the periphery of my main areas of work, so had never been published apart from as a York technical report. Also, this was in the days before research assessment, before publish-or-perish fever had ravaged academia, and when many of the most important pieces of work were ‘only’ in technical report series. Indeed, our Department library had complete sets of many of the major technical report series such as Xerox Parc, Bell Labs, and Digital Equipment Corporation Labs where so much work in programming languages was happening at the time.

My main area was, as it is now, human–computer interaction, and at the time principally the formal modelling of interaction. This was the topic of my PhD Thesis and of my first book “Formal Methods for Interactive Systems” [Dx91] (an edited version of the thesis).   Although I do less of this more formal work now-a-days, I’ve just been editing a book with Benjamin Weyers, Judy Bowen and Philippe Pallanque, “The Handbook of Formal Methods in Human-Computer Interaction” [WB17], which captures the current state of the art in the topic.

Moving from mathematics into computer science, the majority of formal work was far more broad, but far less deep than I had been used to. The main issues were definitional: finding ways to describe complex phenomena that both gave insight and enabled a level of formal tractability. This is not to say that there were no deep results: I recall the excitement of reading Sannella’s PhD Thesis [Sa82] on the application of category theory to formal specifications, or Luca Cardelli‘s work on complex type systems needed for more generic coding and understanding object oriented programing.

The reason for the difference in the kinds of mathematics was that computational formalism was addressing real problems, not simply puzzles interesting for themselves. Often these real world issues do not admit the kinds of neat solution that arise when you choose your own problem — the formal equivalent of Rittel’s wicked problems!

Crucially, where there were deep results and complex proofs these were also typically addressed at real issues. By this I do not mean the immediate industry needs of the day (although much of the most important theoretical work was at industrial labs); indeed functional programming, which has now found critical applications in big-data cloud computation and even JavaScript web programming, was at the time a fairly obscure field. However, there was a sense in which these things connected to a wider sphere of understanding in computing and that they could eventually have some connection to real coding and computer systems.

This was one of the things that I often found depressing during the REF2014 reading exercise in 2013. Over a thousand papers covering vast swathes of UK computer science, and so much that seemed to be in tiny sub-niches of sub-niches, obscure variants of inconsequential algebras, or reworking and tweaking of algorithms that appeared to be of no interest to anyone outside two or three other people in the field (I checked who was citing every output I read).

(Note the lists of outputs are all in the public domain, and links to where to find them can be found at my own REF micro-site.)

If this had been pure mathematics papers it is what I would have expected; after all mathematics is not funded in the way computer science is, so I would not expect to see the same kinds of connection to real world issues. Also I would have been disappointed if I had not seen some obscure work of this kind; you sometimes need to chase down rabbit holes to find Aladdin’s cave. It was the shear volume of this kind of work that shocked me.

Maybe in those early days, I self-selected work that was both practically and theoretically interesting, so I have a golden view of the past; maybe it was simply easier to do both before the low-hanging fruit had been gathered; or maybe just there has been a change in the social nature of the discipline. After all, most early mathematicians happily mixed pure and applied mathematics, with the areas only diverging seriously in the 20th century. However, as noted, mathematics is not funded so heavily as computer science, so it does seem to suggest a malaise, or at least loss of direction for computing as a discipline.

Anyway, roll back to the mid 1980s. A colleague of mine, David Wakeling, had been on a visit to a workshop in the States and heard there about Pending Analysis and Young and Hudak’s proof of its correctness . He wanted to use the algorithm in his own work, but there was something about the proof that he was unhappy about. It was not that he had spotted a flaw (indeed there was one, but obscure), but just that the presentation of it had left him uneasy. David was a practical computer scientist, not a mathematician, working on compilation and optimisation of lazy functional programming languages. However, he had some sixth sense that told him something was wrong.

Looking back, this intuition about formalism fascinates me. Again there may be self-selection going on, if David had had worries and they were unfounded, I would not be writing this. However, I think that there was something more than this. Hardy and Wright, the bible of number theory , listed a number of open problems in number theory (many now solved), but crucially for many gave an estimate on how likely it was that they were true or might eventually have a counter example. By definition, these were non-trivial hypotheses, and either true or not true, but Hardy and Wright felt able to offer an opinion.

For David I think it was more about the human interaction, the way the presenters did not convey confidence.  Maybe this was because they were aware there was a gap in the proof, but thought it did not matter, a minor irrelevant detail, or maybe the same slight lack of precision that let the flaw through was also evident in their demeanour.

In principle academia, certainly in mathematics and science, is about the work itself, but we can rarely check each statement, argument or line of proof so often it is the nature of the people that gives us confidence.

Quite quickly I found two flaws.

One was internal to the mathematics (math alert!) essentially forgetting that a ‘monotonic’ higher order function is usually only monotonic when the functions it is applied to are monotonic.

The other was external — the formulation of the theorem to be proved did not actually match the real-world computational problem. This is an issue that I used to refer to as the formality gap. Once you are in formal world of mathematics you can analyse, prove, and even automatically check some things. However, there is first something more complex needed to adequately and faithfully reflect the real world phenomenon you are trying to model.

I’m doing a statistics course at the CHI conference in May, and one of the reasons statistics is hard is that it also needs one foot on the world of maths, but one foot on the solid ground of the real world.

Finding the problem was relatively easy … solving it altogether harder! There followed a period when it was my pet side project: reams of paper with scribbles, thinking I’d solved it then finding more problems, proving special cases, or variants of the algorithm, generalising beyond the simple binary domains of the original algorithm. In the end I put it all into a technical report, but never had the full proof of the most general case.

Then, literally a week after the report was published, I had a notion, and found an elegant and reasonably short proof of the most general case, and in so doing also created a new technique, the sandwich proof.

Reflecting back, was this merely one of those things, or a form of incubation? I used to work with psychologists Tom Ormerod and Linden Ball at Lancaster including as part of the Desire EU network on creativity. One of the topics they studied was incubation, which is one of the four standard ‘stages’ in the theory of creativity. Some put this down to sub-conscious psychological processes, but it may be as much to do with getting out of patterns of thought and hence seeing a problem in a new light.

In this case, was it the fact that the problem had been ‘put to bed’, enabled fresh insight?

Anyway, now, 30 years on, I’ve made the report available electronically … after reanimating Troff on my Mac … but that is another story.


[Dx91] A. J. Dix (1991). Formal Methods for Interactive Systems. Academic Press.ISBN 0-12-218315-0

[Dx88] A. J. Dix (1988). Finding fixed points in non-trivial domains: proofs of pending analysis and related algorithms. YCS 107, Dept. of Computer Science, University of York.

[HW59] G.H. Hardy, E.M. Wright (1959). An Introduction to the Theory of Numbers – 4th Ed. Oxford University Press.

[Sa82] Don Sannella (1982). Semantics, Imlementation and Pragmatics of Clear, a Program Specification Language. PhD, University of Edinburgh.

[WB17] Weyers, B., Bowen, J., Dix, A., Palanque, P. (Eds.) (2017) The Handbook of Formal Methods in Human-Computer Interaction. Springer. ISBN 978-3-319-51838-1

[YH96] J. Young and P. Hudak (1986). Finding fixpoints on function spaces. YALEU/DCS/RR-505, Yale University, Department of Computer Science

Six weeks on the road

I’ve been at home for the last week after six weeks travelling around the UK and elsewhere.  I’ve not kept up while on the road so doing a retrospective post on it all and need to try to catch on other half written posts.

As well as time at Talis offices in B’ham and at Lancs (including exam board week), travels have taken me to Pisa for a workshop on ‘Supportive User Interfaces’, to Koblenz for Web Science conference giving a talk on embodiment issues and a poster on web-scale reasoning , to Newcastle for British HCI conference doing a talk on fridge, to Nottingham to give a talk on extended episodic experience, and back to Lancs for a session on creativity! Why can’t I be like sensible folks and talk on one topic!

Supportive User Interfaces

Monday 13th June I attended a workshop in Pisa on “Supportive User Interfaces“, which includes interfaces that adapt in various ways to users.  The majority of people there were involved in various forms of model-based user interfaces in which various models of the task, application and interaction are used to generate user interfaces on the fly. W3C have had a previous group in this area; Dave Raggett from w3c was at the workshop and it sounds like there will be a new working group soon.  This clearly has strong links to various forms of ‘meta-level’ representations of data, tasks, etc..  My own contribution started the day, framing the area, focusing partly on reasons for having more ‘meta-level’ interfaces including social empowerment, and partly on the principles/techniques that need to be considered at a human level.

Also on Monday was a meeting of IFIP Working Group 2.7/13.4. IFIP is the UNESCO founded pan-national agency that national computer societies such as as the BCS in the UK and ACM and IEEE Computer in the US belong to.  Working Group 2.7/13.4 is focused on the engineering of user interfaces.  I had been actively involved in the past, but have had many years’ lapse.  However, this seemed a good thing to re-engage with with my new Talis hat on!

SUI: paper:

Web Science Conference in Koblenz

Jaime Teevan from Microsoft gave the opening keynote at WebSci 2011.  I know her from her earlier work on personal information management, but her recent work and keynote was about work on analysing and visualising changes in web pages.  Web page changes are also analysed alongside users re-visitation patterns; by looking at the frequency of re-visitation Jaime and her colleagues are able to identify the parts of pages that change with similar frequency, helping them, inter alia, to improve search ranking.

Had many great conversations, some with people I know previously (e.g. the Southampton folks), but also new, including the group at Troy that do lots of work with  I was particularly interested in some work using content matching to look for links between otherwise unlinked (or only partly inter-linked) datasets.  Also lots of good presentations including one on trust prediction and a fantastic talk by Mark Bernstein from Eastgate, which he delivered in blank verse!

My own contribution included the poster that Dave@Talis prepared, which was on the web-scale spreading activation work in collaboration with Univ. Athens.  Quite a niche area in a multi-disciplinary conference, so didn’t elicit quite the interest of the social networking posters, but did lead to a small number of in depth discussions.

In addition I gave talk on the more cognitive/philosophical issues when we start to use the web as an external extension to / replacement of memory, including its impact on education.  Got some good feedback from this.

Closing keynote was from Barry Wellman, the guy who started social network analysis way before they were on computers.  At one point he challenged the Dunbar number1. I wondered whether this was due to cognitive extension with address books etc., but he didn’t seem to think so; there is evidence that some large circles predate web (although maybe not physical address books).  Made me wonder about itinerant tradesmen, tinkers, etc., even with no prostheses. Maybe the numbers sort of apply to any single content, but are repeated for each new context?

WebSci papers:

The HCI Conference – Newcastle

I attended the British HCI conference in Newcastle. This was the 25th conference, and as my very first academic paper in computing2 was at the first BHCI in 1984, I was pleased to be there at this anniversary.  The paper I was presenting was a retrospective on vfridge, a social networking site dating back to 1999/2000, it seemed an historic occasion!

As is always the case presentations were all interesting. Strictly BHCI is a ‘second tier’ conference compared with CHI, but why is it that the papers are always more interesting, that I learn more?  It is likely that a fair number of papers were CHI rejects, so it should be the other way round – is it that selectivity and ‘quality’ inevitably become conservative and boring?

Gregory Abowd gave the closing keynote. It was great to see Gregory again, we meet too rarely.  The main focus of his keynote was on three aspects of research: novelty, value and reliability and how his own work had moved within this space over the years.  In particular having two autistic sons has led him in directions he would never have considered, and this immediately valuable work has also created highly novel research. Novelty and value can coexist.

Gregory also reflected on the BHCI conference as it was his early academic ‘home’ when he did his PhD and postdoctoral here in the late 1980’s.  He thought that it could be rather than, as with many conferences, a second best to getting a CHI paper, instead a place for (not getting the quote quite perfect) “papers that should get into CHI”, by which he meant a proving ground for new ideas that would then go on to be in CHI.

Alan at conference dinnerHowever I initially read the quote differently. BHCI always had a broader concept of HCI compare with CHI’s quite limited scope. That is BHCI as a place that points the way for the future of HCI, just as it was the early nurturing place of MobileHCI.  However CHI has now become much broader in it’s own conception, so maybe this is no longer necessary. Indeed at the althci session the organisers said that their only complaint was that the papers were not ‘alt’ enough – that maybe ‘alt’ had become mainstream. This prompted Russell Beale to suggest that maybe althci should now be real science such as replication!

Gregory also noted the power of the conference as a meeting ground. It has always been proud of the breadth of international attendance, but perhaps it is UK saturation that should be it’s real measure of success.  Of course the conference agenda has become so full and international travel so much cheaper than it was, so there is a tendency to  go to the more topic specific international conferences and neglect the UK scene.  This is compounded by the relative dearth of small UK day workshops that used to be so useful in nurturing new researchers.

Tom at conference dinnerI feel a little guilty here as this was the first BHCI I had been to since it was in Lancaster in 2007 … as Tom McEwan pointed out I always apologise but never come! However, to be fair I have also only been twice to CHI in the last 10 years, and then when it was in Vienna and Florence. I have just felt too busy, so avoiding conferences that I did not absolutely have to attend.

In response to Gregory’s comments, someone, maybe Tom, mentioned that in days of metrics-based research assessment there was a tendency to submit one’s best work to those venues likely to achieve highest impact, hence the draw of CHI. However, I have hardly ever published in CHI and I think only once in TOCHI, yet, according to Microsoft Research, I am currently the most highly cited HCI researcher over the last 5 years … So you don’t have to publish in CHI to get impact!

And incidentally, the vfridge paper had NOT been submitted to CHI, but was specially written for BHCI as it seemed the fitting place to discuss a thoroughly British product 🙂

vfridge paper:

Nottingham MRL

I was at Mixed Reality Lab in Nottingham for Joel Fischer‘s PhD viva and while there did a seminar the afternoon on “extended episodic experience” based on Haliyana Khalid‘s PhD work and ideas that arose from it. Basically, whereas ‘user experience’ has become a big issue most of the work is focused on individual ‘experiences’ whereas much of life consists of ongoing series of experiences (episodes) which together make up the whole experience of interacting with a person or place, following a band, etc.

I had obviously not done a good enough job at wearing Joel down with difficult questions in the PhD viva in the morning as he was there in the afternoon to ask difficult questions back of his own 😉

Docfest – Digital Economy Summer School

The last major event was Docfest, which brought together the PhD students from the digital economy centres from around the country. Not sure of the exact count but just short of 150 participants I think. They come from a wide variety of backgrounds, business, design, computing, engineering, and many are mature students with years of professional experience behind them.

This looked like being a super event, unfortunately I was only able to attend for a day 🙁  However, I had a great evening at the welcome event talking with many of the students and even got to ride in Steve Forshaw‘s Sinclair C5!

My contribution to the event was running the first morning session on ‘creativity’. Surprise, surprise this started with a bad ideas session, but new for me too as the largest group I’ve run in the past has been around 30.  There were a number of local Highwire students acting as facilitators for the groups, so I had only to set them off and observe results :-). At the end of the morning I gave some the theoretical background to bad ideas as a method and in understanding (aspects of) creativity more widely.

Other speakers at the event included Jane Prophet, Chris Csikszentmihalyi and Chris Bonnington, so was sad to miss them; although I did get a fascinating chat with Jane over breakfast in the hotel hearing about her new projects on arts and neural imaging, and on how repetitious writing induces temporary psychosis … That is why the teachers give lines, to send the pupils bonkers!

  1. The idea that there are fundamental cognitive limits on social groups with different sized circles family~6, extended family~20, village~60, large village~200[back]
  2. I had published previously in agricultural engineering.[back]

language, dreams and the Jabberwocky circuit

If life is always a learning opportunity, then so are dreams.

Last night I both learnt something new about language and cognition, and also developed a new trick for creativity!

In the dream in question I was in a meeting. I know, a sad topic for a dream, and perhaps even sadder it had started with me filling in forms!  The meeting was clearly one after I’d given a talk somewhere as a person across the table said she’d been wanting to ask me (obviously as a sort of challenge) if there was a relation between … and here I’ll expand later … something like evolutionary and ecological something.  Ever one to think on my feet I said something like “that’s an interesting question”, but it was also clear that the question arose partly because the terms sounded somewhat similar, so had some of the sense of a rhyming riddle “what’s the difference between a jeweller and a jailor”.  So I went on to mention random metaphors as a general creativity technique and then, so as to give practical advice, suggested choosing two words next to each other in a dictionary and then trying to link them.

Starting with the last of these, the two words in a dictionary method is one I have never suggested to anyone before, not even thought about. It was clearly prompted by the specific example where the words had an alliterative nature, and so was a sensible generalisation, and after I woke realised was worth suggesting in future as an exercise.  But it was entirely novel to me, I had effectively done the exactly sort of thinking / problem solving that I would have done in the real life situation, but while dreaming.

One of the reasons I find dreams fascinating is that in some ways they are so normal — we clearly have no or little sensory input, and certain parts of our brain shut down (e.g. motor control to stop us thrashing about too much in our sleep) — but other parts seem to function perfectly as normal.  I have written before about the cognitive nature of dreams (including maybe how to model dreaming) and what we may be able to learn about cognitive function because not everything is working, rather like running an engine when it is out of the car.

In this dream clearly the ‘conscious’ (I know an oxymoron) problem-solving part of the mind was operating just the same as when awake.  Which is an interesting fact about dreaming, but  I was already aware of it from previous dreams.

In this dream it was the language that was interesting, the original conundrum I was given.  The problem came as I woke up and tried to reconstruct exactly what my interlocutor had asked me.  The words clearly *meant* evolutionary and ecological, but in the dream had ‘sounded’ even closer aurally, more like evolution and elocution (interesting to consider, images of God speaking forth creation).

So how had the two words sound more similar in my dream than in real speech?

For this we need the Jabberwocky circuit.

There is a certain neurological condition that arises, I think due to tumours or damage in particular areas of the grain, which disrupts particular functions of language.   The person speaks interminably; the words make sense and the grammar is flawless, but there is no overall sense.  Each small snippet of speech is fine, just there is no larger scale linkage.

When explaining this phenomenon to people I often evoke the Jabberwocky circuit.  Now I should note that this is not a word used by linguists, neurolinguists, or cognitive scientists, and is a gross simplification, but I think captures the essence of what is happening.  Basically there is a part of your mind (the conscious, thinking bit) that knows what to say and it asks another bit, the Jabberwocky circuit, to actually articulate the words.  The Jabberwocky circuit knows about the sound form of words and how to string them together grammatically, but basically does what it is told.  The thinking bit needs to know enough about what can be said, but doesn’t have time to deal with precisely how they are strung together and leaves that to Jabberwocky.

Even without brain damage we can see occasional slips in this process.  For example, if you are talking to someone (and even more if typing) and there is some other speech audible (maybe radio in the background), occasionally a word intrudes into your own speech that isn’t part of what you meant to say, but is linked to the background intruding sound.

Occasionally too, you find yourself stopping in mid sentence when the words don’t quite make sense, for example, when what would be reasonable grammar overlaps with a colloquialism, so that it no longer makes sense.  Or you may simply not be able to say a word that you ‘know’ is there and insert “thingy” or “what’s it called” where you should say “spanner”.

The relationship between the two is rather like a manager and someone doing the job: the manager knows pretty much what is possible and can give general directions, but the person doing the job knows the details.  Occasionally, the instructions get confused (when there is intruding background speech) or the manager thinks something is possible which turns out not to be.

Going back to the dream I thought I ‘heard’ the words, but examining more closely after I woke I realised that no word would actually fit.  I think what is happening is that during dreaming (and maybe during imagined dialogue while awake), the Jabberwocky circuit is not active, or not being attended to.  It is like I am hearing the intentions to speak of the other person, not articulated words.  The pre-Jabberwocky bit of the mind does know that there are two words, and knows what they *mean*.  It also knows that they sound rather similar at the beginning (“eco”, “evo”), but not exactly what they sound like throughout.

I have noticed a similar thing with the written word.  Often in dreams I am reading a book, sheet of paper or poster, and the words make sense, but if I try to look more closely at the precise written form of the text, I cannot focus, and indeed often wake at that point1.  That is the dream is creating the interpretation of the text, but not the actual sensory form, although if asked I would normally say that I had ‘seen’ the words on the page in the dream, it is more that I ‘see’ that there are words.

Fiona does claim to be able to see actual letters in dreams, so maybe it is possible to recreate more precise sensory images, or maybe this is just the difference between simply writing and reading, and more conscious spelling-out or attending to words, as in the well known:

Paris in the
the spring

Anyway, I am awake now and the wiser.  I know a little more about dreaming, which cognitive functions are working and which are not;  I know a little more about the brain and language; and I know a new creativity technique.

Not bad for a night in bed.

What do you learn from your dreams?

  1. The waking is interesting, I have often noticed that if the ‘logic’ of the dream becomes irreconcilable I wake.  This is a long story in itself, but I think similar to the way you get a ‘breakdown’ situation when things don’t work as expected and are forced to think about what you are doing.  It seems like the ‘kick’ that changes your mode of thinking often wakes you up![back]

Reflection in practice: Schön and science

I have just finished reading Schön’s “The Reflective Practitioner“. It is one of those books that you feel you ought to have read years ago, resonating so much with many of my own thoughts and writing about creativity and innovation. However, I found myself at odds slightly with the adversarial dualism between science and practice, but realise this is partly because it is a book of its time. I will return to this later.

Continue reading

Comics and happy problem solving

I am in Eindhoven doing CSCW, silly ideas and other things with the USI students here. On the book shelf here is Scott McCloud’s “Understanding Comics” I picked this up last year and couldn’t put it down until I had read it all. There is another book on the shelves this year “Reinventing Comics” and I daren’t pick it up until I’ve done all the work I want to today!

Understanding Comics is both an apologetic for comics as an art form and also an exploration into what makes a comic a comic and how comics manage to captivate and give a sense of narrative and action through what are basically static images. As well as being a good read about comics and about art there seem to be many lessons there for other forms of narrative and animation especially on the web.

As far as I can see (without starting to read it and not being able to stop), Reinventing Comics seems to be about the way online delivery trough the web is giving new opportunities for Comic art … but maybe when I finish everything today I will find out.

Less graphic and less fun, but no less fascinating, I have been dipping into chapters of “The Psychology of Problem Solving“, which was also sitting on the USI shelves. I was particularly enthralled by descriptions of experiments where subjects were asked to accomplish divergent thinking tasks whilst either pushing their palms upwards from under a table, or pushing down from on top. The former a positive, ‘come to me’ gesture elicited more diverse ideas than the latter, negative, ‘go away’ gesture, even though the only difference was the muscle groups in tension. I’ve seen other research that shows how our brains monitor our body state to ‘see how we feel’ (like smiling therapy), but this was one of the most subtle and conclusive.

During the week I have had the USI students work through a design brief starting with silly ideas then moving through  structured analysis to good ideas. Perhaps I should have had them pushing up on tables in the first part and down in the second?

I was just sent a link to an article in The Psychologist “Sleep on a Problem… It works like a dream” by Josephine Ross

The article gathers loads of anecdotal evidence of creativity in dreams … including, inevitably, those benzine rings!

Personally … while I’m sure that some things happen unconsciously and during sleep, my guess is that 90% of these creativity stories have simpler reasons through selective memory or semi-random inspiration.

Continue reading