Lucid – the temporal language

In 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

<0,1,4,9,…>
<0,2,4,6,…>
<1,1,1,1,…>

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)

Advertisements

About Bill Wadge

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

One Response to Lucid – the temporal language

  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:

WordPress.com Logo

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

Twitter picture

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

Facebook photo

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

Google+ photo

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

Connecting to %s