Review: Three Views of Logic: Mathematics, Philosophy, and Computer Science

I read this book largely by accident, because I was attracted by the title. As an academic in (or rather, on the edge of) computer science, I come across logic regularly, both in teaching and research. Mathematics underpins almost everything I do, and I’m certainly interested in whether a mathematician’s view of logic differs significantly from that of a theoretical computer scientist (as a keen reader of mathematics, I’m well aware that standard mathematical practice of proof differs quite strongly from the formal approach studied in computer science, but this isn’t quite the same thing!) I once had a strong interest in philosophy, most significantly in epistemology, which is being rekindled by my involvement in education at the school level, and so combining all these factors, the title was very appealing. What I actually discovered when I started reading wasn’t exactly what I expected. But this book turns out to be an excellent, crystal clear, textbook suitable for undergraduates and those with just a limited level of mathematical maturity. The book is explicitly partitioned into three sections, but in practice I found that the first two sections, proof theory and computability theory (the “maths” and the “computer science”) were very familiar material for any computer scientist, and from my perspective there was no very clear difference in approach taken, just a difference in the range of topics covered.

Part 1, by Loveland, covers propositional and predicate logic, with a particular focus on automated proof by resolution. I found the description of resolution to be very clear, with a particular focus on the difference between resolution for propositional and predicate logic, and with one of the clearest descriptions of completeness results I’ve seen.

Part 2, by Hodel, covers computability theory. Again, the clarity is exemplary. The first chapter discusses concepts informally, the second precisely defines two machine models in a way very accessible to a computer engineer (effectively one supporting general recursion and one supporting only primitive recursion) and discusses their relative computational power. The insistence of an informal discussion first makes these distinctions come to life, and allows Hodel to frame the discussion around the Church-Turing thesis. The focus on compositionality when preserving partial recursiveness, and the emphasis on the ‘minimalisation’ operator (bounded and unbounded) was new to me, and again very clearly presented. Most introductory texts I’ve read only tend to hint at the link between Gödel’s Incompleteness Theorem and Church’s Undecidability Theorem, whereas Hodel makes this link precise and explicit in Section 6.6, Computability and the Incompleteness Theorem.

Part 3, by Sterrett, covers philosophical logic. In particular, Sterrett considers the existence of alternatives to (rather than extensions of) classical logics. She focuses on the logic of entailment aka relevance logic introduced by Anderson and Belnap, into which she goes into depth. This logic comes from rethinking the meaning ascribed to the connective, $\rightarrow$ , logical implication. In classical logic, this is a most confusing connective (or at least was to my students when I taught an introductory undergraduate course in the subject long ago). I would give my students examples of true statements such as “George is the Pope” implies “George is Hindu” to emphasise the difference between the material implication of classical logic and our everyday use of the word. It is exactly this discrepancy addressed by Anderson and Belnap’s logic. I was least familiar with the content of this part of the book, therefore the initial sections came as something of a surprise, as I found them rather drawn out and repetitive for my taste, certainly compared to the crisp presentation in Parts 1 and 2. However, things got exciting and much more fast moving by Chapter 8, Natural Deduction, where there are clear philosophical arguments to be had on both sides. In general, I found the discussion very interesting. Clearly a major issue with the line of reasoning given by my Pope/Hindu example above is that of relevance. Relevance might be a slippery notion to formalise, but it is done so here in a conceptually simple way: “in order to derive an implication, there must be a proof of the consequent in which the antecedent was actually used to prove the consequent.” Actually making this work in practice requires a significant amount of baggage, based on tagging wffs with relevance indices, which get propagated through the rules of deduction, recalling to my mind, my limited reading on the Curry-Howard correspondence. The book finishes with a semantics of Anderson and Belnap’s logic, based on four truth values rather than the two (true/false) of classical logic.

I can’t emphasise enough how easy this book is to read compared to most I’ve read on the subject. For example, I read all of Part 1 on a single plane journey. I will be recommending this book to any of my research students who need a basic grounding in computability or logic.

Math Circle Session 3: Knots

Today saw the third session of the primary school math circle we’ve been running for kids in Year 2 to Year 6. (I was absent for Session 2, where my wife covered mathematical card tricks.)

Today we looked at knots, drawing inspiration from Rozhkovskaya’s book as well as Adams’ introduction to knot theory. In particular, we covered the following points:

(Medial) graph representations of knot projections, moving backward and forward between them (see http://en.wikipedia.org/wiki/Knots_and_graphs)
The importance of assigning an (under/over) decision to crossings
Getting the kids to think of their own ideas for what knot equivalence might mean (shape, size, rotation, deformation – of what type) etc.

The key innovation we used here, which I think really brought the session to life, was to get the kids actually physically making the knots using Wikkistix, wax-coated string which allowed them to make, break, and remake their knots.

The kids really ran with this, and made their own discoveries, in particular:

One child discovered that some knots corresponding to the graph $K_3$ could be manipulated to produce the unknot, some could not.
A child discovered that it is possible to produce two interconnected knots, forming a link. Another child came to the same conclusion from the graph representation.
Consider the graph with vertex set $\{v_1,\ldots,v_n\}$ and edge set $\{\{v_i,v_{i+1}\} | 1 \leq i \leq n-1\}\} \cup \{\{v_n,v_1\}\}$ (is there a name for these graphs?). One child completely independently found that for $n$ even, this corresponds to a link of two knots, whereas for $n$ odd, it corresponds to a single knot.

I certainly had a lot of fun this afternoon – I hope they did too!

Where High Performance Reconfigurable Computing Meets Embedded Systems

I have just returned from attending HiPEAC 2015 in Amsterdam. As part of the proceedings, I was asked by my long-time colleague Juergen Becker to participate in a panel debate on this topic.

Panels are always good fun, as they give one a chance to make fairly provocative statements that would be out of place in a peer review publication, so I took up the opportunity.

In my view, there are really two key areas where reconfigurable computing solutions provide an inherent advantage over most high performance computational alternatives:

In embedded systems, notions of correct or efficient behaviour are often defined at the application level. For example, in my work with my colleagues on control system design for aircraft, the most important notion of incorrect behaviour is would this control system cause the aircraft to fall out of the sky? An important metric of efficient behaviour might be how much fuel does the aircraft consume? These high level specifications, which incorporate the physical world (or models thereof) in its interaction with the computational process, allow a huge scope for novelty in computer architecture, and FPGAs are the ideal playground for this novelty.
In real time embedded systems, it is often important to know exactly how long a computation will take in advance. Designs implemented using FPGA technology often provides such guarantees – down to the cycle – where others fail. There is, however, potentially a tension between some high level design methodologies being proposed and the certainty of the timing of the resulting architecture.

Despite my best attempts to stir up controversy, there seemed to be very few dissenters to this view from other members of the panel, combined with a general feeling that the world is no longer one of “embedded” versus “general purpose” computing. If indeed we can draw such divisions, they are now between “embedded / local” and “datacentre / cloud”, though power and energy concerns dominate the design process in both places.

Starting a Math Circle

I’ve been intrigued for a couple of years by the idea of math circles. Over Christmas I finally plucked up the courage to start one at a local primary school with my wife, a maths teacher. The school was happy, and recruited six pupils from Year 2 to Year 6 to attend.

Armed with a number of publications from the American Mathematical Society’s Mathematical Circles Library, our first task was to find a suitable topic for Session 1. Our primary goal was to find a topic that was clearly not everyday school maths, preferably as far away from the National Curriculum as possible, and ideally including practical activities.

In the end, we decided to look at Möbius strips. In the traditional of journal keeping for Mathematical Circles, I thought I would report the experience here in case anyone else wants to give it a go. In particular, we took the following approach:

Make zero half-turn bands (loops) and colour the outside in one colour. Then colour the inside in a different colour.
Repeat with a one half-turn band. This caused some surprise when it became apparent that one colour coloured the whole band.
Predict what would happen if you cut the zero half-turn band down the centre (prediction was universally that you’d get two zero half-turn bands). Try it.
Now predict for the one half-turn band. Children were less sure about this case, but the most popular prediction was two half-turn bands. More surprise when it turned out to create a single four half-turn band. One child then went off on his own exploring what happened when you cut one of these four half-turn bands (two four half-turn bands).

By this time some of children were already off under their own steam, trying out their own experiments. This was great, but even with only six children and with two adults, I found it hard to pull together the outcomes of these experiments in any systematic way in real time.

Eventually we discovered together that:

If the initial number of half-turns is odd, cutting gives you one larger band with more half turns. (I was hoping we’d be able to quantify this, but it turns out to be very difficult to count the number of half-turns in a strip – even for me, let alone for the younger children!)
If the initial number of half-turns is even, cutting gives you two interlinked bands with the same number of half-turns.

This took up pretty much the whole 50mins we had for Session 1, though I did briefly try to show them an explanation of why this might be the case, following the diagrammatic representation in this document from the University of Surrey. I probably didn’t leave enough time to do this properly, and they were anyway keen on cutting and exploring by that time, so with hindsight I probably should have just left them to it.

What delighted me was the child who wanted to take home his Möbius strip to show his dad. So, not a bad start to the Math Circle. Let’s see how we get on!