As promised, I’ll be posting revised chapters for a second edition of GWT in bite-sized instalments. So I’ve added just a dozen pages this time, covering two more chapters (just stylistic/clarificatory revisions of the old chapters 4 and 5). I have also — for any new readers — now included the front matter with a revised Preface. So here they are, the first five chapters.
According to Littlewood in his Miscellany, the great Edmund Landau “read proof-sheets [for one of his books] seven times, once for each of a particular kind of error”. I confess I can’t claim such levels of meticulousness. So I say it, and mean it, every time: corrections and friendly suggestions are immensely welcome at this stage. Now really is the time to let me know if you had issues with the first edition!
Updated, corrected with many thanks again to David Furcy.
I am wondering if you have thought about making a version of your amazing texts available as open source like the Open Logic Project books. I so much like to use your books for teaching but I often use the OLP since I can add small changes based on each course, easily make lecture notes out of them, etc. But If I wanted to do that with your texts, I would have to type up the whole book!
At the moment, the source codes of the various books are a complete mess … and e.g. in the case of IFL, over 80 different files (for separate chapters, end-of-chapter exercises, etc.).
Maybe one day I will make them open source (as well as open access), when the books are in a stable state, and I have stopped tinkering with them. But not yet!
I don’t know if this affects GWT in any significant way, but I’m still not completely clear on how primitive recursion should be understood in programming-language terms. ‘for’ loops with an explicit upper bound are in; unbounded ‘while’ loops are out (because they might never terminate?)
However, there can be loops without an explicit bound on the number of iterations that are nonetheless known to iterate only a finite number of times, for instance because the data structure they’re iterating over has to be finite. For example, in some languages that have lists (such as pure Lisp), lists are necessarily of finite length, and there can be a looping construct like this
for ⟨variable⟩ in ⟨list-valued-expression⟩: …
Also, there’s no length field, and calculating the length takes a loop of the above sort
len = 0
for ⟨variable⟩ in ⟨list-valued-expression⟩: len = len + 1
Such loops can be rewritten as ‘while’ loops. For example
len = 0
tail = ⟨list-valued-expression⟩
while tail is not empty:
— len = len + 1
— tail = rest(tail)
(I’m using ‘–‘ just for indentation. ‘rest’ is an operation on singly-linked lists that returns a list minus its first element. Angle brackets delimit syntactic placeholders a.k.a. nonterminal symbols in the grammar.)
So: does a program that uses such loops count as primitive recursive? I think when we discussed this before you said it didn’t. If it doesn’t, though, why doesn’t it? It can’t be because the loop might never terminate, because it always would. However, if ‘for-in’ loops are allowed, why not the equivalent ‘while’ loops too?
Primitive recursion could be defined syntactically, I suppose. In effect, there’d be a canonical PR language (which didn’t include ‘while’ or ‘for-in’) and only programs that could be translated fully into that language would count as primitive recursive. Is that how ‘primitive recursive’ is meant to be understood?
I’ll look carefully at what I say when I get round to revising the chapter. But as I recall, the arm-waving talk about “for” loops and “while” loops was not supposed to be load-bearing — and maybe the particular way things are put there are too coloured by my ancient-history memory of some early languages.
I certainly, though, wouldn’t want to say that it is *programs* that are or are not primitive recursive.