ALogTime, LogCFL, and threshold circuits: dreams of fast solutions

Our protagonists are the following (DLogTime-) uniform circuit classes

• NC¹ (ALogTime)
• SAC¹ (LogCFL)
• TC⁰ (threshold circuits)

Interesting things can be said about those classes. Things like Barrington’s theorem (NC¹), closure under complementation by inductive counting (SAC¹), or circuits for division and iterated multiplication (TC⁰). Things like TC⁰ recognises the Dyck language with two types of parentheses, NC¹ recognises visibly pushdown languages, or SAC¹ recognises context free languages. (and also the languages recognisable in nondeterministic logarithmic-space).

But how are those classes related to dreams about speed? There are sometimes situations where both fixed width integers and floating point numbers are problematic, but much faster than better alternatives because of explicit hardware support. The dream is to allow arbitrary alternative number formats getting sufficient hardware support to remain reasonable alternatives to the number formats supported explicitly by current hardware.

ALogTime – fast solutions for predictable stack height

Considering how parameter passing to subroutines and a huge part of memory management in mainstream computer languages is stack based, an obvious and natural variation is to restrict the unbounded memory of a Turing machine to be a stack. With those words, I justified copying a part of my answer to my own question yet another time. During my research for that answer, I also learned about Nested Words and Visibly Pushdown Languages and that they can be recognized in LOGSPACE. Recently, I read

The Boolean formula value problem is in ALOGTIME (25 pages)
https://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean/paper.pdf
by S Buss – Jan 1987

I immediately suspected that Visibly Pushdown Languages can also be recognized in ALogTime, and that recognition in LOGSPACE is just a simple corollary. Indeed it is:

Complexity of Input-Driven Pushdown Automata (21 pages)
http://research.cs.queensu.ca/~ksalomaa/julk/p47-okhotin.pdf
by A Okhotin, K Salomaa – 2014

The remarks following the proof of theorem 8 (with the beautiful Figure 3 shown above) say: “Finally, Dymond [12] applied the method of Buss [7] to implement the Mehlhorn–Rytter algorithm [36] in NC¹“. Dymond’s paper is short and sweet:

Input-driven languages are in log n depth (4 pages)
https://www.sciencedirect.com/science/article/pii/0020019088901482?via%3Dihub
by P Dymond – 1988

Polynomial size log depth circuits: Between NC¹ and AC¹ by Meena Mahajan gives a different summary of Dymond’s paper:

Dymond gave a nice construction [14] showing that they are in fact in NC¹. His approach is generic and works not just for VPAs but for any PDA satisfying the following:

1. no ϵ moves,
2. an accepting run should end with an empty stack
3. the height of the pushdown, after processing i letters of the input, should be computable in NC¹. If there is more than one run (nondeterministic PDA), and if the height profiles across different runs are different, then the heights computed should be consistent with a single run. Furthermore, if there is an accepting run, then the heights computed should be consistent with some accepting run.

For such PDA, Dymond transforms the problem of recognition to an instance of formula value problem, and then invokes Buss’s ALogTime algorithm [8] for it.

This post links extensively to external material. It is clear that the reader of this post will not read most of it. The more interesting question is whether I have read that material, or at least plan to read it. The initial plan of this post was to indicate which material I have already read and understood, and which material I still plan to read. But this is unpractical and boring for the reader. What I want to say is that I have read Buss’ paper in principle, but didn’t yet work thoroughly enough through section 7, and I don’t understand yet why Buss says (page 10): “However, we shall use the yet stronger property (c) of deterministic log time reducibility. Although it is not transitive, it is perhaps the strongest possible reasonable notion of reducibility.” Why is DLogTime not transitive? In some of the other papers quoted above, I only read the parts which interested me. And here is another paper by Buss et al which I still plan to read:

An optimal parallel algorithm for formula evaluation (42 pages)
https://www.math.ucsd.edu/~sbuss/ResearchWeb/Boolean2/finalversion.pdf
by S Buss, S Cook, A Gupta, V Ramachandran – Nov 20, 1990

Parallel and distributed computing

The main conclusion of the last section is that ALogTime is quite powerful, because it can recognize languages accepted by input driven stack automata. I wondered whether this result is taught in typical introductions to parallel computing. Here is my sample:

Thinking in Parallel: Some Basic Data-Parallel Algorithms and Techniques (104 pages)
http://www.umiacs.umd.edu/users/vishkin/PUBLICATIONS/classnotes.pdf
by Uzi Vishkin – October 12, 2010

Parallel Algorithms (64 pages)
https://www.cs.cmu.edu/~guyb/papers/BM04.pdf
by Guy E. Blelloch and Bruce M. Maggs – 1996

Limits to Parallel Computation: P-Completeness theory (327 pages)
https://homes.cs.washington.edu/~ruzzo/papers/limits.pdf
by R Greenlaw, H Hoover, W Ruzzo – 1995

Parallel Algorithms (347 pages)
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.466.8142&rep=rep1&type=pdf
by H Casanova, A Legrand, Y Robert – 2008

My conclusion is that it is not taught, at least not explicitly. And I already took care that they would talk about ALogTime by saying (uniform) NC¹. Chapter 10 where Uzi Vishkin talks about tree contraction is related, and NC¹ is discussed in some of the texts. (It should be clear that I didn’t really try to read those texts, and just browsed through them.)

Some words on LogCFL and threshold circuits

I looked for hardware support for LogCFL, as seems possible for NC¹

A more promising approach could be to look for problems complete under appropriate many-one reductions for these classes. The word problem for (or ) would be such a problem for NC¹. The solution of that word problem is nicely scalable, since one can subdivide the word into smaller parts, and thereby generate a smaller word on which the same procedure can be applied again.

That many-one reduction to that word problem is Barrington’s theorem proved in

Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹ (15 pages)
https://people.cs.umass.edu/~barring/publications/bwbp.pdf
https://www.sciencedirect.com/science/article/pii/0022000089900378
by David A.Barrington – 1987

