Hidden Algebra Homepage
Contents
A Brief Overview of Hidden Algebra

Hidden algebra aims to give a semantics for software engineering, and in particular for concurrent distributed object systems, supporting correctness proofs that are as simple and mechanized as possible. This emphasis on effective proofs rather than semantic modelling is supported by taking a calculational approach based on equations, rather than one based on, for example, higher order logic, type theory, denotational semantics, or any particular kind of model or set theory, because equational proofs achieve maximal simplicity and mechanization, while still allowing adequate expressiveness. It is also convenient that the models of a hidden algebraic specification are precisely its possible implementations.

Hidden algebra effectively handles the most troubling features of large systems, including concurrency, distribution, nondeterminism, and local states, as well as the usual features of the object paradigm, including classes, subclasses (inheritance), attributes and methods, in addition to supporting logical variables (as in logic programming), abstract data types, generic modules and more generally, the very powerful module system of prameterized programming. Hidden algebra generalizes the process algebra and transition system approaches to include non-monadic operations, so that it can take advantage of equations involving methods and attributes parameterized by data; this extra power can also dramatically simplify proofs. Coinduction methods appear to be more effective for behavioral properties (including behavioral refinement) than any alternative of which we are aware, and moreover, they can be automated to a very significant degree.

The hidden algebra approach takes as basic the notion of observational abstraction, or more precisely, behavioral satisfaction: this means that hidden specifications characterize how objects (and systems) behave in response to a given set of experiments, rather than how they are implemented; this provides a version of what is called a behavioral type in the object oriented jargon, but which we prefer to call a hidden theory, behavioral theory, or hidden specification. A hidden correctness proof for a refinement (or implementation) shows that one hidden theory behaviorally satisfies another, in the sense that any model of the second theory yields a model of the first; however, the formal proof is algebraic, not model-based. Successive refinement of designs is a useful model of software development, which avoids the unproductive "semantic swamp" of verifying actual code.

The Kumo examples homepage is designed to serve as a basic tutorial for both hidden algebra and the Kumo system which implements it, but the following remarks may also be helpful. Sorts are used in two distinct ways in hidden algebra:

• some are used for data values (e.g., of attributes), as in the algebraic approach to data types; and
• others are used for states, as in the algebraic approach to abstract machines.
The latter give objects. These two uses for sorts are dual: induction is used to establish properties of data types; while coinduction is used to establish (behavioral) properties of objects with states. Similarly, initiality is important for data types, while finality is important for states. However, we do not insist that implementations of abstract machines (or objects) must be final; on the contrary, we accept any implementation that satisfies the given axioms. This is important because in general, the most efficient implementations are neither initial nor final, but somewhere between. Moreover, hidden algebra's generality is such that final models may not even exist (this is because we allow operations with multiple hidden arguments).

Because we use hidden sorts to specify classes of objects, order sorted algebra provides a very natural way to handle inheritance; it also allows specifying partial recursive functions, partially defined functions, subtypes of various kinds, error definition and recovery, coercions and multiple representations. The module system of parameterized programming gives us other forms of inheritance, plus all the power of higher order functional programming in a first order setting which makes both proofs and programming easier. The most important results in hidden algebra justify efficient proof techniques based on coinduction. We consider hidden algebra to be the natural next step in the evolution of algebraic specification.

Some relatively recent developments in coinduction are described in Behavioral Verification of Distributed Concurrent Systems with BOBJ, by Joseph Goguen and Kai Lin; there is also a postscript version; in particular, the BOBJ system c4rw algorithm for proving behavioral properties by a combination of behavioral rewriting with circular coinduction and case analysis is described; the main example is a correctness proof of the alternating bit protocol. A more detailed discussion of the algorithm may be found in Conditional Circular Coinductive Rewriting with Case Analysis, by Joseph Goguen, Kai Lin and Grigore Rosu, though most proofs are omitted there. (Detailed citations for these papers in given in the Brief Hidden Bibliography section below). The paper Specifying, Programming and Verifying with Equational Logic, to appear in Festschrift volume for Dov Gabbay, discusses mutual coinduction, and illustrates it with inductive proof schemes; two theoretical contributions are a new formalization of logical programming, and a new semantics for higher order modules. A postscript version is also available, as are versions in the much more voluminous format of the book, in pdf and postscript.

