Research

I work on the foundations of theoretical computer science, in an area of logic known as finite model theory and the related field of descriptive complexity. I study the logical definability of complexity classes given by models of computation whose resources are bounded by mathematical (or physical) limits. My papers are often concerned with elementary (first-order) and inductive (fixed-point) definability on finite structures, in as much as these logics shed light on fundamental questions in the complexity of computation. More recently, I have been interested in logically characterizing the fundamental physical limitations of mechanical computing devices, and related general issues in the philosophical foundations of logic, information and computation. This work is highly abstract, but may be of substantial practical importance when it becomes impossible to make substantial technological improvements to computers.

manuscripts

• Logical normal forms for classes of bounded-degree finite graphs closed under substructure
  Shows how the application of purely classical model theoretic techniques (compactness and saturation arguments) can be used to prove a restricted version of Gaifman’s theorem.
• Quantifier elimination over strings
  Shows how to evaluate every formula over strings in constant-time with linear-time pre-processing.
• A normal form for first-order logic over doubly-linked data structures (Isaac Newton Institute Preprint Series, 2006)
  Summary: Shows that quantification of dependent variables can be eliminated over models with unary relations and bijective functions.
  Also see the recent talk at Cambridge University.
• Computing monadic fixed-points in linear-time on doubly-linked data structures (LCC 2005).
  Also see the talk.Inductive Classes of Finite Models
  Summary: We show that the property of an induction having a finite closure ordinal is itself inductively definable.
• Monadic Counting Does Not Suffice (1995)
  Abstract: This result separates monadic from dyadic counting over finite ordered structures. It is proved by showing that in the absence of any other relations, the former is a decidable theory, while the latter is not.
• Exponentiation is elementarily definable from addition and multiplication on finite structures (1995)
  Abstract: We explain how to define powering from plus and times in first-order logic on finite structures.

papers

• “Infinitary methods in finite model theory” (with Scott Weinstein and Henry Towsner) in Logic without Borders – Essays on Set Theory, Model Theory, Philosophical Logic and Philosophy of Mathematics, ed. Roman Kossak, De Gruyter 2015.
• “Real-Time Collaboration Tools for Digital Ink“, Journal of Computing Sciences in Colleges, Volume 25, Number 3, January 2010, pp. 24-31.
• “A normal form for first-order logic over doubly-linked data structures” IJFCS Vol. 19 No. 1 (Feb. 2008) pp. 205-217.
• A Term Logic for Physically Realizable Models of Information (near final draft). Appears as Chapter 8 in the book The Old New Logic: Essays on the Philosophy of Fred Sommers published by MIT press (2005). ACM Computing Review
  Summary: A paper in two parts.  The first part establishes a mathematical model of information based on uniform arrangements of matter in space.  These so-called singulary structures correspond to material representations of symbolic patterns, determined by the physical requirements of storing arbitrarily large amounts of data in a memory of unbounded size.  The second part introduces a functionally based term logic using numerical threshold quantifiers without variables.  Our main result shows that this classically motivated singulary logic has the same expressive power as ordinary first-order logic within this context. It can be seen as contributing to the logical foundations of information.
• “The Role of Decidability in First Order Separations over Classes of Finite Structures” in the Proceedings of the 15th Annual IEEE Symposium ” (co-written with Scott Weinstein), on Logic in Computer Science (2000), pp. 45-50.
• “Elementary Properties of the Finite Ranks” (co-written with Anuj Dawar, Kees Doets, & Scott Weinstein), Mathematical Logic Quarterly, Vol. 44, pp. 349-353 (1998).
• “A Constant-Space Sequential Model of Computation for First-Order Logic“, Information and Computation Vol. 143, pp. 231-250 (1998). [Summary]”
• Generalized Implicit Definitions on Finite Structures” (co-written with Stéphane Grumbach & Zoé Lacroix), in Kleine-Büning, H. (ed.), Computer Science Logic ’95, Springer-Verlag, Lecture Notes in Computer Science Vol. 1092, 1996, pp. 252-265.
• “First Order Logic, Fixed Point Logic and Linear Order” (co-written with Anuj Dawar & Scott Weinstein), in Kleine-Büning, H. (ed.), Computer Science Logic ’95, Springer-Verlag, Lecture Notes in Computer Science Vol. 1092, 1996, pp. 161-177.
• “A Constant-Space Sequential Model of Computation for First-Order Logic” Logic and Computational Complexity, Lecture notes in Computer Science no. 960, Daniel Leivant (ed.), Springer-Verlag 1995 pp. 447-462.
• “Infinitary Logic and Inductive Definability over Finite Structures” (co-written with Anuj Dawar & Scott Weinstein), Information and Computation, Vol. 119, No. 2, June 1995 pp. 160-175.
• “A Purely Logical Characterization of Circuit Uniformity” in Proceedings of the 7th Annual IEEE Conference on Structure in Complexity Theory, (1992), pp. 185-192.
• A Logspace Algorithm for Tree Canonization in Proceedings of the 24th Annual ACM Symposium on the Theory of Computing (1992), pp. 400-404.
• “The Invariant Problem for Binary String Structures and the Parallel Complexity Theory of Queries,” Journal of Computer and System Sciences, Vol. 44, no. 3, June 1992, pp. 385-410.
• “An Analysis of Fixed-Point Queries on Binary Trees,” Theoretical Computer Science, Vol. 85 (1991) 75-95.

dissertation

The Logical Complexity of Queries on Unordered GraphsUniversity of California, Los Angeles, 1987. Abstract

talks (selected)