One thing which could still go wrong when trying to use TC¹, NC¹, and SAC¹ for actual efficient computer architectures is that those fast and nice many-one reductions are studied to decision problems, but in the end we are much more interested in computing solutions to function problems. This came up when I described my plans to a friend. But I am not the first to dream about hardware support for those theoretical fast solutions:

Explicit Multi-Threading (XMT): A PRAM-On-Chip Vision
A Desktop Supercomputer (4 pages)
http://www.umiacs.umd.edu/users/vishkin/XMT/index.shtml
http://www.umiacs.umd.edu/users/vishkin/XMT/ICCD09proc-version.pdf
by Uzi Vishkin – 2009

Back to LogCFL: for “closure under complementation by inductive counting,” see:

Two applications of inductive counting for complementation problems (20 pages)
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.394.1662&rep=rep1&type=pdf
by A Borodin, S Cook, P Dymond, W Ruzzo, M Tompa – 1989

and for: “SAC¹ recognises context free languages. (and also the languages recognisable in nondeterministic logarithmic-space),” note that LogCFL = AuxPDA(log n, n^O(1)) = SAC¹ see here. This means the class of log n auxiliary pushdown automaton which run in non-deterministic polynomial time. (Probably “non-deterministic” can also be replaced by “deterministic”. The direct meaning of LogCFL is the class of problems which can be many-one reduced to CFL in deterministic logspace.) I also guess that LogCFL can be solved by a dynamic programming algorithm, since both NL and CFL allow such a solution. (Probably an easy exercise. I just wanted to have LogCFL in this post, since it is part of my dream, and allows to solve interesting problems. And it seems close to ALogTime from a hardware perspective.)

Now to threshold circuits: “TC⁰ recognises the Dyck language with two types of parentheses”. I don’t have a good primary reference at the moment. But this shows that threshold circuits are surprisingly close to ALogTime with respect to their capabilities. And “circuits for division and iterated multiplication,” has some references in the wikipedia article, but I liked the following lecture notes:

Lecture 8: Multiplication ∈ TC⁰ (4 pages)
https://users-cs.au.dk/arnsfelt/CT08/scribenotes/lecture8.pdf
by Kristoffer Arnsfelt Hansen – 2008

The paper by P Dymond – 1988 ends with the following speculation:

This result shows that a large class of cfl’s is in log depths, and it is natural to inquire about the possibility that all deterministic cfl’s, which are known to be in log space, might also be in log depth. One dcfl in log space which is not currently known to be recognizable in log depth is the two-sided Dyck language on four letters [5].

Word Problems Solvable in Logspace
https://rjlipton.wordpress.com/2009/04/16/the-word-problem-for-free-groups/
http://cpsc.yale.edu/sites/default/files/files/tr60.pdf
by RJ Lipton, Y Zalcstein – 1977

It is an interesting question whether ALogTime and LOGSPACE are different for naturally occurring problems. Including LogCFL in the hardware acceleration tries to evade this question. But there are programming approaches specifically focusing on LOGSPACE, since it may model an important aspect of practical algorithms for really big data:

Computation-by-Interaction for Structuring Low-Level Computation
http://www2.tcs.ifi.lmu.de/~schoepp/habil.pdf
by U Schöpp – 2014

Understanding whether ALogTime != PH is hard to prove

I was wondering about how to define function classes for ALogTime: How to transform words over an input alphabet to words over an output alphabet. I wondered whether I should write a mail to Emil Jeřábek. Maybe I only wanted to have a reason to write him, but I didn’t. Instead, I googled my way until I understood even much weaker function classes. Then a naive idea for proving ALogTime != PH crossed my mind: Prove some problem complete for ALogTime under some extremely weak many-one reduction. If that would work, it would be sort of a “fool’s mate”, since no genuinely new idea is needed, just a careful application of well known techniques. So when Scott Aaronson said

On reflection, though, Mubos has a point: all of us, including me, should keep an open mind. Maybe P≠NP (or P=NP!) is vastly easier to prove than most experts think, and is susceptible to a “fool’s mate.”

in HTTPS / Kurtz / eclipse / Charlottesville / Blum / P vs. NP, I couldn’t help but ask him about whether my naive idea has any chance of proving ALogTime != PH, even if just for testing whether he really keeps such an open mind. His answer was: “I don’t know enough to give you detailed feedback about your specific approach”. So he keeps an open mind, even if Stephen A. Cook is slightly more open with respect to the possibility that separating P from weaker classes like NL or ALogTime could be within reach of current techniques:

The Tree Evaluation Problem: Towards Separating P from NL (8 pages)
https://www.cs.toronto.edu/~toni/Courses/PvsNP/CS2429.html
https://www.cs.toronto.edu/~toni/Courses/PvsNP/Lectures/lecture6.pdf
by Stephen A. Cook – 2014

This post has many links to papers like the one above. As if I could justify myself for believing that ALogTime can be separated from P by current techniques. But the links show at least that investing time into this topic is an interesting learning experience. The following sections Weak reductions and isomorphism theorems, and DAG automata link to material which I read (or still plan to read) in order to make progress on ALogTime != P.

Weak reductions and isomorphism theorems

DLogTime many-one reduction already look quite weak. (I don’t understand yet why Buss says (page 10): “However, we shall use the yet stronger property (c) of deterministic log time reducibility. Although it is not transitive, it is perhaps the strongest possible reasonable notion of reducibility.” Why is DLogTime not transitive?) One could go weaker by looking at DLogTime-uniform NC⁰ reduction or even DLogTime-uniform projections (each output symbol/bit depends at most on a single input symbol/bit). But recently, people proposed even weaker uniformity notions than DLogTime:

A circuit uniformity sharper than DLogTime (19 pages)
https://hal.archives-ouvertes.fr/hal-00701420/document
by G Bonfante, V Mogbil – May 25, 2012