An interesting application to verifying the Kumo distributed proof protocol is given in A Protocol for Distributed Cooperative Work, by Joseph Goguen and Grigore Rosu, with a brief summary of the main definitions and results in an earlier framework. A relatively leisurely introduction to some main concepts is in Hiding More of Hidden Algebra by Joseph Goguen and Grigore Rosu.

A high level snapshot of the UCSD Tatami project as of late September 2000 may be found in Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin; a snapshot as of November 1999, with more emphasis on the web-based user interface, may be found in An Overview of the Tatami Project, by Joseph Goguen and Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi; see also the one page summary of progress on our NSF grant up to mid October 1999, Hidden Algebra and Concurrent Distributed Software, in Software Engineering Notes, volume 25, number 1, page 51, January 2000.

A web-based tutorial on hidden algebra (though written for an early version of hidden algebra) is available, with pages on over 20 different topics, including links to background material on many sorted algebra and first order logic, although the version of hidden algebra used there is now out of date.

A Behavior Discussion List has been formed to facilitate progress on behavioral aspects of computer science and mathematics, including, but not limited to, versions of hidden algebra and behavioral equational logic, observational logic, and coalgebra, as well as systems that support them, such as CafeOBJ and Kumo. There is also a Behavior Homepage, which lists all members of the Behavior Discussion List, with links to their homepages whenever we could find them.

Hidden algebra is also implemented in CafeOBJ, a new generation algebraic specification system developed in Japan under the direction of Prof. Kokichi Futatsugi at Japan Advanced Inst of Science and Technology (JAIST). CafeOBJ preserves the distinctive useful features of OBJ3 with a different syntax, and adds new features for hidden algebra, rewriting logic, and their combinations with order sorted algebra. A somewhat more general version of hidden algebra is implemented in the BOBJ system, supporting circular coinductive rewriting with case analysis, automatic cobasis generation, and concurrent connection, for behavioral operations with multiple hidden arguments. The Kumo system provides theorem proving capability for full first order hidden logic, and in addition generates websites that document proofs done using it.

Latest Hidden Results

Hidden algebra has developed greater generality and more effective proof techniques through a series of steps, which are summarized in the bullets below, and are described in detail in our publications.

• Behavioral and non-behavioral operations are distinguished; the former are called congruent.
• Behavioral operations may have more than one hidden argument.
• Cobases can be used in coinduction, dual to the notion of basis for induction; when well chosen, they can greatly simplify proofs.
• Automatic cobasis generation is provided (though users can also define their own), using congruence criteria that take account of the special role of the untupling operation in concurrent connection.
• Rules for equational deduction and coinduction have been developed for these generalizations.
• An institution has been developed for hidden algebra to captures all these generalizations; it differs from prior institutions in treating congruent operations as sentences rather than as part of the signature.
• Circular coinductive rewriting has significantly extended the power of coinductive proofs, by combining coinduction, hidden rewriting, and cobasis generation.
• A Case analysis capability has been added to the circular coinductive rewriting algorithm.
The bullets below concern the BOBJ implementation, which has all of the above, plus the following:
• Cobases are treated as first class citizens (i.e., they can be declared and named).
• Sort declarations, a feature of order sorted algebra that allows the equational definition of subsorts, are supported.
• Second order parameterized programming is implemented, including parameterized views, and passing parameterized modules as parameters.
The Kumo behavioral proof assistant and proof website generator is available over the web in browser mode; a number of examples plus some documentation can be found at the Kumo examples homepage; see the Online Interactive Examples section below for a list of all these examples. You can also get the (more or less) most recent version of BOBJ from the BOBJ ftp site.

