TY - JOUR

T1 - Final algebras, cosemicomputable algebras and degrees of unsolvability

AU - Moss, Lawrence S.

AU - Meseguer, José

AU - Goguen, Joseph A.

N1 - Funding Information:
This paper studies some computability notions for abstract data types, and in particular compares cosemicomputable many-sorted algebras with a notion of finality to model minimal-state realizations of abstract (software) machines. Given a finite many-sorted signature S and a set V of visible sorts, for every Z-algebra A with co-r.e. behavior and nontrivial, computable V-behavior, there is a finite signature extension P’ of P (without new sorts) and a finite set E of Z’-equations such that A is isomorphic to a reduct of the final (X’, E)-algebra relative to V. This uses a theorem due to Bergstra and Tucker [3]. If A is computable, then A is also isomorphic to the reduct of * The research reported here was supported in part by a gift from the System Foundation. ** This paper was written while this author was a post-doctoral of Language and Information. *** The research reported here was supported in part by Office of Naval Research Contracts C-0417. N0014-86-C-0450 and N00014-90-C-0086.

PY - 1992/6/29

Y1 - 1992/6/29

N2 - This paper studies some computability notions for abstract data types, and in particular compares cosemicomputable many-sorted algebras with a notion of finality to model minimal-state realizations of abstract (software) machines. Given a finite many-sorted signature Σ and a set of V of visible sorts, for every Σ-algebra A with co-r.e. behavior and nontrivial, computable V-behavior, there is a finite signature extension Σ' of Σ (without new sorts) and a finite set E of Σ'-equations such that A is isomorphic to a reduct of the final (Σ', E)-algebra relative to V. This uses a theorem due to Bergstra and Tucker [3]. If A is computable, then A is also isomorphic to the reduct of the initial (Σ′, E)-algebra. We also prove some results on congruences of finitely generated free algebras. We show that for every finite signature Σ, there are either countably many Σ-congruences on the free Σ-algebra or else there is a continuum of such congruences. There are several necessary and sufficient conditions which separate these two cases. We introduce the notion of the Turing degree of a minimal algebra. Using the results above, we prove that there is a fixed one-sorted signature such that for every r.e. degree d, there is a finite set E of Σ-equations such the initial (Σ, E)-algebra has degree d. There is a two-sorted signature Σ0 and a single visible sort such that for every r.e. degree d there is a finite set E of Σ-equations such that the initial (Σ, E, V)-algebra is computable and the final (Σ, E, V)-algebra is cosemicomputable and has degree d.

AB - This paper studies some computability notions for abstract data types, and in particular compares cosemicomputable many-sorted algebras with a notion of finality to model minimal-state realizations of abstract (software) machines. Given a finite many-sorted signature Σ and a set of V of visible sorts, for every Σ-algebra A with co-r.e. behavior and nontrivial, computable V-behavior, there is a finite signature extension Σ' of Σ (without new sorts) and a finite set E of Σ'-equations such that A is isomorphic to a reduct of the final (Σ', E)-algebra relative to V. This uses a theorem due to Bergstra and Tucker [3]. If A is computable, then A is also isomorphic to the reduct of the initial (Σ′, E)-algebra. We also prove some results on congruences of finitely generated free algebras. We show that for every finite signature Σ, there are either countably many Σ-congruences on the free Σ-algebra or else there is a continuum of such congruences. There are several necessary and sufficient conditions which separate these two cases. We introduce the notion of the Turing degree of a minimal algebra. Using the results above, we prove that there is a fixed one-sorted signature such that for every r.e. degree d, there is a finite set E of Σ-equations such the initial (Σ, E)-algebra has degree d. There is a two-sorted signature Σ0 and a single visible sort such that for every r.e. degree d there is a finite set E of Σ-equations such that the initial (Σ, E, V)-algebra is computable and the final (Σ, E, V)-algebra is cosemicomputable and has degree d.

UR - http://www.scopus.com/inward/record.url?scp=0026882144&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0026882144&partnerID=8YFLogxK

U2 - 10.1016/0304-3975(92)90305-Y

DO - 10.1016/0304-3975(92)90305-Y

M3 - Article

AN - SCOPUS:0026882144

VL - 100

SP - 267

EP - 302

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 2

ER -