This proposed rational-uniformity can be summarized as as writing in binary and applying a finite state transducer to that input for computing the circuit description. I haven’t read the full paper yet. Another recently proposed approach uses descriptive complexity for defining very weak uniformity notions:

The lower reaches of circuit uniformity (16 pages)
https://eccc.weizmann.ac.il/report/2011/095/
by C Behle, A Krebs, K-J Lange, P McKenzie – May 12, 2012

I didn’t understand too much of that paper yet. I tried reading revision 0 (didn’t notice that it wasn’t the latest revision), but revision 1 might turn out to be easier to read: “Results are stated in more clear way, and overall readability was improved.”

Another line of attack for making the many-one reductions weaker is to only allow isomorphisms. It may seem counter-intuitive first that this should be possible, but the Schröder-Bernstein theorem can sometimes be adapted. This is described in two classic papers:

Reductions in Circuit Complexity: An Isomorphism Theorem and a Gap Theorem (17 pages)
https://www.sciencedirect.com/science/article/pii/S0022000098915835
http://ftp.cs.rutgers.edu/pub/allender/switch3.pdf
http://www.cs.cmu.edu/~rudich/papers/ac0reductions.ps
by M Agrawala, E Allender, S Rudich – 1998

Reducing the Complexity of Reductions (9 pages or 22 pages)
https://cseweb.ucsd.edu/~russell/reductions.ps
http://ftp.cs.rutgers.edu/pub/allender/stoc97.pdf
by M Agrawala, E Allender, R Impagliazzo, T Pitassi, S Rudich – 2001

I didn’t read those papers yet, but Algebra, Logic and Complexity in Celebration of Eric Allender and Mike Saks by Neil Immerman gives a nice survey of those results, which I read for a start.

DAG automata

One important property of input driven stack automata is that the dependency graphs will be planar DAGs. For general polynomial time algorithms, the dependency graphs will be general non-planar DAGs (due to variable binding with an unbounded number of variables). In order to learn what is already known about this, I googled “DAG automata”. The first three hits are awesome:

DAG Automata – Variants, Languages and Properties (48 pages)
http://www8.cs.umu.se/education/examina/Rapporter/JohannesBlum_submitted.pdf
by J Blum – May 25, 2015

How Useful are Dag Automata? (26 pages)
https://hal.archives-ouvertes.fr/hal-00077510/document
by S Anantharaman, P Narendran, M Rusinowitch – ‎2004

DAG Automata for Meaning Representation (12 pages)
http://aclweb.org/anthology/W17-3409
by F Drewes – London, UK, July 13–14, 2017

The first and third hit are related, Frank Drewes was the adviser of Johannes Blum. I read both, and they were really worth it. (I only browsed the paper from 2004, just to see that the newer papers really achieved a breakthrough.) They reduce determining which rules are useless to a question about Petri nets, and then provide a solution for that problem: “A Petri net is structurally cyclic if every configuration is reachable from itself in one or more steps. We show that structural cyclicity is decidable in deterministic polynomial time.”

Structurally Cyclic Petri Nets (9 pages)
https://arxiv.org/abs/1510.08331
by F Drewes, J Leroux – ‎2015

On understanding a problem, without solving it

One can understand a problem without solving it. So one can understand why something is a problem and why a solution would be challenging, without being able to come up with a solution. I don’t know whether the best experts in computer science understand P != NP in this sense. I don’t understand it yet, but I have the deeply rooted belief that it can be understood.

And understanding for me also means to be able to read work that others have done, and to see and feel the connection to the questions which interest me.

Conclusions?

This post is too long, but I didn’t really care this time. Since the reader is expected to read at least some of the linked material, it is implicitly even much longer than its nominal length (which is too long) indicates. The initial goal was to write it in order to be able to focus again on more urgent topics. But of course, this didn’t really worked out that way. Still, this post was always intended to be mainly a collection of links to papers I already read or still plan to read in order make progress on understanding ALogTime, LogCFL, and threshold circuits. And I also knew that I would try to justify myself for believing that this topic is worth studying.

Do I believe that the dreams of fast solutions can come true? I don’t know. Uzi Vishkin seems to have made a much more serious effort than I ever will, and even argued his case from an economic perspective:

Alas, the software spiral is now broken: (a) nobody is building hardware that provides improved performance on the old serial software base; (b) there is no broad parallel computing application software base for which hardware vendors are committed to improve performance; and (c) no agreed-upon architecture currently allows application programmers to build such software base for the future

Could proof of work problems for crytocurrency mining provide the incentive to make dreams come true? Who knows, money is important, after all. But personally, I am rather a believer in “constant dripping wears away the stone,” so I think in the long run, it is quite possible that things progress. Probably in ways I cannot even imagine today.

Advertisements

A subset interpretation (with context morphisms) of the sequent calculus for predicate logic

The previous two posts used the sequent calculus with a subset interpretation:

We work with sequents , and interpret the propositions (and ) as subsets of some universe set . We interpret the sequent itself as .

While writing the previous post, there was the temptation to introduce the sequent calculus rules for existential and universal quantification. But the subset interpretation with a fixed universe set didn’t seem helpful for free variables and quantification. But what if we allow different universe sets for different sequents? One way would be to augment the sequent rules to change the universe sets in a well defined way. However, the cut rule and two of the four quantification rules (those that replace an arbitrary term by a quantified variable) are a bit problematic. For them, the universe can sometimes be shrunk down, since a formula or a term was eliminated. Therefore, we just add two separate rules for changing the universe, and apply the sequent rules themselves only with respect to a fixed universe set.

This is the last planed post on the sequent calculus for the moment. (There might be an additional post in this series, extending the subset interpretation to natural deduction.) Since this post will remain vague and unsatisfactory in many ways, a list of related online materials on the sequent calculus seems appropriate: I often consulted the wikipedia article while writing these posts. (I never consulted Sequent Calculus Primer, but it looks nice and has exercises.) This MathOverflow question on introductions to sequent calculus suggests the chapter on Sequent Calculus from Frank Pfenning’s manuscript on Automated Theorem Proving, which I really liked. It also suggests Proofs and Types by Jean-Yves Girard, which was my first introduction to the sequent calculus. It left me unsatisfied, and I agree with Charles Stewart:

A warning: Girard’s style is a little slippery, and it is common for students to say they have read it, who turn out to have absorbed the opinions but little of the results.

I am still slightly ashamed that one of my first questions – when I met a group of academic logicians (with a focus on proof assistants) – was whether they found Girard easy to understand. Girard claims that the sequent calculus is generally ignored by computer scientists, an exception being Logic For Computer Science Foundations of Automatic Theorem Proving by Jean H. Gallier. A nice text, but who has time to read those 500+ pages? This is one reason why I like An Introduction to Proof Theory by Samuel R. Buss.

The sequent calculus rules for predicate logic

We are interested in normal first order predicate logic with predicates and functions. Here a signature with a finite number of predicate and function symbols is given, which include the arity for each of the symbols. The sequent calculus rules for quantification are:

Left quantification rules	Right quantification rules

Those rules look simple, but what do they mean? What is the difference between and ? And how to interpret a sequent with formulas containing free variables? First, is a free variable not occurring in , , or . And means that each free occurrence of in is replaced by . Next, is an arbitrary term, with no restrictions at all on the variables occurring in it. A term is just any reasonable combination of function symbols (from the signature) and variables, like where both and are binary function symbols.

There are many possible interpretations of predicate logic, but that answer just avoids answering the question. The interpretation of a formula or sequent with free variables can be controversial. My previous effort at a subset based interpretations of predicate logic compatible with non-classical logic left out equality, functions and constants. Even so we are talking only about classical logic here, the goal of the following interpretation is to be also applicable more generally. That interpretation will follow naturally once we clarify which models we want to allow.

Models and interpretations of predicate calculus

For the typical interpretations, a model consists of a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol. A straightforward interpretation in that context is that a formula with free variables is a subset of , and a formula without free variables (i.e. a sentence) is either true or false. And for any set of variables, we can interpret any formula whose free variables are included in that set as a subset of . A sequent in this interpretation is true, iff for the subsets formed by the formulas interpreted relative to the set of all free variables in the sequent, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.

This straightforward interpretation above is already a subset interpretation, but we want a slightly more general subset interpretation. For propositional logic, the possible models were given by a set and a subset of for each propositional variable . In predicate logic, the 0-ary predicates take the role of the propositional variables, so we want them to be subsets of . For our generalised interpretation, a model consists of a set (whose subsets are the truth values) and a set (which is the universe where the variables live), a subset of for each -ary predicate symbol, and a function for each -ary function symbol.

The way will enter into the model is to have some implicit context such that formulas like in the formal syntax become in the model. So for any set of free variables, we can interpret any formula whose free variables are included in that set as a subset of . For a given set of variables and a sequent for which the free variables of the formulas are contained in that subset, the a sequent is true, iff for the subsets formed by the formulas interpreted relative that set of variables, the intersection of the subsets on the left side is contained in the union of the subsets on the right side.

(If we have a formula like , we would like to interpret it as a subset of , so we normally use and then just omit it. Here the element is called unit, the set represents truth, and the empty set represents falsehood.)

Context morphisms give life to the subset interpretation

If we have (a sequent of) subsets over , then a (partial) function from to gives us (a sequent of) subsets over by taking inverse images of the subsets. We have

• 
• 
• 

and hence

The direct translation into the language of sequences reads

This just tells us that global substitution is unproblematic. (But is required in case is a partial function, which is easily missed.) However, the more typical function for our purpose is similar to , i.e. a function from to . It is typical, since the expressions grow in complexity for most rules of sequent calculus. Here is an example:

This example also shows, how we can separately change the universe set, and apply the sequent rules only with respect to a fixed universe set. After applying the or rule, we can shrink the universe set. To illustrate, let us first apply the and rule, where we cannot always shrink the universe set:

Here we cannot shrink the universe set.

Now we can shrink the universe set, but only after checking that the sequent no longer depends on . But when we apply , we can always shrink the universe set:

How can we justify this shrinking in terms of images or inverse images? The inverse image under for an arbitrary function (constant) could be a justification. But we don’t really write , and is arbitrary and irrelevant. So the image under might be a nicer justification. But we only have

• 
• 
• 

However, if we assume , then and hence

Doubts about context morphisms and substitutions

Let us apply the above to propositional logic. Surely, from we can deduce . But we cannot justify it from in terms of inverse images. Can we justify it from ? Yes, take the map with . Here and can be arbitrary and . Note that we only need .

How justified are those substitutions into the expressions? Here, we used

Can we justify this? Can such substitutions go wrong? Yes, if is a partial function:

Here fails, but it would work if were a total function. We could have omitted , but then it would fail because of . That was actually the point were I noticed that the restriction is required for partial functions.

The substitutions are justified, because they work for each operation individually:

• 
• 
• 
• 
• 
• 
• 
• 

Treating equality without special rules

Equality can be given by a binary predicate which is a congruence relation for the functions, and compatible with the other predicates. There are different ways to treat equality, and it is important for most interesting applications of predicate logic. A canonical approach is to write the axioms on the left side of the sequent, and use normal deductions. Concrete examples for the required axioms were already given in the last post in the section “Axiomatic theories in predicate logic without falsehood” for the theory of groups and in the section “Axiomatic theories in predicate logic without falsehood” for Robinson arithmetic.

Part of the reason for presenting a subset interpretation for predicate logic was to better understand how predicate logic could work in case of non-classical logics. There are theories like Heyting arithmetic (and Gentzen’s own work), which seem to fit nicely with the interpretation above. But there are also intuitionistic dependent type theories with special rules and equality types, whose possible interpretations remain unclear to me, despite the nice subset interpretation explained above. Maybe Per Martin Löf is right: In the end, everybody must understand for himself (p.166)

Conclusions?

