Lucid – the temporal language [1000 views]

Gear-Wall-Clock-Glass-Industrial-Mechanical-Round-1622-Inch-Large-HOIS62798-1In the Origins post I explained how we (Ed Ashcroft and I) had at the beginning very modest aims – we just wanted a programming notation that was at the same time mathematical (in fact algebraic) and would allow iterative programming without resorting to tail recursive functions. The solution I suggested was pseudo-functions “first” and “next that would allow equational definitions of loops that were not, on the surface, inconsistent. For example

first(I) = 0
next(I) = I+1
first(J) = 0
next(J) = J+2*I+1

defines a loop with two loop variables I and J, I being a counter 0, 1, 2, 3, … and J enumerating the squares 0, 1, 4, 9, … .

Ed Ashcroft objected, however, that the formal meaning of “first” and “next” was unclear – what are their domains? Without a semantics, there is no way to settle paradoxes like the following: surely next(0)=0, next(1)=1, next(2)=2, (because on the next iteration 3 will still be 3). Shouldn’t this mean that first(I)=I for all I? In which case the equation next(I) = I+1 reduces to I = I+1, a blatant contradiction.

I had no answer for this and so went back to the drawing board (actually scraps of paper in my windowless Waterloo office). About six weeks later I was doodling on a filing card and a lightbulb went on – the domain of first and next consists of infinite sequences (“histories”) of data values (in this case, integers), not just individual integers. In fact first and next had simple formal definitions:

first(<a,b,c,d,…>) = <a,a,a,a,…>
next(<a,b,c,d,…>) = <b,c,d,e,…>

Immediately everything became clear. The equations for I and J given above have a unique solution, namely

I = <o,1,2,3,…>
J = <0,2,4,9,…>

For example, consider the equation

next(J) = J+2*I+1

The left hand side is clearly <1,4,9,25,…>. The right hand side is the sum of series J, 2*I, and 1. J we know, it’s <0,2,4,9,…>. What about 2*I? Obviously, the kth value of 2*I is simply twice the kth value of I. So 2*I is <0,2,4,6,…>. As for “1”, the kth value of “1” is 1, so that the numeral “1” denotes <1,1,1,1,…>

If the equation is valid, the sequence <,1,4,9,25,…>) must be the sum of the sequences


And how do you add sequences? Pointwise, because the value of L+M+N at ‘time’ k is obviously the value of L at time k plus the value of M at time K plus the value of N at time k. And sure enough, the numbers work out. For example, in the third column 4+4+1 = 9, as it should be.

We were pretty chuffed, as the British say, because the semantics not only confirmed laws like next(L+M) = next(L)+next(M), it cleared up the paradox that next seemed to be  the identity function. The fact that next(0)=0, next(1)=1, and so on just reflects the fact that any constant sequence <a,a,a,a,…> is a fixed point of next. But we can’t deduce that next(I)=I because I may not be constant – no contradiction.

It soon became apparent that we had a temporal programming language – one based on a temporal logic, with temporal operators such as first and next. Our next question was, are there other useful temporal operators besides first and next? We immediately found two.

The first was assoonas, which can extract individual values from a loop. In general X assoonas P is the value of X that corresponds to the first true value of P. For example, with I and J defined as above, the value of  J assoonas I eq 8  is 64 (actually, <64,64,64,…>.

The other operator, fby (followed-by), allowed us to combine the first and next equations into one. Formally

<a,b,c,d,…> fby <p,q,r,s,…> = <a,p,q,r,s,…>

so that the four equations for I and J above can be combines to

I = 0 fby I+1
J = 0 fby J+2*I+1

The real significance of fby, however, is that it showed us the way to the dataflow interpretation (to be cont’d)

About Bill Wadge

I am a retired Professor in Computer Science at UVic.
This entry was posted in research. Bookmark the permalink.

1 Response to Lucid – the temporal language [1000 views]

  1. Thanks for the insightful posts. I look forward to reading more.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.