A Brief Hidden Bibliography
• Behavioral Verification of Distributed Concurrent Systems with BOBJ, by Joseph Goguen and Kai Lin. Text of keynote lecture for Conference on Quality Software, Dallas TX, 5-6 November 2003. In Proceedings, Conference on Quality Software, IEEE Press 2003, pages 216-235. Some slides are also available, although they are much more technical than the talk that was actually given. The paper proves correctness of the alternating bit protocol making strong use of recent features of BOBJ, especially conditional circular coinductive rewriting with case analysis. An early version of this paper is A Hidden Proof of the Alternating Bit Protocol, by Kai Lin and Joseph Goguen. See also the brief early web note Correctness of the Alternating Bit Protocol, and proof sketch for the Petersen Critical Section Algorithm.

• Semiotic Morphisms, Representations, and Blending for User Interface Design, by Joseph Goguen. Keynote lecture, in Proceedings, AMAST Workshop on Algebraic Methods in Language Processing, AMAST Press, 2003, pages 1-15 (held Verona, Italy, 25 - 27 August 2003). This paper extends algebraic semiotics to handle interaction by using hidden algebra; some examples are given in detail. A pdf version of the paper, and the slides for the talk are also available (you may have to change the orientation to swap landscape).

• Conditional Circular Coinductive Rewriting with Case Analysis, by Joseph Goguen, Kai Lin and Grigore Rosu, in Recent Trends in Algebraic Development Techniques, Springer Lecture Notes in Computer Science, volume 2755, 2004, pages 216-232; proceedings of 16th Workshop on Algebraic Development Techniques, Frauenchiemsee, Germany, 24-27 September 2002. Slides for the lecture version are also available, Conditional Circular Coinductive Rewriting (Note: You may have to reorient to "seascape"), as is the two page abstract, Conditional Circular Coinductive Rewriting, by the same authors. This paper extends BOBJ's circular coinductive rewriting algorithm to conditional equations and "splits" for case analyses. Postscript version also available. Note: This version does not have proofs.