This post was hard for me to write. This is the classical problem when explaining something obvious (predicate calculus). You have to make a lot of words for something which seems obvious, but where the language is missing to properly write down what is going on behind the scenes. I didn’t solve that language problem, but I came up with a natural example of how the obvious thing can fail to be true. That might help the reader to understand for himself.

The content above already became clear to me while writing the previous post. But only after this current post was nearly finished did I notice the restriction in case is a partial function. Which is funny, after I clarified the notion of context morphism which makes sense of that logic without truth from the first post (in this series), I find out that there is an additional restriction that the antecedent should never be empty. My first reaction was that I don’t like this. Maybe I should look for a transformation which turns this logic about partial functions into the logic without negation or falsehood. But my second reaction was that it could make sense, perhaps any logical deduction needs assumptions.

Still the question remains whether there is a reasonable transformation from the logic without truth (and partial functions) to the logic without negation and falsehood. Probably that question will be easy to answer. Somehow one has to take complements, and hope that the structure of the predicate calculus remains intact. It seems to work, but I still have trouble to intuitively understand it. And I want to finish this post now.

Logic without negation and falsehood

In the last post, consideration related to partial functions lead us to present a logic without truth and implication, using the binary minus operation as a dual of implication and substitute for unary negation. But logic without implication and equivalence is strange. So in this post we want to omit negation and falsehood instead.

(This post got surprisingly long. Sometimes I got slightly sidetracked, for example the discussion of the parity function and its sequent rules could have been omitted. But I already tried to remove most of those sidetracks. The real reason for the size explosion are the examples of axiomatic theories in predicate logic. But those had to be discussed, since they make it clear that one can really omit falsehood without loosing anything essential.)

The classical sequent calculus

Before starting to omit logical operations, let us first recall the classical sequent calculus including as many logical operations as barely reasonable. If we limit ourself to constants, unary operations, and binary operations, then we get:

• Constants for truth () and falsehood ()
• An unary operation for negation ()
• Binary operations for: or (), and (), implication (), minus (), nand (), nor (), equivalence (), and xor (). The remaining binary operations add nothing new: reverse implication, reverse minus, first, second, not first, not second, true, and false

We work with sequents , and interpret the propositions (and ) as subsets of some universe set . We interpret the sequent itself as . Let stand for arbitrary finite sequences of propositions.

Left structural rules	Right structural rules

Axiom	Cut

Left logical rules	Right logical rules

The rules for equivalence were taken from here, where they are also proved. Observe that . Clearly is the parity function, which is famous for its computational complexity. It is easy to derive the rules for it (from the rules given above), but those rules have sequents above the line.

The rules for and are obvious. The rules for and are also obvious, if we agree that this should be read as and . Then and , so there is no need for multi-argument versions of nand and nor.

Omitting falsehood from classical logic

If we want to omit falsehood, it is not sufficient to just omit falsehood (). The operations minus () and xor () must be omitted too, since . Also nand () and nor () must be omitted, since and . (They are functionally complete, so the only surprise is the length of the formulas). And if we want to keep truth () or any of the remaining binary operations (or (), and (), implication (), or equivalence ()), then also negation () must be omitted.

But without negation, how can we express the law of excluded middle or double negation? Both and use negation. If we look at proof by cases, then or rather its generalization suggests itself, which is called Peirce’s law. And the sequent calculus suggests , which expresses a nice algebraic property of classical logic. But how do we prove that we get classical logic, and what does that mean?

At least classical tautologies like not using any of the omitted operations should still be tautologies. If “still be tautologies” is interpreted as being provable in the classical sequent calculus, then this follows from cut elimination. The cut elimination theorem says that the rule (Cut) can be avoided or removed from proofs in the sequent calculus. Since for all other rules, the formulas above the line are subformulas of the formulas below the line, only operations occurring in the sequent to be proved can occur in a cut-free proof.

However, my intended interpretation of “still be tautologies” is being provable in the natural deduction calculus. But let us not dive into the natural deduction calculus here, since this post will get long anyway. We still need to clarify what it means that we get classical logic. The basic idea is that logical expressions involving falsehood can be translated into expressions avoiding falsehood, which still mean essentially the same thing. But what exactly can be achieved by such a translation? Time for a step back.

Boolean functions of arbitrary arity

A Boolean function is a function of the form , where is a Boolean domain and is a non-negative integer called the arity of the function. Any Boolean function can be represented by a formula in classical logic. If we omit falsehood, a Boolean function with certainly cannot be represented, for otherwise our goal to remove falsehood would have failed. The question is whether we can represent all Boolean functions with , and whether the complexity of this representation is still comparable to the complexity of the representation where falsehood is available.

A two step approach allows to convert a given representation to one where falsehood is avoided. The first step is to replace by , by , by , by , and by . This step increases the size of the representation only by a small constant factor. The second step is to replace by the conjunction of all input variables. This step increases the size of the representation by a factor in the worst case. It works, since at least one of the input variables is , if is evaluated at an argument different from .

If one can define a new variable, then the factor can be avoided by defining . However, the underlying idea is have a logical constant together with axioms . This is equivalent to the single axiom which simplifies to .

Interpretation of logic without falsehood

When I initially wondered about omitting negation and falsehood from classical logic, I didn’t worry too much about “what it means that we get classical logic” and said

For a specific formula, falsehood gets replaced by the conjunction of all relevant logical expressions.

Noah Schweber disagreed with my opinion that “you can omit negation and falsehood, and still get essentially the same classical logic” and said

First, I would like to strongly disagree with the third sentence of your recent comment – just because (basically) the same proof system is complete for a restricted logical language when restricted appropriately, doesn’t mean that that restricted logic is in any way similar to what you started with.

So I replaced my harmless initial words by

One approach might be to translate as , where is a free propositional variable. It should be possible to show that this works, but if not then we just keep falsehood in the language.

However, these new words are problematic, since is a classical tautology, but is not. My initial words were not ideal too, since the meaning of “the conjunction of all relevant logical expressions” remained unclear.

