Time for another break from research (at least the normal kind).
I seem to be always discovering fundamental Laws of the Universe, especially about teaching. I’d like to share some of them with you. They are each called “Wadge’s Law” … by me. Maybe the name will catch on. Here they are.
Wadge’s Law (of traffic)
No matter how late you go through an orange light, the guy/gal behind you follows you through.
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.
This summer I was at LC2015, the big European logic conference (it was great). I was sitting listening to a talk with one of my logic buddies when the speaker mentioned “deontic logic”, which is a fancy Greek name for the logic of obligations.
A thought popped into my mind; I turned to my friend and whispered, “you ought to study deontic logic”. Ha ha ha! A self-referential statement!
My friend wasn’t exactly convulsed with laughter but never mind. A whole research program opened up before me – self descriptive “studying <adjective> logic” sentences.
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
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.
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).
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.
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.
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.
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.
