I mentioned the problem of representing time in a (working) mathematical model.

For many purposes, the natural numbers are perfect. This time is discrete, has an origin, and no end.

For other purposes, we may prefer the (positive and negative) integers [no beginning]. Or the rational numbers [dense: between two moments, a third]. Or maybe the real numbers, or some interval, or (who knows) the irrationals,… whatever.

Yampa takes very seriously the idea of values that are a function of continuous time – these are called signals, and are in some sense virtual – the real things are signal transformers. Discrete streams are captured by maybe-valued signals f : T -> A+1.

Now I think I understand T=natural numbers quite well, as a signal transformer is then of type Str A -> Str B, and any such function which is continuous has an implementation by an object of type

nu x. mu y. B * x + (A -> y)

But this depends on Str B being a final coalgebra, at least weakly. How far can one push eating techniques to time-domains like the real numbers, or whatever suits a digital-analog interface?

Lamport’s notion of stuttering ==============================

I mentioned an attractive and unusual approach to time taken by Leslie Lamport.

(Search for the word stuttering throughout the page.)

Lamport restricts his specification language TLA (a form of linear-time temporal logic) so that the temporal properties it can state (of streams of states) are all invariant under stuttering: introducing or deleting finite repetition. The reason he does this is deeply bound up with his notion of what is a (low-level) implementation of a (high-level) specification.

Think of it like this: a formula of temporal logic describes a movie of the system being modelled. The camera’s shutter speed must be fast enough to capture every state-change that takes place, It can be faster, in which case there will be repeated frames.

Because the formulas are stuttering-insensitive, they are not so much properties of movies, as properties of what a movie is of. If you see what I mean.

Thorsten held forth for a while about “special double relativity”, or something like that.