The intuition behind my initial words was that falsehood is just the bottom element of the partial order from the Boolean algebra. Removing the explicit symbol (name) for the bottom element from the language should be harmless, since the bottom element can still be described as the greatest lower bound of “some relevant elements”. (However, removing the symbol does affect the allowed homomorphisms, since the bottom element is no longer forced to be mapped to another bottom element.)

The intuition behind my new words was an unlucky mix up of ideas from Curry’s paradox and the idea to use a free variable as a substitute for an arbitrary symbol acting as a potentially context dependent replacement for falsehood. We will come back to those ideas in the section on axiomatic theories in predicate logic without falsehood.

What are the “relevant logical expressions” for the conjunction mentioned above? Are , , or relevant logical expressions? The first two are not, since , i.e. the propositional variable itself is already sufficient. The third one is relevant, at least for predicate logic with equality. For propositional logic, it is sufficient to replace falsehood by the conjunction of all proposition variables occurring in the formula (and the assumptions of its proof). For predicate logic, it is sufficient to replace falsehood by the conjunction of the universally quantified predicate symbols, including the equality predicate as seen above (if present).

Axiomatic theories not using negation or falsehood

If the axioms or axiom schemes of an axiomatic theory (in classical first order predicate logic) don’t use negation or falsehood or any of the other operations we had to remove together with falsehood, then we don’t need to explicitly remove falsehood.

Let us look at the theory of groups as one example. If we denote the group multiplication by and the unit by , then the axioms are

• 
• 
• 

We see that neither falsehood nor negation occurs in those axioms. This is actually a bit cheated, since it would seem that implication also doesn’t occur. It actually does occurs in the axioms governing equality. Here are some axioms for equality:

• 
• 
• 

They only use implication, but something like the axiom schema

• 

is still missing. Here is any formula, and may contain more free variables in addition to and . This doesn’t work for us, since this could also include formulas which use negation or falsehood! But at least for the theory of groups, the following two axioms (derived from instances of the axiom scheme) should be sufficient.

• 
• 

Here is a typical theorem of the theory of groups that should now be provable.

Here is an informal proof: Since and , we have . Since and , we have . Since and , we have . If we could show (this was omitted in axioms given above), then the proof would be complete.

Axiomatic theories in predicate logic without falsehood

Let us next look at Robinson arithmetic, which is essentially Peano arithmetic without the induction axiom schema.

1. 
2. 
3. 
4. 
5. 
6. 
7. 

Here are the additional axioms for equality.

• 
• 
• 
• 
• 

Universal quantification has been omitted, but that should not worry us here. We see that the first axiom is the only one using falsehood. We could replace it by

1. 

Or we could also introduce a constant and replace by the axioms

0. 
1. 

The second approach has the advantage that if we add the induction axiom schema to get Peano arithmetic, we can just replace falsehood by the constant . The first approach has the advantage that is shows that falsehood was never really required for the induction axiom schema.

The second approach comes closer to my motivations to remove falsehood from the language. I wanted to avoid negation and falsehood, because if there is no (bottom) element connecting everything together, then the damage caused by the principle of explosion can be restricted to specific domains of discourse. I also had the idea to use more specific propositional constants instead of falsehood. For ZFC set theory, one could use one propositional constant for the axiom asserting the existence of the empty set, and another propositional constant for the axiom asserting regularity. However, as soon as one adds the axioms and , both constants will probably turn out to be equivalent.

Conclusions

Such a long post, for such a trivial thing as removing falsehood from the language. At least it should be clear now that one can really remove falsehood if desired, and what it means that one doesn’t loose anything essential. But is there anything to be gained by removing falsehood? The initial idea to remove falsehood came from the rule (suggested by the sequent calculus), which characterises classical logic by a nice algebraic property (not involving negation or falsehood). The motivation to finish this post came from the realisation that implication is the central part of logic. I just read this recent post by Peter Smith on the material conditional, and realised that one really gains something by removing falsehood: the counterintuitive material conditional goes away, and implication becomes the first class citizen it should have always been.

The counterintuitive part didn’t really disappear. The material conditional decomposes into the two sequents and . The proof sketch for those is and . The proof of the second doesn’t even use the special properties of classical logic, but this part is the counterintuitive one: Why should be true, if ? Well, the intuitive everyday logic is more a sort of modal logic than a propositional or predicate logic.

Logic without truth

Pi is wrong! But so what? It is neither new, nor complicated enough to count as real math! And suggestions that  or  might be even better show that it not clear-cut either.

I recently invested sufficient energy into some logical questions to make real progress. But while telling friends and fellow logicians about it, I realized how irrelevant all my results and conclusions will be. I will have to publish them in an appropriate journal nevertheless, since they continue David Ellerman’s work on partition logic. Not publishing them would be dismissive towards the value of David Ellerman’s work, and he really invested lots of effort into it, and believes in its value. I won’t talk about those results here, since I don’t know how it would impact my ability to publish them.

Let’s have some fun instead, stay extremely close to classical logic, and still demonstrate a logic without truth. And let’s get back to Gerhard Gentzen.

Partial truths

I am fond of partial functions. For a partial function , we have

• 
• 
• 
• where

But is only true if is a total function. Especially is only true (even for specific ) if is total, since otherwise

Let’s also prove one of the other claims:

Note that . So the preserved operations are “and”, “or”, and “xor” if interpreted from a logical perspective. It would be nice if implication were preserved too. This seems hopeless, since is always true, and truth is not preserved. But we do have , which means that the external implication given by the order is preserved. So we should be able to turn this into a logic, where internal truth is not preserved under context morphisms.

Gerhard Gentzen’s sequent calculus

The sequent calculus is a proof calculus with significant practical and theoretical advantages compared to more obvious proof calculus systems. It works with sequents . The propositions (and ) could be logical formulas like (the 4-th Peano axiom). They can also be interpreted as subsets of some universe set , which is sufficient for understanding the basics of the sequent calculus. Then the sequent itself is interpreted as .

