When Clare got up, I said casually "Your cat's missing". She dutifully went out to search the local highways and byways, with no result. She fell to musing about the number of cats we've had which have vanished, over the years. I think she counted four.
We then fell to speculating? Was it roaming more widely than usual in the current clement weather? Had it decided belatedly to return to its ancestral home in Hastings? Had it been taken in by a kindly farmer, and allowed to sleep in the barn? ... Or was it a squashed bundle of meat and fur on the A303?
Our thinking began to incline towards that final possibility, and I was instructed to throw the remnants of its food onto the garden for the birds.
This afternoon, about quarter to five, it nonchalantly strolled through the cat-flap without a care in the world.
I had considered writing a nostalgic piece from my time at Standard Telecommunications Laboratories in Harlow back in the 1980s, when I was studying denotational semantics. Having got a job at the lab without the right mathematical training at that time, I was always hitting new material without having studied the necessary prerequisites. So it proved with the meaning of programs. I was thrown into continuous lattice theory before properly understanding what the problem was.
Eventually I realised that we were adopting a deliberately ignorant view of the text of programs written in some programming language (e.g. Algol, C).
We were trying to do for these texts what truth-functional semantics does for logic, namely find a domain of entities where the elementary terms of the programming language could find objects which could constitute their meaning, and where the syntactic rules for compilable programs could be matched by compositional semantic rules which would assemble an entity which would be the meaning of the overall program.
The problems included:
- in programming we can do the equivalent of applying a function to itself (breaks set-theoretic cardinality rules);
- we can assign different values to identifiers writing, for example, x := x+1 (this statements, with := interpreted as equality, is simply false);
- we can explicitly modify the 'flow of control' with inherently dynamic constructs (e.g. GOTO).
Denotational semantics led to the development of super-powerful functional programming languages replete with specification-capability and logical clarity. To run functional languages such as Lisp, ML and the numerous derivatives, we even had hardware (Lisp Machines et al.), meant to take us beyond the unholy Von Neumann compromise.
As I said, I had planned to write about this, but as I was planning the memo I looked up continuations at Wikipedia, which caused a conceptual stack overflow, so I decided not to bother.