Initiality, induction, and computability.

*(English)*Zbl 0571.68004
Algebraic methods in semantics, Semin. Fontainebleau/France 1982, 459-541 (1985).

[For the entire collection see Zbl 0568.00021.]

This paper surveys, unifies, and extends a number of results on induction and computability in the context of an algebraic approach to the semantics of programming. The close relationship between computability, induction, and initiality is emphasized.

Highlights of this paper include: a software engineering motivation for the initial algebra approach to data abstraction; a review of many-sorted general algebra, including rules for equational deduction that are sound and complete; simple ’inductive’ characterizations of initiality (including generalized Peano axioms); constructions for both initial and final (i.e., minimal) algebra realizations of abstract software modules; and a detailed introduction to computable algebras and their relationship to initiality; finality, and rewrite rules, showing in particular how Gödel numberings arise from initiality, and how equationally defined equality relates to both theorem proving by ’inductionless induction’ and computability. The latter permits us to give a purely algebraic characterization of computable algebras: an algebra is computable iff it is a reduct of an initial model of a finite equational equality presentation.

This paper surveys, unifies, and extends a number of results on induction and computability in the context of an algebraic approach to the semantics of programming. The close relationship between computability, induction, and initiality is emphasized.

Highlights of this paper include: a software engineering motivation for the initial algebra approach to data abstraction; a review of many-sorted general algebra, including rules for equational deduction that are sound and complete; simple ’inductive’ characterizations of initiality (including generalized Peano axioms); constructions for both initial and final (i.e., minimal) algebra realizations of abstract software modules; and a detailed introduction to computable algebras and their relationship to initiality; finality, and rewrite rules, showing in particular how Gödel numberings arise from initiality, and how equationally defined equality relates to both theorem proving by ’inductionless induction’ and computability. The latter permits us to give a purely algebraic characterization of computable algebras: an algebra is computable iff it is a reduct of an initial model of a finite equational equality presentation.

##### MSC:

68N01 | General topics in the theory of software |

68P05 | Data structures |

68Q60 | Specification and verification (program logics, model checking, etc.) |