## Hurry up please it’s time

June 1st, 2007 by HancockI 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.

http://research.microsoft.com/users/lamport/pubs/pubs.html#what-good

(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.