Left structural rules	Right structural rules

Here stand for arbitrary finite sequences of propositions. The structural rules may be relatively boring. The following global rules are slightly more interesting

Axiom	Cut

None of the rules up to now has used any logical constant or connective. They can be verified directly for the subset interpretation. The following logical rules can only be verified after the (intended) interpretation of the logical connectives has been fixed.

Left logical rules	Right logical rules

One possible interpretation for these connectives in terms of subsets would be , , , , and .

But it may be more instructive to see an interpretation where one of the classical logical rules is violated. So let us use instead, where is the interior operator of some topological space. The propositions (and ) are interpreted as open subsets in this case. The rule is violated now, and has to be replaced by the rule . This gives us the intuitionistic sequent calculus, which exactly characterizes the valid conclusions of intuitionistic logic.

To see that  is violated, let , correspond to , , and . Above the line we have , which is true. Below the line we have , which is false.

An evil twin of sequent calculus

Note that implication satisfies or rather . Let us replace implication by minus. Note that minus satisfies with . Then we get the following two rules instead of and .

Of course, we also remove and from the language together with the rule . This sequent calculus is still as sound and complete as the original sequent calculus. But we no longer reason about implication, but only about minus. Some sort of implication is still present in , but it is no longer mirrored internal in the language of the logic itself. So this is our logic without truth.

I don’t really know (or understand) whether this sort of context morphism has any sort of relevance, and whether that logic without truth occurs anywhere in the real world. Is there any relation to the fact that it is easier to deny the relevance or truth of a given conclusion than to prove that it is important and true? What I like about that logic is the asymmetry between implication and falsehood, because I wanted to find naturally occurring asymmetries in mathematical hierarchies and logic. Even for the results that I do want to publish, I have the same problem that I don’t really understand the relevance of the corresponding context morphisms, whether there even should be context morphisms, and whether my proposed context morphisms are the correct ones.

Conclusions?

That post initially also contained a logic without falsehood, or rather a logic where falsehood is not used. But it started to get long, and this post is already long enough. Not sure whether this was really a good idea, since the explanation of the sequence calculus was also intended to better understand how such a logic with a reduced set of logical constants and connectives still maintains its main features. Maybe I will manage to create another blog post from the removed material. Or maybe nobody including myself cares anyway, as already indicated at the beginning. Or maybe I should better use my time to finish the paper about the results I wrote about at the beginning, and submit them to…

Learning category theory: a necessary evil?

The end of my last blog post (about isomorphism testing of reversible deterministic finite automata) explained how category theory gave me the idea that the simplified variant of my question about permutation group isomorphism should be easy to solve:

The idea to consider the case where the group is fixed came from reading an introduction to category theory, because those morphisms of left -sets felt like cheating (or oversimplifying) to me. So I guessed that this case should be easy to solve, if I would only…

I hinted that this felt like cheating (or oversimplifying) to me, but I realized three month later that my original question could be reduced to the simplified variant by a brute force technique exploiting the fact that minimal generating sets of groups are very small. So it turned out that category theory was actually helpful and not cheating at all.

Why does a mathematician interested in logic, (semi-)lattice theory and universal algebra reads an introduction to category theory? Because it is a good readable (medium level) German book on a mathematical subject I’m currently interested in.

And it is written by Martin Brandenburg, who always helped people like me, when they got stuck on questions related to category theory. If the explanations and examples in the book are as good as his contributions on MathOverflow and the MathStack Exchange site, then I would be fluent in both theory and practice after finishing that book.

But why am I interested in category theory?

• There are all those forgetful functors with left adjoints in universal algebra. And when doing semigroup theory, switching freely between monoids and semigroups by adjoining an identity is very common. Seems like a good idea to understand this.
• I like inverse semigroups, which are closely related to partial bijections, and hence to partial functions. Mathematicians don’t like partial functions, but category theory at least admits that each function has a domain and a codomain. Some existing work on partial functions has been phrased in the language of category theory.
• I have read basic introductions to category theory, but kept forgetting about adjoint functors. Then I worked two times thru a reasonable introduction to the adjoint functor theorem (by Chris Henderson), and hopefully settled this problem.
• I would like to better understand the Ext and Tor functors in group cohomology, and diagram chasing like the snake lemma.
• I like non-classical logic, including intuitionistic logic, linear logic and partition logic. My understanding of non-classical logic is mostly based on lattice theory. Sadly, lattice theory is a very confusing name, and it has only few followers. So if I translate my ideas about non-classical logic and lattice theory into the language of category theory, then I should be able to reach a more relevant audience.
• I liked assembly language when I started to program, and set theory feels similar to assembly language. Category theory is one alternative to get around all the engrained prejudices about logic and model theory embedded into mainstream ZFC set theory.

Maybe I could find more reasons, but let’s talk about the content now

• Category theorists seem to have a strange relation to calculations. The introduction to the adjoint functor theorem by Chris Henderson often has imbalanced parenthesis in the formulas (my printout has those marked on page 6, 7, 11, and 12), indicating that the formulas have at least some errors. Sometimes (like the near the bottom of page 7) I couldn’t figure out what the correct formula was supposed to be.
• The book by Martin Brandenburg has fewer of those unnecessary errors, but it is still annoying if is written instead of when explaining the Yoneda construction on page 109, which is difficult for me even without such errors.
• I actually had to return the book while reading chapter 5 on the Yoneda construction a second time. I bought my own copy of the book in the meantime, but haven’t resumed reading yet.
• Category theorists are similar to physicists in not noticing the places where the computational complexity can explode. So they claim only the universal property would be important, and the concrete representation an unimportant detail. But identity testing for the free modular lattice on 4 generators is undecidable, it is NP-complete for the free Boolean algebra, and trivial for free abelian groups. The universal algebra people are much more aware of such niceties, something which can easily get lost when doing universal algebra through the lens of category theory.

