John V. Tucker

dblp:t/JohnVTucker · also John Vivian Tucker · DBLP profile ↗
← Back
55ranked-venue papers
10as first author
7since 2021 · last 2025
0000-0003-4689-8760ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 44 · 10 first-author · 3 since 2021Software engineering, systems software and programming languages · 4 · 2 since 2021Applied, interdisciplinary, general and emerging computing · 4 · 2 since 2021Systems, architecture and hardware · 1Databases, data management, data science and information retrieval · 1Graphics, computer vision, multimedia, augmented reality and games · 1
YearPublicationVenuePosition
2025 For rational numbers with Suppes-Ono division, equational validity is one-one equivalent with Diophantine unsolvability
abstract
Adding division to rings and fields leads to the question of how to deal with division by 0. From a plurality of options, we discuss in detail what we call Suppes-Ono division in which division by 0 produces 0. We explain the backstory of this semantic option and its associated notion of equality, and prove a result regarding the logical complexity of deciding equations over the rational numbers equipped with Suppes-Ono division. We prove that deciding the validity of the equations is computationally equivalent to the Diophantine Problem for the rational numbers, which is a longstanding open problem.
Jan A. Bergstra, John V. Tucker
Theor. Comput. Sci.2
2025 A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
abstract
We analyse abstract data types that model numerical structures with a concept of error. Specifically, we focus on arithmetic data types that contain an error value \(\bot\) whose main purpose is to always return a value for division. To rings and fields, we add a division operator \(x/y\) and study a class of algebras called common meadows wherein \(x/0=\bot\) . The set of equations true in all common meadows is named the equational theory of common meadows . We give a finite equational axiomatisation of the equational theory of common meadows and prove that it is complete and that the equational theory is decidable.
Jan A. Bergstra, John V. Tucker
ACM Trans. Comput. Log.2
2024 Eager Term Rewriting For The Fracterm Calculus Of Common Meadows
abstract
Abstract Eager equality is a novel semantics for equality in the presence of partial operations. We consider term rewriting for eager equality for arithmetic in which division is a partial operator. We use common meadows which are essentially fields that contain an absorptive element $\bot $. The idea is that term rewriting is supposed to be semantics preserving for non-$\bot $ terms only. We show soundness and adequacy results for eager term rewriting w.r.t. the class of all common meadows. However, we show that an eager term rewrite system which is complete for common meadows of rational numbers is not easy to obtain, if it exists at all.
Jan A. Bergstra, John V. Tucker
Comput. J.2
2023 On The Axioms Of Common Meadows: Fracterm Calculus, Flattening And Incompleteness
abstract
Abstract Common meadows are arithmetic structures with inverse or division, made total on $0$ by a flag $\bot $ for ease of calculation. We examine some axiomatizations of common meadows to clarify their relationship with commutative rings and serve different theoretical agendas. A common meadow fracterm calculus is a special form of the equational axiomatization of common meadows, originally based on the use of division on the rational numbers. We study axioms that allow the basic process of simplifying complex expressions involving division. A useful axiomatic extension of the common meadow fracterm calculus imposes the requirement that the characteristic of common meadows be zero (using a simple infinite scheme of closed equations). It is known that these axioms are complete for the full equational theory of common cancellation meadows of characteristic $0$. Here, we show that these axioms do not prove all conditional equations which hold in all common cancellation meadows of characteristic $0$.
Jan A. Bergstra, John V. Tucker
Comput. J.2
2023 Eager Equality for Rational Number Arithmetic
abstract
Eager equality for algebraic expressions over partial algebras distinguishes or separates terms only if both have defined values and they are different. We consider arithmetical algebras with division as a partial operator, called meadows, and focus on algebras of rational numbers. To study eager equality, we use common meadows, which are totalisations of partial meadows by means of absorptive elements. An axiomatisation of common meadows is the basis of an axiomatisation of eager equality as a predicate on a common meadow. Applied to the rational numbers, we prove completeness and decidability of the equational theory of eager equality. To situate eager equality theoretically, we consider two other partial equalities of increasing strictness: Kleene equality, which is equivalent to the native equality of common meadows, and one we call cautious equality. Our methods of analysis for eager equality are quite general, and so we apply them to these two other partial equalities; and, in addition to common meadows, we use three other kinds of algebra designed to totalise division. In summary, we are able to compare 13 forms of equality for the partial meadow of rational numbers. We focus on the decidability of the equational theories of these equalities. We show that for the four total algebras, eager and cautious equality are decidable. We also show that for others the Diophantine Problem over the rationals is one-one computably reducible to their equational theories. The Diophantine Problem for rationals is a longstanding open problem. Thus, eager equality has substantially less complex semantics.
Jan A. Bergstra, John V. Tucker
ACM Trans. Comput. Log.2
2022 A model of systems with modes and mode transitions
abstract
We propose a method of classifying the operation of a system into finitely many modes. Each mode has its own objectives for the system's behaviour and its own algorithms designed to accomplish its objectives. A central problem is deciding when to transition from one mode to some other mode, a decision that may be contested and involve partial or inconsistent information. We propose some general principles and model mathematically their conception of modes for a system. We derive a family of data types for analysing mode transitions; these are simplicial complexes, both abstract and concretely realised as geometric spaces in euclidean space Rn. In the simplicial complex, a mode is represented by a simplex and each state of a system can be evaluated by mapping it into one or more simplices. This evaluation measures the extent to which different modes are appropriate for the state and can decide on a transition. To illustrate the general model in some detail, we work though a case study of an autonomous racing car.
Edwin J. Beggs, John V. Tucker
J. Log. Algebraic Methods Program.2
2022 Partial arithmetical data types of rational numbers and their equational specification
abstract
Upon adding division to the operations of a field we obtain a meadow. It is conventional to view division in a field as a partial function, which complicates considerably its algebra and logic. But partiality is one out of a plurality of possible design decisions regarding division. Upon adding a partial division function ÷ to a field Q of rational numbers we obtain a partial meadow Q(÷) of rational numbers that qualifies as a data type. Partial data types bring problems for specifying and programming that have led to complicated algebraic and logical theories – unlike total data types. We discuss four different ways of providing an algebraic specification of this important arithmetical partial data type Q(÷) via the algebraic specification of a closely related total data type. We argue that the specification method that uses a common meadow of rational numbers as the total algebra is the most attractive and useful among these four options. We then analyse the problem of equality between expressions in partial data types by examining seven notions of equality that arise from our methods alone. Finally, based on the laws of common meadows, we present an equational calculus for working with fracterms that is of general interest outside programming theory.
Jan A. Bergstra, John V. Tucker
J. Log. Algebraic Methods Program.2
2017 Computations with oracles that measure vanishing quantities
abstract
We consider computation with real numbers that arise through a process of physical measurement. We have developed a theory in which physical experiments that measure quantities can be used as oracles to algorithms and we have begun to classify the computational power of various forms of experiment using non-uniform complexity classes. Earlier, in Beggs et al. (2014 Reviews of Symbolic Logic7(4) 618–646), we observed that measurement can be viewed as a process of comparing a rational number z – a test quantity – with a real number y – an unknown quantity; each oracle call performs such a comparison. Experiments can then be classified into three categories, that correspond with being able to return test results $$\begin{eqnarray*} z < y\text{ or }z > y\text{ or }\textit{timeout},\\ z < y\text{ or }\textit{timeout},\\ z \neq y\text{ or }\textit{timeout}. \end{eqnarray*} $$ These categories are called two-sided, threshold and vanishing experiments, respectively. The iterative process of comparing generates a real number y. The computational power of two-sided and threshold experiments were analysed in several papers, including Beggs et al. (2008 Proceedings of the Royal Society, Series A (Mathematical, Physical and Engineering Sciences)464 (2098) 2777–2801), Beggs et al. (2009 Proceedings of the Royal Society, Series A (Mathematical, Physical and Engineering Sciences)465 (2105) 1453–1465), Beggs et al. (2013a Unconventional Computation and Natural Computation (UCNC 2013), Springer-Verlag 6–18), Beggs et al. (2010b Mathematical Structures in Computer Science20 (06) 1019–1050) and Beggs et al. (2014 Reviews of Symbolic Logic, 7 (4):618-646). In this paper, we attack the subtle problem of measuring physical quantities that vanish in some experimental conditions (e.g., Brewster's angle in optics). We analyse in detail a simple generic vanishing experiment for measuring mass and develop general techniques based on parallel experiments, statistical analysis and timing notions that enable us to prove lower and upper bounds for its computational power in different variants. We end with a comparison of various results for all three forms of experiments and a suitable postulate for computation involving analogue inputs that breaks the Church–Turing barrier.
Edwin J. Beggs, José Félix Costa, Diogo Poças, John V. Tucker
Math. Struct. Comput. Sci.4
2013 Services2Cloud: A Framework for Revenue Analysis of Software-as-a-Service Provisioning
abstract
Software as a Service (SaaS) is an increasingly attractive option for delivering software functionality. Software vendors act as service providers provisioning the functionality directly via the Internet, and customers pay for access to the service on a flexible billing model such as subscription or pay-per-use. As a result, the generated revenue is difficult to analyse due to the highly dynamic nature of the customer's interaction with the service. We present the Services2Cloud framework to assist service providers in the analysis of their expected revenue based on customer subscription and service usage. Our approach is based on a formal specification of the service on offer and a concise expression of the service usage as probabilistic patterns which are interpreted as stochastic processes. Key features of our theoretical framework have been implemented within a web-based toolkit that aims to facilitate the revenue analysis process for service providers.
Kenneth Johnson, Yuanzhi Wang, Radu Calinescu, Ian Sommerville, Gordon D. Baxter, John V. Tucker
CloudCom (2)6
2013 The data type of spatial objects
abstract
Abstract A spatial object consists of data assigned to points in a space. Spatial objects, such as memory states and three dimensional graphical scenes, are diverse and ubiquitous in computing. We develop a general theory of spatial objects by modelling abstract data types of spatial objects as topological algebras of functions. One useful algebra is that of continuous functions, with operations derived from operations on space and data, and equipped with the compact-open topology. Terms are used as abstract syntax for defining spatial objects and conditional equational specifications are used for reasoning. We pose a completeness problem:Given a selection of operations on spatial objects, do the terms approximate all the spatial objects to arbitrary accuracy?We give some general methods for solving the problem and consider their application to spatial objects with real number attributes.
Kenneth Johnson, John V. Tucker
Formal Aspects Comput.2
2013 Oracles that measure thresholds: the Turing machine and the broken balance
abstract
What can algorithms compute with the help of information provided by an oracle that is a physical system? We have developed a theory that combines Turing machines with experiments that perform physical measurements in which queries are governed by subtle timing protocols and provide the equipment with numerical data with (i) infinite precision, (ii) finite but unbounded precision or (iii) finite but fixed precision. Here, we consider the measurement of physical quantities that are thresholds, whose values are obtained by a sequence of approximate measurements that converge either from above or from below. The thresholds may be authentic physical properties or artefacts of the methods and equipment that performs the measurement. Using a canonical example of a threshold oracle, the broken beam balance for measuring mass, we develop methods to cope with thresholds and classify the computational power in polynomial time of this physical oracle using non-uniform complexity classes. Surprisingly, new complexity classes arise illuminating the influence of the operation of the equipment. All classes break the Turing Barrier.
Edwin J. Beggs, José Félix Costa, Diogo Poças, John V. Tucker
J. Log. Comput.4
2012 The impact of models of a physical oracle on computational power
abstract
Using physical experiments as oracles for algorithms, we can characterise the computational power of classes of physical systems. Here we show that two different physical models of the apparatus for a single experiment can have different computational power. The experiment is thescatter machine experiment(SME), which was first presented in Beggs and Tucker (2007b). Our first physical model contained a wedge with a sharp vertex that made the experiment non-deterministic with constant runtime. We showed that Turing machines with polynomial time and an oracle based on a sharp wedge computed the non-uniform complexity classP/poly. Here we reconsider the experiment with a refined physical model where the sharp vertex of the wedge is replaced byanysuitable smooth curve with vertex at the same point. These smooth models of the experimental apparatus are deterministic. We show thatno matter what shape is chosen for the apparatus: (i) the time of detection of the scattered particles increases at least exponentially with the size of the query; and (ii) Turing machines with polynomial time and an oracle based on a smooth wedge compute the non-uniform complexity classP/log* ⫋P/poly. We discuss evidence that many experiments that measure quantities have exponential runtimes and a computational power ofP/log*.
Edwin J. Beggs, José Félix Costa, John V. Tucker
Math. Struct. Comput. Sci.3
2011 Continuity of operators on continuous and discrete time streams
John V. Tucker, Jeffery I. Zucker
Theor. Comput. Sci.1
2010 Limits to measurement in experiments governed by algorithms
abstract
We pose the following question: If a physical experiment were to be completely controlled by an algorithm, what effect would the algorithm have on the physical measurements made possible by the experiment? In a programme to study the nature of computation possible by physical systems, and by algorithms coupled with physical systems, we have begun to analyse: (i) the algorithmic nature of experimental procedures; and (ii) the idea of using a physical experiment as an oracle to Turing Machines. To answer the question, we will extend our theory of experimental oracles so that we can use Turing machines to model the experimental procedures that govern the conduct of physical experiments. First, we specify an experiment that measures mass via collisions in Newtonian dynamics and examine its properties in preparation for its use as an oracle. We begin the classification of the computational power of polynomial time Turing machines with this experimental oracle using non-uniform complexity classes. Second, we show that modelling an experimenter and experimental procedure algorithmically imposes a limit on what can be measured using equipment. Indeed, the theorems suggest a new form of uncertainty principle for our knowledge of physical quantities measured in simple physical experiments. We argue that the results established here are representative of a huge class of experiments.
Edwin J. Beggs, José Félix Costa, John V. Tucker
Math. Struct. Comput. Sci.3
2009 Meadows and the equational specification of division
Jan A. Bergstra, Yoram Hirshfeld, John V. Tucker
Theor. Comput. Sci.3
2008 Programming Experimental Procedures for Newtonian Kinematic Machines
Edwin J. Beggs, John V. Tucker
CiE2
2008 On the Complexity of Measurement in Classical Physics
Edwin J. Beggs, José Félix Costa, Bruno Loff, John V. Tucker
TAMC4
2008 Oracles and Advice as Measurements
Edwin J. Beggs, José Félix Costa, Bruno Loff, John V. Tucker
UC4
2008 Division Safe Calculation in Totalised Fields
abstract
A 0-totalised field is a field in which division is a total operation with 0−1=0. Equational reasoning in such fields is greatly simplified but in deriving a term one still wishes to know whether or not the calculation has invoked 0−1. If it has not then we call the derivation division safe. We propose three methods of guaranteeing division safe calculations in 0-totalised fields.
Jan A. Bergstra, John V. Tucker
Theory Comput. Syst.2
2007 The rational numbers as an abstract data type
abstract
We give an equational specification of the field operations on the rational numbers under initial algebra semantics using just total field operations and 12 equations. A consequence of this specification is that 0 −1 = 0, an interesting equation consistent with the ring axioms and many properties of division. The existence of an equational specification of the rationals without hidden functions was an open question. We also give an axiomatic examination of the divisibility operator, from which some interesting new axioms emerge along with equational specifications of algebras of rationals, including one with the modulus function. Finally, we state some open problems, including: Does there exist an equational specification of the field operations on the rationals without hidden functions that is a complete term rewriting system?
Jan A. Bergstra, John V. Tucker
J. ACM2
2007 Can Newtonian systems, bounded in space, time, mass and energy compute all functions?
Edwin J. Beggs, John V. Tucker
Theor. Comput. Sci.2
2007 Computability of analog networks
John V. Tucker, Jeffery I. Zucker
Theor. Comput. Sci.1
2005 A Network Model of Analogue Computation over Metric Algebras
John V. Tucker, Jeffery I. Zucker
CiE1
2004 Abstract versus concrete computation on metric partial algebras
abstract
In the theory of computation on topological algebras there is a considerable gap between so-called abstract and concrete models of computation. In concrete models, unlike abstract models, the computations depend on the representation of the algebra. First, we show that with abstract models, one needs algebras with partial operations, and computable functions that are both continuous and many-valued. This many-valuedness is needed even to compute single-valued functions, and so abstract models must be nondeterministic even to compute deterministic problems. As an abstract model, we choose the "while"-array programming language, extended with a nondeterministic "countable choice" assignment, called the WhileCC* model. Using this, we introduce the concept of approximable many-valued computation on metric algebras. For our concrete model, we choose metric algebras with effective representations. We prove:(1) for any metric algebra A with an effective representation α, WhileCC* approximability implies computability in α, and (2) also the converse, under certain reasonable conditions on A. From (1) and (2) we derive an equivalence theorem between abstract and concrete computation on metric partial algebras. We give examples of algebras where this equivalence holds.
John V. Tucker, Jeffery I. Zucker
ACM Trans. Comput. Log.1
2003 The algebraic structure of interfaces
D. Ll. L. Rees, Karen Stephenson, John V. Tucker
Sci. Comput. Program.3
2002 Domain representations of partial functions, with applications to spatial objects and constructive volume geometry
Jens Blanck, Viggo Stoltenberg-Hansen, John V. Tucker
Theor. Comput. Sci.3
2002 Abstract computability and algebraic specification
abstract
Abstract computable functions are defined by abstract finite deterministic algorithms on many-sorted algebras. We show that there exist finite universal algebraic specifications that specify uniquely (up to isomorphism) (i) all abstract computable functions on any many-sorted algebra; (ii) all functions effectively approximable by abstract computable functions on any metric algebra. We show that there exist universal algebraic specifications for all the classically computable functions on the set ℝ of real numbers. The algebraic specifications used are mainly bounded universal equations and conditional equations. We investigate the initial algebra semantics of these specifications, and derive situations where algebraic specifications precisely define the computable functions.
John V. Tucker, Jeffery I. Zucker
ACM Trans. Comput. Log.1
2000 Constructive Volume Geometry
abstract
We present an algebraic framework, called Constructive Volume Geometryn (CVG), for modelling complex spatial objects using combinational operations. By utilising scalar fields as fundamental building blocks, CVG provides high‐level algebraic representations of objects that are defined mathematically or built upon sampled or simulated datasets. It models amorphous phenomena as well as solid objects, and describes the interior as well as the exterior of objects. We also describe a hierarchical representation scheme for CVG, and a direct rendering method with a new approach for consistent sampling. The work has demonstrated the feasibility of combining a variety of graphics data types in a coherent modelling scheme.
Min Chen 0001, John V. Tucker
Comput. Graph. Forum2
1999 Concrete Models of Computation for Topological Algebras
Viggo Stoltenberg-Hansen, John V. Tucker
Theor. Comput. Sci.2
1999 Computation by 'While' Programs on Topological Partial Algebras
John V. Tucker, Jeffery I. Zucker
Theor. Comput. Sci.1
1996 Algebraic Models of Microprocessors: Architecture and Organisation
Neal A. Harman, John V. Tucker
Acta Informatica2
1995 A Data Type Variety of Stack Algebras
Jan A. Bergstra, John V. Tucker
Ann. Pure Appl. Log.2
1995 Equational Specifications, Complete Term Rewriting Systems, and Computable and Semicomputable Algebras
abstract
We classify the computable and semicomputable algebras in terms of finite equational initial algebra specifications and their properties as term term rewriting systems, such as completeness.Further results on properties of these specifications, such as on their size and orthogonality, are provided which show that our main results are the best possible.
Jan A. Bergstra, John V. Tucker
J. ACM2
1992 Theory of Computation over Stream Algebras, and its Applications
John V. Tucker, Jeffery I. Zucker
MFCS1
1991 Algebraic and Fixed Point Equations over Inverse Limits of Algebras
Viggo Stoltenberg-Hansen, John V. Tucker
Theor. Comput. Sci.2
1990 Provable Computable Functions on Abstract Data Types
John V. Tucker, Stanley S. Wainer, Jeffery I. Zucker
ICALP1
1989 Horn Programs and Semicomputable Relations on Abstract Structures
John V. Tucker, Jeffery I. Zucker
ICALP1
1989 The concurrent assignment representation of synchronous systems
Andrew Richard Martin, John V. Tucker
Parallel Comput.2
1988 Complete Local Rings as Domains
abstract
Contents: Introduction. §1: Computable rings and modules. §2: Ideal membership relation. §3: Effective structured domains. §4: Completion of a local ring as a domain. §5: The recursive completion. Epilogue. References. Introduction. Completion is an important general mathematical device. Often, but not always, a completion takes the following form. Let A be a topological algebraic structure whose topology is derived from a metric. For A, a topological algebra  and an embedding i: A →  are constructed such that  is a complete metric space in which A is densely embedded by i. The long list of structures for which such completions exist begins with Cantor's construction of the real number field and includes objects like the p-adic integers, Baire space, and Boolean algebras. In Bourbaki [6] a careful and thorough account of completions for arbitrary topological groups and fields is given, for which it is important to note that the topological structures need not be metrizable, but must possess a uniformity. The effectiveness of the completion process of a computable structure A cannot be readily studied using the tools of computable algebra, simply because the resulting structure  is almost invariably uncountable. However, in particular cases, it has been possible to define and study the substructure Ak of computable elements of Â; this has been done for the structures mentioned above, starting with the field of recursive real numbers. In this paper we analyse the effectivity of the completion of a local ring R. We do this using structured Scott-Ershov domains. Our study may be considered as a prototype containing methods applicable to a broad class of completions, including all the examples mentioned above, except for the real number field, which needs a generalisation of the domain concept. A Scott-Ershov domain D formalises how a set Dt of possibly “infinite” elements, called total elements, is constructed from a set Dc of “finite” elements, called compact elements. This is achieved by means of an approximation ordering which determines a topology on D and, in particular, on Dt. Our methodology is to associate to a given topological algebra A a structured domain D(A) such that the total elements D(A)t form a topological algebra topologically isomorphic to A. In such circumstances A is said to be domain definable by D(A). The theory of computability for domains is now applied to study the effectivity of the topological algebra A.
Viggo Stoltenberg-Hansen, John V. Tucker
J. Symb. Log.2
1987 Algebraic Specifications of Computable and Semicomputable Data Types
Jan A. Bergstra, John V. Tucker
Theor. Comput. Sci.2
1985 Top-Down Design and the Algebra of Communicating Processes
Jan A. Bergstra, John V. Tucker
Sci. Comput. Program.2
1984 The Axiomatic Semantics of Programs Based on Hoare's Logic
Jan A. Bergstra, John V. Tucker
Acta Informatica2
1984 Hoare's Logic for Programming Languages with two Data Types
Jan A. Bergstra, John V. Tucker
Theor. Comput. Sci.2
1983 Initial and Final Algebra Semantics for Data Type Specifications: Two Characterization Theorems
abstract
We prove that those data types which may be defined by conditional equation specifications and final algebra semantics are exactly the cosemicomputable data types-those data types which are effectively computable, but whose inequality relations are recursively enumerable. And we characterize the computable data types as those data types which may be specified by conditional equation specifications using both initial algebra semantics and final algebra semantics. Numerical bounds for the number of auxiliary functions and conditional equations required are included in both theorems.
Jan A. Bergstra, John V. Tucker
SIAM J. Comput.2
1983 Hoare's Logic and Peano's Arithmetic
Jan A. Bergstra, John V. Tucker
Theor. Comput. Sci.2
1982 Complexity Theory and the Operational Structure of Algebraic Programming Systems
Peter R. J. Asveld, John V. Tucker
Acta Informatica2
1982 The Completeness of the Algebraic Specification Methods for Computable Data Types
Jan A. Bergstra, John V. Tucker
Inf. Control.2
1982 Two Theorems About the Completeness of Hoare's Logic
Jan A. Bergstra, John V. Tucker
Inf. Process. Lett.2
1982 Expressiveness and the Completeness of Hoare's Logic
Jan A. Bergstra, John V. Tucker
J. Comput. Syst. Sci.2
1982 Some Natural Structures which Fail to Possess a Sound and Decidable Hoare-Like Logic for their While-Programs
Jan A. Bergstra, John V. Tucker
Theor. Comput. Sci.2
1982 Floyds Principle, Correctness Theories and Program Equivalence
Jan A. Bergstra, Jerzy Tiuryn, John V. Tucker
Theor. Comput. Sci.3
1981 Algebraically Specified Programming Systems and Hoare's Logic
Jan A. Bergstra, John V. Tucker
ICALP2
1981 On the Power of Algebraic Specifications
Jan A. Bergstra, Manfred Broy, John V. Tucker, Martin Wirsing
MFCS3
1980 A Characterisation of Computable Data Types by Means of a Finite Equational Specification Method
Jan A. Bergstra, John V. Tucker
ICALP2
1980 Computability and the Algebra of Fields: Some Affine Constructions
abstract
A natural way of studying the computability of an algebraic structure or process is to apply some of the theory of the recursive functions to the algebra under consideration through the manufacture of appropriate coordinate systems from the natural numbers. An algebraic structureA= (A;σ1,…,σk) iscomputableif it possesses a recursive coordinate system in the following precise sense: associated toAthere is a pair (α, Ω) consisting of a recursive set of natural numbersΩand a surjectionα:Ω→Aso that (i) the relation defined onΩbyn≡αmiffα(n) =α(m) inAis recursive, and (ii) each of the operations ofAmay be effectively followed inΩ, that is, for each (say)r-ary operationσonAthere is anrargument recursive function onΩwhich commutes the diagram whereinαrisr-foldα× … ×α. This concept of a computable algebraic system is the independent technical idea of M.O.Rabin [18] and A.I.Mal'cev [14]. From these first papers one may learn of the strength and elegance of the general method of coordinatising; note-worthy for us is the fact that computability is a finiteness condition of algebra—an isomorphism invariant possessed of all finite algebraic systems—and that it serves to set upon an algebraic foundation the combinatorial idea that a system can be combinatorially presented and have effectively decidable term or word problem.
John V. Tucker
J. Symb. Log.1