Algebra Seminar talk
2016-05-19
Zoltan Esik (University of Szeged)
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.
(Location: This talk will take place on Thursday May 19 at 11:00 s.t., in the "Besprechungsraum (green area)" on the 5th floor of the Freihaus building, Wiedner Haupstraße 8-10.)