Structural induction in institutions (Q719243)

It seems appropriate to begin this review by quoting the following illuminating sentences from the author's introduction: ``Since its introduction within computing science by \textit{R. M. Burstall} in [``Proving properties of programs by structural induction'', Comput. J. 12, 41--48 (1969; Zbl 0164.46202)] structural induction has become a major method for performing inductive proofs, which constitute one of the most important formal verification trends. Originally structural induction was confined to proving properties of abstract data types, specified within many-sorted algebra. But over the past decades due to the population explosion of underlying logics for specification formalisms, the meaning and scope of structural induction has been extended to logical systems that are increasingly sophisticated and different from many-sorted algebra. However these structural induction proof methodologies are often developed on a rather ad hoc basis without clear mathematical foundations, a situation that in our opinion ultimately undermines the credibility of the associated formal methods.'' In the article under review, which is a part of a series of earlier articles by the author devoted to the `institution-independent' program, Diaconescu develops a general logic-independent structural induction proof method at the level of the theory of institutions of Goguen-Burstall (that may be applied to various actual induction proof methods in various logical systems). The main features of his development are: (1) an axiomatic approach to substitution at the level of institutions, (2) the possibility of simultaneous induction on several variables, (3) a proof method applicable in principle to any set of axioms, and (4) an abstract generic treatment of constructors. More specifically, the author, in Section 2, after stating notation and conventions about category theory and institution theory, the author gives a sketch of five institutions (many-sorted algebra, preordered algebra, multiple-valued logic, many-sorted algebra with predefined types, and partial algebra (cf. the reviewer's remarks below on this last institution)) that are relevant for theoretical computer science, formal specification, and to test his theory. Afterwards, he defines the concept of (weak) amalgamation square, institution with (weak) model amalgamation (i.e., an institution such that each pushout square of signatures is a (weak) amalgamation square), and semi-exact institution (i.e., an institution with the model amalgamation property extended also to model homomorphisms). In Section 3, the author presents an axiomatization of the notion of substitution within the theory of institutions, which, as the author says: ``is meant to support our institution-independent study of structural induction.'' To this end, the author begins by recalling, from the standpoint of the theory of institutions, the concepts of: variable (for a signature \(\Sigma\) of an institution, a \(\Sigma\)-variable is an object of the comma category \(\Sigma\downarrow\mathbf{Sig}\)), universal quantification, and substitution (for a signature \(\Sigma\) of an institution, and \(\Sigma\)-variables \(\chi\) and \(\chi'\), a \(\Sigma\)-substitution from \(\chi\) to \(\chi'\) is a pair \(\theta = (\mathrm{Sen}(\theta),\mathrm{Mod}(\theta))\) with \(\mathrm{Sen}(\theta)\) a mapping from \(\mathrm{Sen}(\mathrm{cod}(\chi))\) to \(\mathrm{Sen}(\mathrm{cod}(\chi'))\) and \(\mathrm{Mod}(\theta)\) a functor from \(\mathbf{Mod}(\mathrm{cod}(\chi'))\) to \(\mathbf{Mod}(\mathrm{cod}(\chi))\) satisfying suitable conditions). Then he shows that, for every signature \(\Sigma\) of an institution, one obtains a category \(\mathbf{Sbt}(\Sigma)\), the category of \(\Sigma\)-substitutions, in which the objects are the \(\Sigma\)-variables and the morphisms the \(\Sigma\)-substitutions (cf. the reviewer's remarks below on this last matter). Afterwards, to obtain in the next section the main result of the article, the institution-independent structural induction theorem, he defines the concepts of: system of substitutions in a given institution (a family \(\mathcal{S} = (\mathcal{S}_{\Sigma})_{\Sigma\in \mathrm{Ob}(\mathbf{Sig})}\) such that, for every \(\Sigma\in \mathrm{Ob}(\mathbf{Sig})\), \(\mathcal{S}_{\Sigma}\) is a subcategory of \(\mathbf{Sbt}(\Sigma)\) satisfying convenient conditions), a depth measure for a system of substitutions in an institution (a family of mappings from the substitutions to the set \(\mathbb{N}\) of natural numbers satisfying suitable conditions), and, in an institution with a system of substitutions and a depth measure, the atomic substitutions (a family \(\mathrm{At} = (\mathrm{At}_{\Sigma})_{\Sigma\in \mathrm{Ob}(\mathbf{Sig})}\) such that, for every \(\Sigma\in \mathrm{Ob}(\mathbf{Sig})\), \(\mathrm{At}_{\Sigma}\subseteq \mathcal{S}_{\Sigma}\) satisfying appropriate conditions). In Section 4, the author states the main result of his article: the institution-independent structural induction theorem (for a semi-exact institution with pushouts of signatures and equipped with a system of substitutions \(\mathcal{S}\), a depth measure \(d\) for \(\mathcal{S}\), a system of atomic substitutions \(\mathrm{At}\) for \(\mathcal{S}\) and \(d\), and a suitable binary relation on each set \(\mathrm{At}(\chi,\chi')\)), which is Theorem 4.1. Next, the author shows that the structural induction theorem is applicable to the five aforementioned institutions. In Section 5, the author provides an institution-independent study of the relation \[ \text{O}_{\Gamma}\models (\forall X)\rho \text{ if } \Gamma\models \theta(\rho) \text{ for all `substitutions' } \theta: X\rightarrow \mathrm{T}_{\Sigma} \] where \(\Gamma\) is a specification, \(\text{O}_{\Gamma}\) denotes the initial model (if it exists) of \(\Gamma\), \(\rho\) denotes a sentence, and \(\mathrm{T}_{\Sigma}\) the set of terms for the underlying signature of \(\Gamma\). This represents, as the author says: ``the justification for using the structural induction method of Theorem 4.1 for proving inductive properties.'' For this, the author provides a treatment of the concept of constructor. Section 6 is devoted to illustrate the abstract developments with formal verification proof scores written in specific languages. The article offers a variety of interesting concepts and results. Moreover, the article under review deserves attention because it extends the scope of the old theory and puts it in the much broader context of the theory of institutions of Goguen-Burstall. Reviewer's remarks: The author of the article says, on p. 1199, the following: ``In order to avoid the existence of empty interpretations of the sorts, which may complicate unnecessarily our presentation, we assume that each signature has at least one \textit{constant} (i.e., function symbol with empty arity) for each sort.'' In this connection I think it is suitable to recall what \textit{J. Schmidt} says in [``Algebraic operations and algebraic independence in algebras with infinitary operations'', Math. Jap. 6, 77--112 (1962; Zbl 0119.25903)], talking about single-sorted algebras (and which is also applicable, with appropriate modifications, when talking about many-sorted algebras): ``Let us still note the discussion of the particular rôle of the algebras of very low cardinal number, i.e., of cardinals \(0\) or \(1\), to be found in this paper. Thus, the empty algebra (if it exists), and the one-element algebras of a certain similarity type are defined (somehow analogously to the definition of subalgebras etc.) as the unique algebraic structures in which obvious conditions hold. But the discussion of the algebras of very low cardinal number, especially of the empty algebra, is not a purely dogmatic affair as some authors and reviewers seem to assume. Thus, many theorems of General Algebra do not hold for these algebras of very low cardinal number, at least not for the empty algebra, a failure which remains unnoticed by some authors. Other authors try to escape the situation by not admitting the empty or one-element algebra; unfortunately, they sometimes forget their own special convention, because it appears inconvenient at other places, e.g., when speaking of subalgebras. Still other authors do not even admit the subalgebra generated by the empty set; the futility of doing so becomes almost evident by the remark that one can consider any arbitrary algebra \(A\) -- by a more or less unessential change of the algebraic structure -- as generated by the empty set. The last remark seems to make evident that -- notwithstanding all possible conventions concerning the special treatment of the empty and the one-element set according to convenience and individual taste -- there are mathematical facts connected with the low cardinal numbers which as inconvenient as the[y] may be in the very nature of things: one can not avoid them.'' The author, sometimes, uses the expression ``Peano algebras''. Certainly such an expression is so entrenched that it is probably vain to try to change it by the expression ``Dedekind-Peano algebras'', which, I believe, reflects the history more accurately. I think it would be interesting to consider in addition to the institution \(\mathbf{PA}\), of many-sorted partial algebras (and homomorphisms), the institution of many-sorted partial algebras in which the morphisms between many-sorted partial algebras are the \(p\)-morphisms defined by \textit{V. S. Poythress} in [``Partial morphisms on partial algebras'', Algebra Univers. 3, 182--202 (1973; Zbl 0274.08008)]. Finally, in connection with the concept of substitution, it seems to me appropriate to add that such a concept is functorial. Concretely, that, for every institution \(\mathbf{I}\), there exists a contravariant functor, \(\mathrm{Sbt}_{\mathbf{I}}\), which sends a signature \(\Sigma\) of \(\mathbf{I}\) to the category \(\mathbf{Sbt}_{\mathbf{I}}(\Sigma)\), and a morphism \(\alpha: \Sigma\rightarrow\Omega\) between signatures of \(\mathbf{I}\) to a functor \(\mathrm{Sbt}_{\mathbf{I}}(\alpha)\) from \(\mathbf{Sbt}_{\mathbf{I}}(\Omega)\) to \(\mathbf{Sbt}_{\mathbf{I}}(\Sigma)\).