by Hancock on June 1, 2007.
Tagged as: Lunches.
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.
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.