Elgot Algebras
Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot to base denotational semantics on iterative theories instead, i.e., theories in which abstract recursive specificati...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2006-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2235/pdf |
| Summary: | Denotational semantics can be based on algebras with additional structure
(order, metric, etc.) which makes it possible to interpret recursive
specifications. It was the idea of Elgot to base denotational semantics on
iterative theories instead, i.e., theories in which abstract recursive
specifications are required to have unique solutions. Later Bloom and Esik
studied iteration theories and iteration algebras in which a specified solution
has to obey certain axioms. We propose so-called Elgot algebras as a convenient
structure for semantics in the present paper. An Elgot algebra is an algebra
with a specified solution for every system of flat recursive equations. That
specification satisfies two simple and well motivated axioms: functoriality
(stating that solutions are stable under renaming of recursion variables) and
compositionality (stating how to perform simultaneous recursion). These two
axioms stem canonically from Elgot's iterative theories: We prove that the
category of Elgot algebras is the Eilenberg-Moore category of the monad given
by a free iterative theory. |
|---|---|
| ISSN: | 1860-5974 |