Modelling Infinite Structures with Atoms

(Link).

Author: Mikołaj Bojańczyk (University of Warsaw)

Conference: Workshop on Logic, Language, Information and Computation (WoLLIC 2013), 20-23 August, 2013, Darmstadt, Germany.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: The topic of this week's paper, from an author we've met twice before (here and here) is compactness. Compactness is the property that states that an infinite set of logical sentences is satisfiable (not contradictory) if and only if all the finite subsets of that infinite set are satisfiable. Some logics have the property, but others may not. The importance of this result may not be immediately obvious; it was first discovered by Kurt Gödel for first-order logic as a mere corollary to another theorem (completeness). However compactness went on to be a cornerstone principle of the mathematical field of model theory, which in a broad sense looks at how logical claims can be 'satisfied' by mathematical constructions.

Bojańczyk is interested in shifting first-order logic from its usual set-theoretic foundations to the world of nominal sets, the mathematical model for names in syntax that I've discussed in many places on this blog, e.g. here (in fact, as discussed in that link, Bojańczyk has a somewhat more general notion in mind than is usually meant by 'nominal sets', but such subtleties are orthogonal enough to the gist of this paper that we will pass by them). Making first-order logic nominal means that predicates can involve names, and disjunctions and conjunctions can be infinite, although only 'orbit-finite'.

Compactness is fundamentally a theorem about infinite and finite collections; in nominal sets such issues become a bit subtle. First, each element of a nominal set has what is called the finite support property, which means that it 'depends' on only finitely many names. This is a very helpful assumption in practice, and is motivated by the idea that real syntax can only ever involve finitely many names (even when the syntax might get infinitely large, as I discussed here). Moving up a level, we see that no non-trivial nominal set is finite. However there is a notion something like finiteness that does make sense for nominal sets - that of orbit-finiteness, which essentially says that the nominal set is finitely 'generated', rather like an infinite number of reflections in a hall of mirrors could be generated by a finite number of people standing in its middle.

With familiar notions of finiteness and infinity upended by the nominal sets model, getting a halfway sensible notion of compactness becomes quite difficult. It clearly makes no sense to state the theorem in terms of finite sets of sentences, because there are no interesting finite nominal sets. More surprisingly, the compactness postulate got by replacing the word 'finite' with 'orbit-finite' turns out to be false. In fact to validate that version of the theorem we initially need to jump outside of the nominal sets model entirely by axing the finite support property. This is by no means an illegitimate move but it does create worries, because sets with names but no finite support property are less relevant to computer science applications. However Bojańczyk finishes the paper by putting the rabbit back into the hat by defining what are called 'stratified models', more complicated constructions which have the finite support property but also satisfy compactness by 'approximating' the non-finitely supported models.

Update: Due to workload my next post will be a fortnight after this one.

Formalizing Bounded Increase

(Link)

Author: René Thiemann (University of Innsbruck)

Conference: 4th International Conference on Interactive Theorem Proving (ITP '13), 22-26 July 2013, Rennes, France.

Journal reference: Lecture Notes in Computer Science 7998, pages 245-260, 2013.

Comments: This paper concerns the fundamental problem in computing of determining whether a given algorithm or program terminates, or instead gets stuck in an infinite loop. This is called the Halting Problem. In 1936 Alonzo Church and Alan Turing independently proved that this problem is, in general, insoluble - a program that accepts other programs as input and tells you if they terminate or not is logically impossible. This is the most spectacular result in all computer science, but the proof is really quite simple at its heart - just a little logic game involving feeding hypothetical programs to themselves until they display behaviour that it clearly paradoxical.

This is all a lot of fun, but the practical need to work out whether particular programs terminate or not remains, and so there is an obvious need for techniques that work to prove termination at least some of the time. This paper looks at bounded increase, where each iteration of the program (or some part of it) increases some index until it hits a 'ceiling' that it is provably not permitted to surpass. Because the index increases constantly but cannot do so forever, the program is guaranteed to terminate.

This technique was developed in an earlier paper by Thiemann and co-authors; this paper goes a step further by formalising it in the interactive theorem prover Isabelle/HOL. This sort of formalisation has been discussed several times on this blog - see here for example - and its usual motivation is to increase confidence in a result and detect any subtle errors. This is certainly a motivation here, and Thiemann discusses a number of issues that arise during this formalisation, particularly in the section on 'conditional constraints', but this particular formalisation is also intended to certify proofs produced by specialist termination provers such as AProVE and TTT2. Indeed, a bug in AProVE was uncovered by this research.

This is the second week in a row that Google Scholar Updates has recommended a paper that, while interesting, is not massively related to my research interests. At least this week the reason for the recommendation is a bit more clear - the author's formalisation had to grapple with some (fairly simple) issues involving variable binding, and he considers use of the specialist package Nominal Isabelle to deal with them; the outcome was that the package proved too heavy duty for his requirements and Thiemann instead defined everything needed for binding himself.

Partial Recursive Functions and Finality

(Link).

Author: Gordon Plotkin (University of Edinburgh)

Reference: Computation, Logic, Games, and Quantum Foundations: The Many Facets of Samson Abramsky, Lecture Notes in Computer Science Volume 7860, 2013, pp 311-326.

Comments: As I've mentioned before, there's a nice tradition in science of 'festschrift' volumes put out to celebrate the birthdays of prominent scientists. I myself have published a paper in a festschift for Gordon Plotkin's 60th birthday; here Plotkin himself contributes to a festschrift for the 60th birthday of Oxford computer scientist Samson Abramsky.

Despite this connection, this week's recommendation from Google Scholar Updates is unfortunately not very pertinent to my research interests. That's not to say it's not a nice paper, but Updates is supposed to be a source of personalised recommendations; I have other ways to find papers that are merely nice! The paper is about how partial recursive functions - which is to say, partially computable functions - can be 'represented' (in the technical sense used in the paper) within general category theory. Why has the algorithm recommended this to me? There is some use made of algebra and coalgebra, but that doesn't really seem sufficient grounds to send a paper my way (am I to be recommended every paper at CALCO, for example?). Perhaps publishing in a volume dedicated to Plotkin was enough?

Note: Next week I will be on leave and so my next blog will be in a fortnight.