• Logic and Models of Computation (lecture series given in the Third Indian School on Logic and its Applications on January 20-23, 2010 at University of Hyderabad, Gachibowli, India)
  1. History of logic
  2. Historical models of computation
  3. Computing without machines
  4. Logical definability over finite models
  5. First-order logic over doubly-linked data structures
• “Real-Time Collaboration Tools for Digital Ink” (October 30, 2009 at Villanova University in the 25th Annual Consortium for Computing Sciences in Colleges Eastern Conference).
• Computation: A Mathematical or Physical Notion? (November 5, 2007 at Villanova University) Abstract: Models of computation such as the Turing machine are based on the idealized psychological characteristics of a human calculator — an autonomous machine that changes its “state of mind” in a stepwise fashion based on the recognition of symbolic cellular configurations. This leads to a mathematical model of effective computability, and its complexity is traditionally quantified by measuring the amount of time (steps) and space (cells) required in the computation. However, a concrete model of computation must use matter and energy, operating under natural constraints governed by the laws of physics. This leads to a new notion of feasibility based on physical resources, particularly when the laws of thermodynamics and gravitation are taken into account.
• A physical analysis of mechanical computability (May 25, 2006 at the Isaac Newton Institute for Mathematical Sciences). Abstract: Turing’s model of autonomous computation is based on the idealized psychological characteristics of a human calculator — its ability to change its “state of mind” in a stepwise fashion based on the recognition of symbolic configurations. This leads to a mathematical model of effective computability, with its well known capabilities and limitations. We extend this analysis to the idealized physiological characteristics of a machine computer — its ability to manipulate matter using energy. This leads to a new notion of feasibility based on physical resource bounds, in which mass and energy constraints further restrict the usual notions of space and time complexity.
• A normal form for singulary logic over physically realizable data models (February 28, 2006 at the Isaac Newton Institute for Mathematical Sciences in Cambridge, England as part of the Logic and Databases Workshop). [audio] Summary: Relying on the symmetry of labeled connections between elements of the structure, this result shows that elementary definability can be reduced to boolean combinations of numerical quantifiers applied to quantifier-free formulas.
• Computing monadic fixed-points in linear-time on doubly-linked data structures (June 24, 2005 at Seventh International workshop on Logic and Computational Complexity). Abstract: In general, the computational effort required solving a problem described by a first-order or fixed-point query (logical formula) requires time polynomial in the size of the database (finite structure). We show how a linear-time evaluation algorithm for first-order logic on bounded-degree data structures can be extended to monadic fixed-point formulas, pointing the way to a logical characterization of linear-time computability.Summary
• Revisiting finite-visit computations (June 21, 2004 at rump session of Conference on Computational Complexity) Summary: Incorporating matter and energy requirements into physically implemented machines sheds new light on feasible computability. Under certain circumstances, conventional mathematical models may not be asymptotically realizable due to the limited availability of resources required to store data and execute instructions.
• Linear-time algorithms for Monadic Logic (University of Pennsylvania’s Logic and Computation Seminar, February 2003) [a shorter version skipping slides 7, 9, 10, 11 was given at the rump session of LICS 2003]. Summary: Descriptive complexity studies the asymptotic computational effort required to evaluate logical queries on finite databases, with a focus on queries expressed by first-order or fixed-point formulas. In general, these queries require a polynomial amount of time with respect to the size of the structure. We illustrate the special case of how monadic first-order formulas can be evaluated in linear-time on ordinary data structures. We even extend this to monadic fixed-point formulas, leading to the possibility of providing a logical characterization of linear-time computability.
• Physically Scalable Computation – an axiomatic approach (June 19, 2001 at rump session of Conference on Computational Complexity) Summary: A consideration of the matter and energy requirements of physically implemented machines leads tentatively to a finer mathematical analysis of asymptotic space and time computability.
• Computer Science as a Liberal Art: the Convergence of Technology and Reason, (a Faculty Research talk presented at Haverford College on January 24, 2001). Summary: Aimed at a general non-mathematical audience, I hope to explain how logical reasoning can be used to understand the fundamental theoretical issues behind the future potentials and limits of computing technology. Included will be a discussion of how this study can be viewed as continuing in the historical tradition of the seven original liberal arts.The Role of Decidability in First Order Separations over Classes of Finite Structures, given at the Logic in Computer Science conference in Santa Barbara, California June 2000. Abstract
• Using non-standard techniques to analyze first-order definability over finite structures was an invited presentation at the NSF/DIMACS sponsoredWorkshop on Logic and Cognitive Science, given at the University of Pennsylvania’s Institute for Research in Cognitive Science, April 18th, 1999.Fixed-point versus first-order definability on structures with arithmetic, invited presentation at the DIMACS workshop on Descriptive Complexity and Finite Models, Princeton University, January 17, 1996.
• A Constant-Space Model of Computation for First-Order Queries (presented at the DIMACS Special Year on Logic and Algorithms Seminar, November 8, 1995 and also at the University of Pennsylvania in their Logic and Computation seminar on Monday, April 3, 1995). Abstract
• Computing Without Machines – a logical approach to the mathematics of computation, at the Haverford-Bryn Mawr mathematics colloquium on Friday, March 18, 1994.
• A Logspace Algorithm for Tree Canonization (presented at the 1992 ACM Symposium on the Theory of Computing).Fixed-point Logic and Cyclic Formulas — Finite Model Theory and its Connections with Computational Complexity (VILLANOVA UNIVERSITY Computer Science Colloquium October 10, 1991). Abstract
• The invariant problem for binary string structures and its connection with the parallel complexity of queries, (presented at the annual meeting of the Association for Symbolic Logic held in the University of California, Berkeley January 1990). Abstract