ICE-TCS seminar: Zoltan Esik (University of Szeged, Hungary)
Date/Time: Tuesday, 24 May 2016, 13:00-14:00
Location: M1.02 - Reykjavík University
Speaker: Zoltan Esik (University of Szeged, Hungary)
Title: Equational Logic of Fixed Point Operations
Abstract: Fixed point operations play a fundamental role in theoretical computer science due to the fact that the semantics of recursion is usually described by fixed points of functions, functionals, functors or other constructors. There has been a tremendous amount of work on the existence, construction, algorithmic aspects, and logic of fixed point operations. This talk focuses on the equational logic of fixed point operations.
It has been shown over the past three decades that the equational properties of most fixed point operations used in computer science are precisely described by the axioms of iteration theories (or iteration categories) introduced by Bloom, Elgot and Wright and independently by Esik in 1980. A prototypical example of an iteration category is the category of complete lattices and monotonic functions equipped with the (parametrized) least fixed point operation.
We will provide (necessarily infinite) equational bases of iteration categories and describe finitely based
quasi-equational theories which are sound and complete for the equational theory of iteration categories. We will also present decidability and complexity results.
This talk is part of the ICE-TCS Theory Week, which will be concluded by the annual ICE-TCS Theory Day on Friday, 27 May.