Publications

Abstract. We show that the Mean Value Theorem is provable in the weak subsystem RCA₀ of second order arithmetic. Note that it is impossible to prove in RCA₀ that every continuous function on the interval [0,1] attains maximum and minimum values, and that the usual proof of the Mean Value Theorem makes use of this theorem.

Abstract. The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron, 2000).

Abstract. We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.

Abstract. The universal Horn theory of relational Kleene algebra with tests is of practical interest, particularly for program semantics, where Horn formulas can be used to verify correctness of programs or compiler optimizations. Unfortunately, this theory is known to be Pi-1-1-complete. However, many formulas arising in practice fall into fragments of the theory that are of lower complexity. In this paper, we see that the location of occurrences of the Kleene asterate operator * within a formula has a great impact on complexity. Using syntactic criteria based on the location of *, we give a fragment of the theory that is Sigma-0-1-complete, and a slightly larger fragment that is Pi-0-2-complete. We show that the same results hold over *-continuous Kleene algebras with tests. The techniques exhibit a relationship between first-order logic and the Horn theories of relational and *-continuous Kleene algebra, even though the theories are not first-order axiomatizable.

Abstract. The universal Horn theory of relational Kleene algebra with tests (RKAT) is of practical interest, particularly for program semantics. We develop an (infinitary) proof system, based on well-founded trees of finite automata, which is sound and complete for this theory. A small modification of this system yields a proof system which is sound and complete for the universal Horn theory of *-continuous Kleene algebras with tests (KAT*). This sheds light on the relationship between RKAT and KAT*.

Abstract. Kleene algebra arises in many areas of computer science. In particular, Kleene algebra with tests provides an algebraic way of representing and studying programs. When using Kleene algebra for this purpose, one generally wishes to restrict attention to algebras built from binary relations on some set of states, since they capture a common model for computation; these are called relational Kleene algebras.

The equivalence of two programs, which is useful for verifying program correctness or compiler optimizations, can be expressed as an equation in Kleene algebra. The equational theory of relational Kleene algebra is already well understood, and decidable. One often needs to reason about programs under certain hypotheses about the semantics of individual program fragments, however, and this requires the use of Horn formulas.

We show that the Horn theory of relational Kleene algebra is Pi-1-1-complete (highly undecidable). We then exhibit special types of Horn formulas for which the complexity is much lower. We give an infinitary proof system for the Horn theory of relational Kleene algebra that is sound and complete, along with a closely related system that is sound and complete for the Horn theory of *-continuous Kleene algebras. Despite being infinitary, these systems have practical applications; in particular, proof theoretic arguments over these systems can yield new decidability results.

Abstract. Given a universal Horn formula of Kleene algebra of the form r=0 --> s=t, it is already known that we can efficiently construct an equation s'=t' which is valid if and only if r=0 --> s=t is valid. This is an example of elimination of hypotheses, which is useful because the equational theory of Kleene algebra is decidable while the universal Horn theory is not. We show that hypotheses of the form r=0 can still be eliminated in the presence of other hypotheses. This lets us extend any technique for eliminating hypotheses to include hypotheses of the form r=0.

Abstract. We consider the problem of how agents might try to guess values of a function based only on knowledge of the function on a subset of the domain, without any assumptions about the function being analytic or even continuous. At the level of a single agent, this is a hopeless problem. When one considers a collection of agents, however, it is often possible, using the Axiom of Choice, for the agents to guess in such a way that almost all of them are correct.

As an application, we can define a strategy which, given an arbitrary function f from the reals into some set, will for all but countably many x correctly guess the value of f on an interval [x, x'), x < x', given only the value of f on (-∞, x). If one interprets this function as the evolution of a system over time, this means that, in principle, one can almost always predict an interval of the system's future based only on its past, without any assumption of continuity.

Abstract. Our starting point is the following question: To what extent is a function's value at a point x of a topological space determined by its values in an arbitrarily small (deleted) neighborhood of x? For continuous functions, the answer is typically ``always'' and the method of prediction of f(x) is just the limit operator. We generalize this to the case of an arbitrary function mapping a topological space to an arbitrary set. We show that the best one can ever hope to do is to predict correctly except on a scattered set. Moreover, we give a predictor whose error set, in T₀ spaces, is always scattered.

Abstract. A common question in mathematics is whether a family of sets has nonempty intersection, and it is useful to have criteria that help answer these questions (for example, any chain of nonempty compact sets in a metric space has nonempty intersection). These questions can be recast in terms of approval voting, in which each voter has an approval set (the set of options that the voter approves of). Having an option that every voter approves of amounts to the approval sets having nonempty intersection. If this fails, one can still ask whether there is an option that a large proportion of the voters approve of.

Francis Su et al. have considered this problem in the case where the approval sets are intervals on a line [1], and showed that if out of every m voters, there are k who can agree on an option, then there is a single option that at least (k–1)/(m–1) of the population approves of. We consider the case where the approval sets are arcs on a circle, and answer a question by Su by showing an analogous result: if out of every m voters, there are k who can agree on an option, then there is a single option that more than (k–1)/m of the population approves of.

[1] D. Berg, S. Norine, F. Su, R. Thomas and P. Wollan. Voting in agreeable societies. American Mathematical Monthly, to appear.

Abstract. We consider a combinatorial problem related to guessing the values of a function at various points based on its values at certain other points, often presented by way of a hat-problem metaphor: there are a number of players who will have colored hats placed on their heads, and they wish to guess the colors of their own hats. A visibility relation specifies who can see which hats. This paper focuses on the existence of minimal predictors: strategies guaranteeing at least one player guesses correctly, regardless of how the hats are colored. We first present some general results, in particular showing that transitive visibility relations admit a minimal predictor exactly when they contain an infinite chain, regardless of the number of colors. In the more interesting nontransitive case, we focus on a particular nontransitive relation on ω that is elementary, yet reveals unexpected phenomena not seen in the transitive case. For this relation, minimal predictors always exist for two colors but never for ℵ₂ colors. For ℵ₀ colors, the existence of minimal predictors is independent of ZFC plus a fixed value of the continuum, and turns out to be closely related to certain cardinal invariants involving meager sets of reals.

Abstract. The transitive closure of a binary relation R can be thought of as the best possible approximation of R “from above” by a transitive relation. We consider the question of approximating a relation from below by transitive relations. Our main result is that every thick relation (a relation whose complement contains no infinite chain) on a countable set has a transitive thick subrelation. This allows for a solution to a problem arising from previous work by the author and Alan Taylor. We also exhibit a thick relation on an uncountable set with no transitive thick subrelation.