My overall conclusion is that I learned quite a bit from working through the category theory book, but that it were the concrete examples from which I benefitted most. But I still would not really recommend learning category theory to somebody who doesn’t know yet why he wants to learn it.

A canonical labeling technique by Brendan McKay and isomorphism testing of deterministic finite automata

A deterministic finite automaton (DFA) is a 5-tuple, , consisting of

• a finite set of states
• a finite set of input symbols
• a (partial) transition function
• an initial state
• a set of accept states

An isomorphism between two DFAs and is a bijection such that , and .

Isomorphism of DFA is GI complete

Without further restrictions, the problem of testing whether two DFAs and are isomorphic is as difficult as testing whether two graphs and are isomorphic, i.e. the problem is GI complete. A simple construction shows that the problem of testing whether two digraphs and are isomorphic reduces to DFA isomorphism testing.

For a digraph , construct the DFA with , , , and defined for by , and for by .

Obviously, the digraphs and are isomorphic iff the DFAs and are isomorphic.

A canonical labeling technique

A reasonable restriction is to require that every state in is reachable from . Let . Then a unique labeling of can be produced by a breadth first search of starting at as follows: You have a queue (first-in, first-out store), initially containing only . Repeatedly do this: remove the state at the head of the queue, say , then push into the queue (at the tail) those of (in that order) which have never previously been put into the queue. Since every state is reachable from , every state is put into the queue eventually. Stop when that has happened and define to be the order in which states were put into the queue. Since this labeling is independent of any ordering or labeling of , it fixes the only bijection between and that can possibly lead to an isomorphism between and . It is easy then to check whether they are actually isomorphic.

Attributing that algorithm to Brendan McKay would be misleading, because it is so obvious. For example J.-E. Pin described the same algorithm (using depth first search instead of breadth first search) earlier, as an answer to a question about finding an isomorphism between finite automata.

Brendan McKay’s canonical labeling technique

The context in which Brendan McKay described his canonical labeling technique was actually slightly more complicated, because there was no distinguished state , and the state space of the automaton wasn’t required to be weakly connected. But instead, was injective for all . If we drop the requirement that is a total function and allow it to be partial, then we end up exactly with the reversible deterministic finite automata, described earlier on this blog. Brendan McKay’s technique generalizes effortlessly to this setting, as does the original context (where group actions are replaced by inverse semigroup actions).

Above are some colored digraphs corresponding to reversible deterministic finite automata (the initial state and the final states are ignored). We continue to describe the canonical labeling technique in terms of deterministic finite automata. For each state , we can produce a unique labeling (of the weakly connected component containing ) by a breadth first search of starting at as above, expect when we remove the state from the head of the queue, (instead of ) we have to push into the queue (at the tail) those of (in that order) which are defined and have never previously been put into the queue.

But how can we create a canonical labeling of from the unique labelings ? Just take (one of) the lexicographically smallest labelings of each block, and sort the block lexicographically based on those labelings. The lexicographical order in this context is defined by encoding a labeled block in some reasonable (unique) way as a string, and comparing those strings lexicographically. It’s a good idea to modify this lexicographical order to first compare the lengths of the strings, but this is already an optimization, and there are more possible optimizations, as described in Brendan’s answer. These optimizations are the context of the following remark at the end of his answer:

The graph is actually a deterministic finite automaton (at most one edge of each colour leaves each vertex). There could be faster isomorphism algorithms out there for DFAs, though I’m dubious that anything would work faster in practice than a well-tuned implementation of the method I described.

This remark was actually the main motivation of this blog post, i.e. to investigate the relation of Brendan’s technique to isomorphism testing for DFAs. If there were really faster isomorphism algorithms out there for DFAs, then either they would not be applicable to the problem which Brendan had solved there (if they rely on reachability from ), or they would also solve GI itself in polynomial time (which is highly unlikely).

Conclusions?

The truth is I have been yak shaving again, even so I explicitly told vzn that I didn’t want to get too involved with GI. How did it happen? Fahad Mortuza (aka Jim) asked me for help refuting his attempts to solve GI in quasipolynomial time. (This is completely unrelated to the recent breakthrough by László Babai, except maybe that he triggered some people to spend time on GI again.) While working with him, I realized that permutation group isomorphism might be more difficult than group isomorphism, and asked some questions to get a better feeling for the relation of permutation group isomorphism to GI. The idea to consider the case where the group is fixed came from reading an introduction to category theory, because those morphisms of left -sets felt like cheating (or oversimplifying) to me. So I guessed that this case should be easy to solve, if I would only understand how Brendan McKay handles automorphisms of graphs efficiently. Then Brendan McKay himself explained his technique (for this case) and I discovered the interesting connection to inverse semigroups and finite automata, so I decided I had to write a blog post on this. Now I have written this post, just to avoid having another item on my ToDo list which never gets done.

On Zeros of a Polynomial in a Finite Grid: the Alon-Furedi bound

This paper is a great achievement. Not just that it formulates and proves a very appropriate common generalization of Alon-Furedi, Schwartz-Zippel and other theorems, it is well organized, easy to read, and very inspiring.

Anurag's Math Blog

My joint paper with Aditya Potukuchi, Pete L. Clark and John R. Schmitt is now up on arXiv: arXiv:1508.06020.

This work started a few months back when I emailed Pete and John, pointing out an easy generalization of Chevalley-Warning theorem using something known as the punctured combinatorial nullstellensatz, after reading their paper on Warning’s second theorem: arXiv:1404.7793. They got pretty excited about it and we started discussing some related things. Finally, it’s not the generalization of Chevalley-Warning that this paper is about but the theorem of Alon-Füredi itself, which is the main tool they used in their paper to generalize Warning’s second theorem. In our discussions we found several unexplored connections between this elementary result on polynomials and results from different areas of maths. My friend Aditya joined us in between with his amazingly simple proof of Alon-Füredi which, along with the annoying realization that a result of DeMillo-Lipton-Zippel doesn’t…

View original post 124 more words