Monday, September 17, 2007
4:00 PM
5130 Upson Hall
  Theory Seminar
Fall 2007
CS 789

Dexter Kozen
Cornell University


Indefinite Summation and the Kronecker Delta


The indefinite summation operator is like a discrete version of an indefinite integral.  Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions defined on graphs, such as the Tutte, chromatic, flow, and reliability polynomials.  These objects give a lot of interesting information about the graph, such as coloring information, but are intractable to compute in general.  They can be produced in polynomial time for bounded treewidth graphs, but the traditional combinatorial algorithms are still very inefficient, and we were led to investigate symbolic algorithms.  To do this, we needed to develop the algebraic properties of the indefinite summation operator and the generalized Kronecker delta from an axiomatic viewpoint.  Our main result is a complete axiomatization of the equational theory of these constructs; that is, all equations that hold under the intended interpretations are derivable in the calculus.  The completeness proof uses some basic notions from algebraic geometry.