Bill Wadge's Blog

The Universal Hybrid Calculus (UHC) is a simple logical formalism that has the power of the monadic predicate calculus but has no bound variables. Natural language statements (which also do not use variables) can be formulated more directly in the UHC. In particular, the UHC, like natural language, uses quantifier phrases (such as some Greeks or all mortals) rather than quantifiers and variables.

(This is joint work with my PhD student Omar Alaqeeli)

The UHC is based on the simplest of the modal logics, S5. S5 can be explained (in a nonstandard way) as follows: there is a nonempty universe of individuals (say, people). Properties of individuals are denoted by property constants, which are upper case letters. For example, M might denote the property of being mortal, and G the property of being Greek. Boolean combinations of property constants also denote properties in the obvious way; so that e.g. G∧M denotes the property of being Greek and Mortal.

Continue reading →

Besides the development  of  Lucid, for a long while I’ve been working on another application of intensionality, namely intensional web pages – pages whose exact content depends on an implicit context. Unlike with Lucid, the contexts are not lists of natural numbers but rather lists of parameter settings – originally, based on the algebra of contexts John Plaice  and I developed back in 1993 in

Plaice, J. and W.W. Wadge, “A new approach to version control,” IEEE Transactions on Software Engineering, pp. 268-276, 1993.

Originally these contexts were intended to specify versions of software systems but we soon realized that they could equally well be used to specify versions of web pages. In its simplest form a context is a list (sum) of parameter settings, for example

Continue reading →

Here is the promised description of the retirement plan mentioned in the Lucid – Eduction post. This description is a slightly edited version of section 3 of “An eductive interpreter for the language pLucid”, by myself and A. Faustini, which appeared way back in 1987 in PLDI87.

Continue reading →

One way of understanding the problem described in “Into the Abyss” is in terms of the domain of streams being used.

The data-push model, discovered originally by Gilles Kahn, models a stream as either a finite or infinite sequence of data items. The infinite sequences represent ‘healthy’ streams that run without interruption – in particular without deadlock. They represent streams produced by devices that never freeze up, that always eventually produce one more output item.

The finite streams, on the other hand, represent computations that at some point do freeze up. Streams produced by devices that at some point permanently stop producing output. In Kahn’s data-push model, deadlock is indeed permanent. If the (say) index 6 component of a stream never appears, neither will the index 7, or 8, or 9 etc components. Kahn asserted that his least fixed point domain semantics corresponded exactly to the data-push computation model, and he was right. (My first PhD student, Tony Faustini, gave the first formal proof of this claim in his 1982 PhD).

Continue reading →

When we discovered the dataflow interpretation of Lucid (see post, Lucid, the dataflow language) we thought we’d found the promised land. We had an attractive computing model that was nevertheless faithful to the declarative semantics of statements-as-equations.

However, there was a snake in paradise, as David May explained in the fateful meeting in the Warwick Arts Center Cafeteria.

The problem was with the if-then-else operator and, more generally, with any operator that can produce output before it has consumed all its inputs. The simplest example is probably the lazy logical disjunction operator, which can produce the output true as soon as an input of true arrives on either of its input pipes.

Continue reading →

Recently I’ve been working with my wife Christine (who teaches in the French Department at UVIC) on a simple system, called Quiz Script, that makes it easy and quick to generate online interactive quizzes. This is the handout we gave to accompany our talk at the May CALICO conference at UVIC. Try it out!

Quizscript – interactive exercises without tears

Quizscript is a simple cloud-based system for generating interactive quizzes from marked-up – in fact, punctuated – text. There is no software to download and install on the client’s computer, and none to install on your institution’s servers. There is no maintenance and, currently,  no charge. All an instructor needs to create a set of exercises is an internet connection, a browser and, optionally, a text editor (an editor for composing unformated texts). Once created the quizz (in the form of an .html text file) can be deployed on a server, emailed to the students, or distributed directly on CDs or flash drives.

Continue reading →

In the last post I explained how temporal logic came to the rescue and enabled equations like

next(I) = I+1

to be interpreted as real equations. In this temporal logic variables like I are variables that change with time – the meaning (denotation) of I is the whole sequence <0,1,2,…> of values that I takes on through its lifetime. Then the mysterious operator next loses its mystery. The operator next maps sequences to sequences in such a way that the tth value of next(I) is the t+1th value of I. Even “+” denotes an operation on sequences, one that adds the components pairwise. For that matter even the numeral “1” denotes the constant sequence <1,1,1,…>.

This revelation opened up a whole universe of possibilities. Why limit the (formerly) mysterious operators to first and next? We immediately found two useful additions (described last entry), namely assoonas to extract values from loops, and fby to combine recurrence equations into a single equation.

Continue reading →

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) = o
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.

Continue reading →

Many years ago Ed Ashcroft and I invented the declarative language Lucid. It’s had an
interesting history.

To begin with, we never intended to design a dataflow language. All we wanted was
a more rigorously structured language which would make it easier to prove assertions
about programs.

I’d moved into computer science after leaving Berkeley and soon became convinced
that this new-fangled “structured programming” was the way to go. In fact I quickly became a real fanatic, convinced that not only did the goto statement have to go, but that even assignment statements caused trouble. My objection to assignments was that they looked like equations but were typically used in a way that defied the logic of equality. For example, early in a program you can have

I = 1

but later you can have

I = J*J+3

which contradicts the first equation. Even worse, you can have

I = I+1

which contradicts itself (because it implies 0=1). No wonder program proving is difficult!

Continue reading →