Recently I was invited to give a 1-hour tutorial at the Computing in Topological Structures workshop (CTS 2022) held partially by zoom and in person in Sochi, Russia. Here is the second part, about programming in Lucid. It will be more accessible than Part I.

Back to Earth. In 1968 the mathematics academic job market collapsed. So when I left Berkeley in 1971 I went to a computer science department, at the University of Waterloo in Canada. Didn’t know much computer science but I did have programming experience.

At Waterloo I became an enthusiastic fan of “structured programming” (now called “programming”) and considered not only gotos harmful but also assignments like i:=i+1 that don’t make sense as equations. I set out to find a way to describe loops with equations. This is what I came up with. The equation next(i)=i+1 is not self-contradictory.

I was specially pleased to discover a simple induction rule that allowed you to prove invariants like j = i**2 directly from the program statements, which double as axioms from which properties of the program can be derived logically.

I was so excited I left my windowless office in the Pure Math corridor and went to see my good friend Ed Ashcroft in the Computer Science corridor. As we sat by his window (he had one) I explained my discovery. He thought it was interesting but asked, what are the semantics? What’s being equated? He’d promised himself never to work on schemes that don’t have semantics.

Anybody familiar with the Baire Space should have seen it in a minute but it took me about 6 weeks. Finally I was doodling on a filing card in my windowless office and the above struck me. Of course! The equations are between infinite sequences, that can be thought of as histories (later, streams). I shot out of my windowless office, down the Pure Math corridor, into the Computer Science corridor and then Ed’s be-windowed office. He was convinced and we began collaborating.

Among the first things we came up with was the operation fby, which doesn’t have an analog in imperative programming.

The fby operation allowed us to combine pairs of equations so that the program is purely definitional. You can show (as Ed pointed out) that it always has a unique minimum solution. So you don’t need special rules to ensure programs are meaningful.

One thing that bothered us was that the programs seems to go on forever – the sequences are infinite, after all. The solution was lazy evaluation, so only those values actually needed are computed. David May, then a grad student, came up with the idea as did (independently) one of Ed’s students. Calvin Ostrum generalized it and Tony Faustini refined it.

There was one hitch, user defined functions. How do you evaluate fib(n) at time 4? Fortunately we came up with a coding scheme which eliminated user defined functions and manipulated what we called the “place” dimension, which indicated a place in the function calling tree. Ostrum had figured out a version of this.

Yaghi code is based on context-switching operators that manipulate place codes. These are examples of intensional operators, as described by Richard Montague and Dana Scott. Lucid is not only computing over the Baire Space, it is intensional programming.

One of the advantages of eduction is that it easily extends to multiple dimensions. Here is a program that uses a space dimension s as well as a time dimension t. An efficient implementation needs to know which dimensions a variable actually depends on. This is dimensionality analysis and is the topic of Monem Shennat’s PhD (May 2022).

Shennat is my 17th (and last) student.

We adapted my PyLucid interpreter to run over the partially ordered domain of dimensionalities.

I’d prepared slides about my current efforts to use multiple time dimensions to implement nested loops. However I ran out of time and didn’t use them. I’ll let you puzzle over them.

Hmmm…

Hmmm…

Hmmm…

Hmmm…

And there you have it.

Look at all the people whose ideas have contributed to our knowledge of the Baire Space and computing on it. Countries? Canada, the US, the UK, Russia, France, Poland, Italy, Jordan, Libya.

Ok mainly men and no one from the Southern hemisphere 🙁

Still, pretty international.