Hi everyone,
Not sure this is the right venue, as this is a question about the
semantics of FRP rather than Haskell...
I have a question about the definition of "causality" for stream
functions. A quick recap... Given a totally ordered set T (of times),
the type of behaviours Beh A is defined to be (T -> A). Behaviours come
with an equivalence relation a =t b (equal up to time t) defined as:
a =t b iff forall s <= t . a(s) = b(s)
A function (f : Beh A -> Beh B) is causal whenever it respects =t, i.e.
(forall t . a =t b => f a =t f b).
This is fine and good, until we hit nested behaviours, where there are
oddities. Consider the function:
double : Beh A -> Beh Beh A
double a t u = a u
This fails to be causual, because (using list notation for behaviours
where the time domain is natural numbers) we have:
[0,1,2,...] 0 = 0 = [0,2,4,...] 0
double [0,1,2,...] 0 = [0,1,2,...] != [0,2,4,...] = double [0,2,4,...]
On the other hand:
weird : Beh Beh A -> Beh A
weird a t = a t (t + 1)
is causal, even though on the surface the behaviour at time t depends on
the behaviour at time t+1. An alternate definition, which allows double
and disallows weird, is a "deep" equality:
a ~t b iff forall s <= t . a(s) ~s b(s)
Note that this depends on deep equality being defined at type A. Some
appropriate definitions for ~t at other types includes:
at type A -> B: f ~t g iff forall s <= t, a ~s b implies f a ~s f b
at type (A,B): (a1,a2) ~t (b1,b2) iff (a1 ~t b1) and (a2 ~t b2)
[And yes, I don't think it's a coincidence that this looks a lot like a
parametricity definition or step-indexed logical relation.]
Has such a definition of "deep" causality been investigated?
Alan.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