• A Hidden Herbrand Theorem: Combining the Object, Logic and Functional Paradigms, by Joseph Goguen, Grant Malcolm, and Tom Kemp, Journal of Logic and Algebraic Programming, Volume 51, 2002, pages 1-41. Shows how to combine the logic and object paradigms using hidden algebra with existential quantifiers. This is a journal version of a paper in Principles of Declarative Programming, edited by Catuscia Palamidessi, Hugh Glaser and Karl Meinke (Proceedings of PLIP/ALP'98 [Programming Languages, Implementations, Logics and Programs / Algebraic and Logic Programming], Pisa, Italy, 14-19 September 1998), Springer Lecture Notes in Computer Science, Volume 1490, pages 445-462. (The paper was completed in 2001, and uses an older version of hidden algebra.) Compressed postscript and postscript versions are also available.

• Web-based Support for Cooperative Software Engineering, by Joseph Goguen and Kai Lin. To in Annals of Software Engineering, volume 12, 2001, a special issue on multimedia software engineering, edited by Jeffrey Tsai. An pdf version is also available. This is an overview of the Tatami project, featuring version 4 of the Kumo proof assistant and website generator, and focusing on its design decisions, its use of multimedia web capabilities, and its integration of formal and informal methods for software development in a distributed cooperative environment. The paper is a revised and expanded version of the paper Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin, which appeared in Proceedings, International Symposium on Multimedia Software Engineering, edited by Jeffrey Tsai and Po-Jen Chuang, IEEE Press, pages 25-32; this meeting was held in Taipai, Taiwan, December 2000.

• Behavioral and Coinductive Rewriting, by Joseph Goguen, Kai Lin, and Grigore Rosu. Keynote address, in Proceedings, Rewriting Logic Workshop, 2000 (Kanazawa, Japan), edited by Kokichi Futatsugi, Japan Advanced Institute of Science and Technology, September 2000, pages 1-22. A somewhat informal summary, including simulating behavioral rewriting with standard rewriting, and circular coinductive rewriting; the latter is a surprisingly effective algorithm for proving behavioral equalities.

• Circular Coinductive Rewriting by Joseph Goguen, Grigore Rosu and Kai Lin, in Proceedings, Automated Software Engineering '00 (Grenoble France), September 2000, IEEE, pages 123-131. Using many examples, this paper introduces the BOBJ system for behavioral specification and computation, and its surprisingly powerful circular coinductive rewriting algorithm for proving behavioral equalitites, which combines behavioral rewriting with circular coinduction. There is also a compressed postscript version.

• Circular Coinduction by Grigore Rosu and Joseph Goguen, in Proceedings, International Joint Conference on Automated Deduction, Sienna, June 2001. This paper provides the full proof of correctness of circular coinduction, and draws some consequences, including various congruence criteria.

• Slides for a lecture Towards the Automation of Behavioral Reasoning, given by Joseph Goguen at a meeting of IFIP WG 1.3 (Foundations of System Specification), at Stanford University on 30 June 2000; based on joint work with Kai Lin and Girgore Rosu, the slides summarize recent work on hidden algebra, especially the paper Circular Coinductive Rewriting by Joseph Goguen, Kai Lin, and Girgore Rosu.

• An Overview of the Tatami Project, by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi, in Cafe: An Industrial-Strength Algebraic Formal Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000, pages 61-78. This paper is a high level snapshop of the UCSD Tatami project as of late November 1999.

• Hidden Algebra and Concurrent Distributed Software, in Software Engineering Notes, volume 25, number 1, page 51, January 2000. A one page summary of progress on our NSF grant up to mid October 1999.

• A Protocol for Distributed Cooperative Work, by Joseph Goguen and Grigore Rosu, in Proceedings, Workshop on Distributed Systems (Iasi, Romania), September 1999, and in Elsevier Electronic Notes in Computer Science, Volume 28, 1999, pages 1-22. Contains a concise summary of the previous version of hidden algebra, and applies it to the correctness of a novel internet broadcast protocol designed to support synchronous distributed cooperative proving. Final revision 27 July 1999.

• Hiding More of Hidden Algebra, by Joseph Goguen and Grigore Rosu , in FM`99 - Formal Methods, Proceedings of World Congress on Formal Methods (Toulouse, France, August 1999), Springer Lecture Notes in Computer Science, Volume 1709, pages 1704-1719. New results relating information hiding to hidden algebra, and some compelling examples of behavioral operations with multiple hidden arguments.

• Hidden Congruent Deduction, by Grigore Rosu and Joseph Goguen, in Automated Deduction in Classical and Non-Classical Logics, edited by Ricardo Caferra and Gernot Salzer, Lecture Notes in Artificial Intelligence, Volume 1761, pages 252-267, 2000. Preliminary version in Proceedings, First-Order Theorem Proving - FTP'98, edited by Ricardo Caferra and Gernot Salzer, Technische Universitat Wien, pages 213-223, 1998 (proceedings of a workshop held at Schloss Wilhelminenberg, Vienna, November 23-25, 1998). The complete proceedings are available on the web, and by ftp. This paper extended all the main notions and results of hidden algebra to operations that may have more than one hidden argument, and also introduced the notion of cobasis, gave criteria for operations to be congruent, and introduced more powerful rules of deduction.

• Hidden Algebra for Software Engineering, in Combinatorics, Computation and Logic, Proceedings, Conference on Discrete Mathematics and Theoretical Computer Science, (University of Auckland, New Zealand, 18-21 January 1999), edited by Cristian Calude and Michael Dinneen, Australian Computer Science Communications, Volume 21, Number 3, Springer, pages 35-59, 1999 (keynote address); a compressed postscript version is also available. A gentle introduction to hidden algebra, with simple examples, much motivation, and some history. Completed 8 November 1998.

• A Hidden Agenda, by Joseph Goguen and Grant Malcolm, Theoretical Computer Science, vol 245, no 1, pages 55-101, August 2000, special issue on Algebraic Engineering, edited by Chrystopher Nehaniv and Masami Ito; a compressed postscript version is also available. This is an early basic paper on hidden algebra, treating coinduction, nondeterminism, concurrency and more. An even earlier version is UCSD Technical Report CS97-538, April 1997, and an obsolete abstract is in Proceedings of Workshop on New Mathematics for Computer Science, in Conference on Intelligent Systems: A Semiotic Perspective (National Institute of Standards and Technology, Gaithersberg MD, 20-23 Oct 1996) pages 159-167. Last modified 29 January 1999.

• Hidden Coinduction, by Joseph Goguen and Grant Malcolm, in Mathematical Structures in Computer Science, 9, number 3, pages 287-319, June 1999; this is a sister paper to A Hidden Agenda.

• Hidden Algebraic Engineering, by Joseph Goguen, in Algebraic Engineering, edited by Chrystopher Nehaniv and Masami Ito, World Scientific, 1999, pages 17-36; also UCSD Technical Report CS97-569, December 1997, and preliminary version in Proceedings, Conference on Semigroups and Algebraic Engineering, edited by Chrystopher Nehaniv (Aizu-Wakamatsu, Japan, 24-26 Mar 1997). This is a gentle introduction to the original version of hidden algebra, with some examples and much motivation.

• Towards an Algebraic Semantics for the Object Paradigm, by Joseph Goguen and Rãzvan Diaconescu, in Recent Trends in Data Type Specification, Proceedings of the 9th Workshop on Abstract Data Types (Caldes de Malevella, Spain, 28 October 1992), edited by Hartmut Ehrig and Fernando Orejas, Springer, Lecture Notes in Computer Science, Volume 785, 1994, pages 1-29. Although this is an early paper on hidden algebra, it includes an approach to inheritance, and details of the categorical concurrent connection construction.
Background information on universal algebra and category theory can be obtained from the following:
• Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm (MIT Press, 1996). Contains entry level introductions to universal algebra and the OBJ3 language. The paper An Executable Course in the Algebraic Semantics of Imperative Programs discusses some pedagogical innovations of this book.

• Two chapters from Theorem proving and Algebra, by Joseph Goguen, to be published by MIT Press: Chapter 1, the Introduction and Chapter 8, First Order Logic, plus the References and the Table of Contents. Chapter 8 is an elegant algebraic exposition of first order logic, proof planning and induction; the treatment of induction is unusually general. This book provides a systematic exposition of universal algebra and its applications in computer science.

• Introducing OBJ, in Software Engineering with OBJ: algebraic specification in action, edited by Joseph Goguen and Grant Malcolm, Kluwer, 2000, pages 3-167. The OBJ3 user manual; complete explanation of the language with many examples. (Revised and extended in August 1999.)

• A Categorical Manifesto, in Mathematical Structures in Computer Science, Volume 1, Number 1, March 1991, pages 49-67. Intuitive motivation for all the basic concepts of category theory, with many computer science examples.

• What is Unification?, in Resolution of Equations in Algebraic Structures, Volume 1: Algebraic Techniques, edited by Maurice Nivat and Hassan Ait-Kaci (Academic Press, 1989) pages 217-261. An introductory exposition of some basic categorical concepts.

• Stretching First order Equational Logic: Proofs with Partiality, Subtypes and Retracts, in Proceedings, International Workshop on First Order Theorem proving (Schloss Hagenbert, Austria, 27-28 October 1997). Watch retracts at work and at play! See how cute and useful they can be!

Some Online Interactive Examples

The tatami project homepage gives a general introduction to the project, and includes links to the web-based interactive examples listed below. Although not all of these illustrate hidden algebra, it is advisable to visit them in the order given, since they were assembled as an integrated sequence for pedagogical purposes; these examples are linked to an online tutorial on hidden algebra (unfortunately an older version), which in turn is linked to background tutorials on first order logic and proof planning.

1. An inductive proof that 1+...+ n = n(n+1)/2. This gives you a chance to explore Kumo's navigation and display conventions on a simple example. (Click on the "question mark" icon for navigation instructions.)

2. A coinductive proof of a behavioral property of a simple flag object. This illustrates some basics of the hidden algebra approach on a very simple example; it includes an especially clear motivation for the necessity of behavioral properties.

3. Two proofwebs for some familiar inductive properties of lists. The first was generated by a duck score written at the beginning of this effort; it is striking that the lemmas needed to complete the proof can be deduced from the way that successive proof attempts fail. The second proofweb succeeds, and was generated by a duck score derived from the first just by reordering its goals so that the lemmas that were found necessary are proved first.

1. This early attempt at proving that the reverse of the reverse of a list is the original list, takes a direct approach, and its explanations emphasize the way that the two lemmas that are needed to complete the proof can be deduced from the output produced by examining unsuccessful proof attempts; one of these lemmas is the associativity of append.
2. Here are the complete proofs for all three inductive properties of lists, including the two lemmas that are needed to establish the main goal.

4. A coinductive proof of the behavioral correctness of the array-with-pointer implementation of stack. This behavioral refinement proof requires introducing a non-trivial lemma, which can also be inferred from a prior proof attempt that fails without it.

5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.

6. A simple inductive proof of a formula for the sum of the squares of the first n natural numbers. This example is deliberately very spare, and in particular has no explanations, in order to illustrate the default conventions that Kumo uses when a user supplies only the absolute minimum input.

7. A detailed proof that the square root of 2 is irrational, illustrating the first order capabilities of Kumo. Note that this uses and proves many auxiliary lemmas; see the directory listing. Note: No explanations have yet been provided.

8. A coinductive correctness proof for the tatami protocol, which maintains the consistency of distributed cooperative proofs that are built using the tatami system (this was done using an older version of Kumo).
All these were generated by Kumo, which has been implemented by Kai Lin; Netscape 3.0 or later and some knowledge of hidden algebra will be needed to read them. Eventually the Java source code should be available for downloading via the Kumo homepage. Kumo is both a proof assistant and a proof website generator, though users must supply the specifications, goals, and explanations (if any). Using Kumo guarantees that the proofs are completely formally correct. Several of these examples also have illustrative Java applets, and there is live proof execution via a BOBJ server. Initial work on Kumo was supported by the large international CafeOBJ Project (see the CafeOBJ Press Release).

Some Related Papers on Other Sites

Some Future Research

• See the Behavior Homepage for a list of all members of the Behavior Discussion List, with links to their homepages whenever we could find them.

• Website of Grigore Rosu, at University of Illinois, Urbana-Champaign.

• CafeOBJ is a new generation algebraic specification language being developed in Japan with support from IPA (Japan). CafeOBJ supports hidden algebra. The CafeOBJ project is lead by Prof Kokichi Futatsugi of JAIST (Japan). More information about CafeOBJ, including its "cafeteria" mailing list, is available at the UCSD mirror site of the CafeOBJ homepage at Japan Advanced Institute of Science and Technology (JAIST).

• Website of Grant Malcolm, at the University of Liverpool.

• Website of Razvan Diaconescu at Institute of Mathematics of the Romanian Academy; neat stuff on the constraint paradigm, behavioral rewriting logic, and more.

• Website on algebraic semantics at Oxford, including links for work of Grant Malcolm, Corina Cirstea, James Worrell, Simone Veglioni, Sula Ma, and Andrew Stevens.

• Website of Horst Reichel at Dresden; neat stuff on coalgebraic semantics for the object paradigm.

• Website of Peter Padawitz at Universitaet Dortmund, Germany; behavioral deduction and declarative programming in his "swinging types" framework.

• Website of Bart Jacobs at Nijmegen, the Netherlands (formerly CWI, Amsterdam); more neat stuff on coalgebraic semantics for the object paradigm, and also for hybrid systems.

• Website of Oscar Nierstrasz at Bern, Switzerland (formerly at Geneva); much interesting information and links on object oriented systems and software composition.