Lucid is based on a simple temporal logic. The time model follows from formalizing iteration as it appears in imperative programs with, say, while or for loops.
In this model there is a first or initial time point, and every time point has a unique successor. Imperative iterations normally terminate, so we should have only finitely many time points. Lucid avoids the complications of finite time domains by making everything at least notionally infinite, so that the domain of time points is the natural numbers with the usual order.
In temporal logic logicians have studied a huge variety of time domains. What do they mean in terms of iteration and how do we write iterative programs over nonstandard time domains?
One simple generalization is to drop the requirement that there be an initial time point and specify instead that every time point also has a unique predecessor. This gives us the integers as the time domain. We won’t get into philosophical problems about infinite negative time and iterations that have formally been going on forever.
We can adapt Lucid to this notion of time by making our streams have the integers as their domain. For primitives we can retain the usual first, next, and fby. It’s obvious how the first two work. And that next has a dual prev. But fby needs some thought. We soon see that X fby Y must be the standard part of Y shifted right preceded by the 0 point of X preceded by the nonstandard part of X. In other words
… x-2, x-1, x0, y0, y1, y2, …
with x0 at the zero point.
After playing around a bit we discover we need another operator that works like fby except that it puts y0 at the zero point. Since it’s sort of a backwards fby; let’s call it ybf. The operator ybf can be used to pre-initialize a sequence. Suppose we want to define the Fibonacci sequence whose standard part is
1, 1, 2, 3, 5, 8, 11, …
1 ybf (0 ybf prev prev Fib + prev Fib)
This definition goes two steps into the past to define the current value of Fib in terms of the two previous values. We can also go only one step by writing
Fib = 0 ybf (1 fby prev Fib + Fib)
and here we’re defining the next value of Fib in terms of the current and previous values.
Either of these is preferable to the confusing
Fib = 1 fby 1 fby Fib + next Fib
which is correct but hard to grasp because it defines next next Fib in terms of next Fib and the current Fib.
What would this mean for imperative programming? What would a while loop look like that has pre-initialization? Let alone one that has already been going on, forever? No idea.
What if we want to define a stream by two recurrence relations, one forward and one reverse? The simplest example is a counter, given in standard Lucid as
I = 0 fby I+1
This clearly gives the wrong answer in the new interpretation; I is
… 0, 0, 0, 0, 1, 2, 3, 4, …
So let’s define the left hand part by
J = J-1 ybf 0
and this defines J as
… -3, -2, -1, 0, 0, 0, 0, …
then we can put them together as J fby I giving
… -3, -2, -1, 0, 1, 2, 3, …
Interestingly, J ybf I gives the same result.
But this is all pretty clumsy. Can we do better? Yes, it turns out
K = K-1 ybf (0 fby K+1)
does the job. What if we parenthesize it the other way? What if
K = (K-1 ybf 0) fby K+1
It turns out we get the same result. This is not a coincidence. There is a general rule that
A ybf (M fby B) = (A ybf M) fby B
for any A, B, and M. Both expressions denote the generalized stream
… a-3, a-2, a-1, a0, m0, b0, b1, b2, b3, …
This is a very pleasing identity (trivial to verify) and justifies us omitting parentheses in definitions such as
K = K-1 ybf 0 fby K+1
which combines two recurrence relations, one backwards, one forward.
Now let’s do an example involving both space and time. Obviously we’ll allow negative space coordinates. Instead of thinking up new names for the operators we’ll simply add .s to the time operators, e.g. prev.s.
The example is a simple minded numerical analysis treatment of heat flow. We have an infinite (in both directions) iron bar at temperature 1 in the middle tapering off linearly to 0. First we define a distribution that goes negative then min it with 0 to get the desired initial heat distribution Q:
P = P-0.01 ybf.s 1 fby.s P-0.01
Now we define an iteration in which (I know this is simple minded) H starts with Q and at each step each value of H is replaced by the average of the neighboring values.
H = Q fby (prev.s H + next.s H)/2
Imagine the headache it would be to do this with only nonnegative indices. We’d have to shift it all over, calculate how much shift, etc.
What about conventional imperative languages – do they have arrays with negative indices? Apparently not … I don’t know of any and neither do knowledgeable friends. Of course in Python (for example) you can write A[-3] but this is just for counting from the end of the array. Odd that.
Next post: branching time.