Being Head of Department sometimes has its drawbacks, but kicking off the Distinguished Lecture Series of the Department of Informatics at King’s College London on 21 June 2012, and introducing our first speaker has to be one of the highlights so far. Emeritus Professor Dov Gabbay has had a remarkable career in Computer Science, and is rightly regarded as one of the outstanding minds in the area of logic. Dov retired in 2011, but I’m delighted that he remains with us at King’s as Emeritus Professor. Indeed, there’s no sign of him slowing down – he remains as active as he ever was.
As I said when I introduced his lecture, one of my prized possessions is one of Dov’s many volumes on logic in his series of handbooks. I acquired it as a PhD student way back, and have ensured that it stays on my shelf, despite being forced to downsize my book collection on several occasions. So it was an honour and a privilege to invite Dov to deliver his lecture.
Of course, the lecture was outstanding, both instructive and entertaining, and set a very high bar for those who will follow in the series of Informatics Distinguished Lectures (look out for future lectures!). We’ve recorded it on video, and I’ll post a link here (as well as several other places) once it’s available.
As Carlito’s nephew(?) in the film, Carlito’s Way, says to Carlito (played by Al Pacino), “You a ****ing legend, man!” I can think of no one to whom such a statement applies more than Dov.
24 October 2012: VIDEO LINK ADDED
The Financial Times recently published a correspondence on Reverse Polish Notation, including this letter from one Peter Jaeger of Tokyo, Japan (published on 2011-09-30):
Sir, Your reader Chris Ludlam describes the input method of his HP12c as “reverse logic”. The correct term is “Reverse Polish”, which is not only far more colourful, but also gives credit to Jan Lukasiewicz, the logician who invented the original Polish Notation which American mathematicians later adapted for computers.”
While it is correct to say that American mathematicians adapted Reverse Polish Notation (RPN) for computers, this is not the whole story. The first person to speak publicly about using RPN for computer architectures was Australian – Charles Hamblin, an Australian philosopher and computer pioneer, speaking at a computer conference held in Salisbury, South Australia, in June 1957. (This was billed as “The First Australian Computer Conference”, but an earlier one had been held in 1951.) Hamblin’s work was published in the conference proceedings and later in a refereed article in the Computer Journal in 1962. Among the attendees at that conference was the British statistician and computer pioneer Maurice Wilkes, who later won an AM Turing Award (in 1967), as well as delegates from computer manufacturing companies.
The first computer manufacturing company to announce deployment of RPN in a commercial computer architecture was British – the English Electric Company (EEC), in their KDF9 machine, announced in 1960 and delivered in 1963. Burroughs, an American computer company, also delivered a computer using RPN in 1963, the Burroughs B5000, but this machine was only announced in 1961. Robert Barton, chief architect of the B5000, later wrote that he developed RPN independently of Hamblin, sometime in 1958.
So the first person to talk publicly about applying RPN to computers was Australian and the first computer company to say publicly they would actually do so was British. Not everything in computing happens first in the USA!
R. S. Barton : Ideas for computer systems organization: a personal survey. pp. 7-16 of: J. S. Jou (Editor): Software Engineering: Volume 1: Proceedings of the Third Symposium on Computer and Information Sciences held in Miami Beach, Florida, December 1969. New York, NY, USA: Academic Press.
C. L. Hamblin : An addressless coding scheme based on mathematical notation. Proceedings of the First Australian Conference on Computing and Data Processing, Salisbury, South Australia: Weapons Research Establishment, June 1957.
C. L. Hamblin : Translation to and from Polish notation. Computer Journal, 5: 210-213.
A search algorithm is a computational procedure (an algorithm) for finding a particular object or objects in a larger collection of objects. Typically, these algorithms search for objects with desired properties whose identities are otherwise not yet known. Search algorithms (and search generally) has been an integral part of artificial intelligence and computer science this last half-century, since the first working AI program, designed to play checkers, was written in 1951-2 by Christopher Strachey. At each round, that program evaluated the alternative board positions that resulted from potential next moves, thereby searching for the “best” next move for that round.
The first search algorithm in modern times dates from 1895: a depth-first search algorithm to solve a maze, due to amateur French mathematician Gaston Tarry (1843-1913). Now, in a recent paper by logician Wilfrid Hodges, the date for the first search algorithm has been pushed back much further: to the third decade of the second millenium, the 1020s. Hodges translates and analyzes a logic text of Persian Islamic philosopher and mathematician, Ibn Sina (aka Avicenna, c. 980 – 1037) on methods for finding a proof of a syllogistic claim when some premises of the syllogism are missing. Representation of domain knowledge using formal logic and automated reasoning over these logical representations (ie, logic programming) has become a key way in which intelligence is inserted into modern machines; searching for proofs of claims (“potential theorems”) is how such intelligent machines determine what they know or can deduce. It is nice to think that theorem-proving is almost 1000 years old.
B. Jack Copeland : What is Artificial Intelligence?
Wilfrid Hodges : Ibn Sina on analysis: 1. Proof search. or: abstract state machines as a tool for history of logic. pp. 354-404, in: A. Blass, N. Dershowitz and W. Reisig (Editors): Fields of Logic and Computation. Lecture Notes in Computer Science, volume 6300. Berlin, Germany: Springer. A version of the paper is available from Hodges’ website, here.
Gaston Tarry : La problem des labyrinths. Nouvelles Annales de Mathématiques, 14: 187-190.