On Wed, Nov 5, 2008 at 1:24 AM, Claus Reinke
How can we support analysis of time and space complexity without expanding ourselves into the complicated dirty world of operational thinking?
equational /= denotational
Nonetheless, Haskell has equational semantics which are derived from its denotational ones. But when I said "equational semantics" I really meant something more like "equations" :-).
operational /= bad
Sometimes, denotational is too abstract, offering no guidelines on behaviour, just as abstract machine based operational thinking is too concrete, hiding the insights in a flood of details. Sometimes, operational semantics based on directed equations give you the best of both worlds: equational reasoning and behavioural guidelines, both at a suitably "clean" and abstract level.
By directed equations you mean unidirectional rewrite rules? But I'd like to back up a bit. I may have been too quick to assign the judgement "dirty" to operational thinking. I am not asking this question as a complaint, as a challenge on the language, or as any other such rhetorical device: my question is earnest. I would like to know or to develop a way to allow abstract analysis of time and space complexity. On my time working with Haskell, I've developed a pretty accurate "intuition" about the performance of programs. It is some meld of thinking in terms of the lazy evaluation mechanism, some higher-level rules of thumb about when new thunks are allocated, and probably some other stuff hiding in the depths of my brain. I know it, but I am not satisfied with it, because I can't formalize it. I wouldn't be able to write them down and explain to a fellow mathematician how I reason about Haskell programs. The example being discussed in this thread is a good one: sum [1..10^8] + length [1..10^8] With Haskell's semantics, we know we can write this as: let xs = [1..10^8] in sum xs + length xs But it causes a change in memory *complexity*, so in some sense these two sentences are not equal. What is the theory in which we can observe this fact? Is it possible to give a simple denotational semantics which captures it?