SGER: Axiomatizing Fixed Points

Stevens Institute Of Technology, Hoboken NJ

Investigators

Abstract

Stephen L. Bloom "Axiomatizing Fixed Points Stevens Inst. of Technology The purpose of the proposed work is to obtain complete, but simple, descriptions of the properties of the "fixed point" or "iteration" operation in computation. Simpler axioms may lead to concrete discreptions of free structures and we intend to use the axioms and/or these concrete descriptions to find and improve decision algorithms. Previous work by Bloom, Esik and others has resulted in a complete description of the equational laws satisfied by the iteration operation. This description takes the form of the axioms for Iteration Theories, which capture important features of many classes of structures of interest in the theory of computation. The original axiomatization of iteration theories contained a complicated equational scheme. Recently, this scheme has been replaced by the "group identities". Nevertheless, further simplifications seem to be possible. Another goal is to find relative finite axiomatizations of iteration theories enriched by additional operations and/or relations. If successful, there are major beneficial corollaries. For example, a relatively simple set of axioms for the concurrent behavior of finite state processes (both for bisimilarity equivalence and for trace equivalence), for Kleene relation algebras with and without conversion, for the behavioral equivalence of recursive program schemes or recursive data type definitions and others. Lastly, some previous work of the investigators and others has indicated that the laws of iteration theories hold in the extremely general setting of 2-categories, and we intend to investigate this phenomenon in detail.