Logic

These are three things I've written since I've been in Bolivia. They were all attempts to persuade people to engage in rational discussion with me. This is what I do best, and this is all I have ever really wanted to do. But the world at large seems to have had other ideas. Nevertheless, I still hope to be able to do more on this, one day, God willing.

This very brief two page note concerns a problem with the conventional wisdom on Tarski's semantic theory of truth.

This is a seven page essay about a common fallacy in three different parts of mathematical logic, which are 1) formal calculi such as lambda calculus and also variable-free combinator calculi, such as occur in Hilbert-style proof systems. 2) Mechanical computing machines like Turing's a-machines, and 3) formal proof systems, such as the ones used by Kurt Gödel in his incompleteness theorems. This is a cut-down version, only four pages, of the same essay, because some people seemed not to know what to attack in the first version, and so they just attacked everything in sight, which wasn't very helpful to me. I let my irritation, with Larry Paulson in particular, show in the last paragraph! 😂

This short note is about conflicting notions of inconsistency in formal systems such as Peano Arithmetic.

These three, together with Damas and Milner's semantic model of polymorphic type systems with both free and bound type variables in the object language might suggest some interesting directions in which ideas about very large models could be explored.

This is my tiniest of ideas, that entered my three-year-old mind when I made a machine out of plastic drinking straws and pipe-cleaners, which I imagined could actually do something. But I lost it, and couldn't remember how to make another one. And I cried, and cried, and cried.

There is one more thing that would be useful. It is the 'C' language function library I wrote between July and October 1989, while I was at my parents' flat in Bath. The library was an interpreter for regular expressions, and translated them into either deterministic or non-deterministic Finite Automata. The non-deterministic automata could involve recursive back-tracking, which was the only intellectual contribution I made. Otherwise, the functions were standard "Red Dragon Book" stuff. I note that more recent editions have a different sort of dragon. One that looks more like a purple dinosaur to me. This is why I called it the Red Dragon Book:

The potential use for this recursive backtracking is in automatically scanning abstractions from the input data to the automaton, that are in some sense optimal, and are the simplest abstractions which regenerate the input string. Maybe Larry Wall at NASA did something similar, in which case the perl regular expressions can do this too. I heard that Larry Paulson uses perl a lot, so maybe ask him about it. I sold two copies of the library: one to Mark Primavesi of Reading, Berks., England, and the other to Peter Kelway, Aptech Systems, Ponteland, Newcastle-upon-Tyne, England. I may also have given a copy to Nik Shaylor before he went to work for Sun Microsystems in California. There was also a copy on the hard disk of my computer which I sold to some guy in Bath, sometime in 1991/2, I think.

I think Peter Sewell at Cambridge may know something about this too, because he once asked me "Do you know how to parse a random grammar?" I said "what the fuck is a random grammar? One that changes as you parse input?" And he said "Oh, I mean an arbitrary grammar." And that is an unsolved problem, or it was at the time he asked, so why ask me whether I knew how to do it? It's like asking someone "Do you know how to solve the halting problem?" But I think now that that library I wrote could have been adapted fairly easily to parse recursive regular expressions, and it would be able to parse arbitrary grammars in polynomial time. I think Tom Ridge was trying very hard to lead me on to this, but by then I had forgotten about that work I had done.

In the PDF of the first edition, there is no mention of backtracking, but I have a recollection that it was mentioned in one of the exercises. Instead, there is this piece on KMP matching, which I don't recall ever reading before. Maybe Vaughan Pratt can help?

Well, I choose to interpret this as La Victoria! Peanut Butter Wolf, let the people have technology!