Denotational semantics can be based on algebras with additional structure(order, metric, etc.) which makes it possible to interpret recursivespecifications. It was the idea of Elgot to base denotational semantics oniterative theories instead, i.e., theories in which abstract recursivespecifications are required to have unique solutions. Later Bloom and Esikstudied iteration theories and iteration algebras in which a specified solutionhas to obey certain axioms. We propose so-called Elgot algebras as a convenientstructure for semantics in the present paper. An Elgot algebra is an algebrawith a specified solution for every system of flat recursive equations. Thatspecification satisfies two simple and well motivated axioms: functoriality(stating that solutions are stable under renaming of recursion variables) andcompositionality (stating how to perform simultaneous recursion). These twoaxioms stem canonically from Elgot's iterative theories: We prove that thecategory of Elgot algebras is the Eilenberg-Moore category of the monad givenby a free iterative theory.
展开▼
