- Authors:
- Gerard Huet,
- Derek C. Oppen
Equations occur frequently in mathematics, logic and computer science. In this paper, we survey the main results concerning equations, and the methods available for reasoning about them and computing with them. The survey is self-contained and unified, using traditional abstract algebra. Reasoning about equations may involve deciding if an equation follows from a given set of equations (axioms), or if an equation is true in a given theory. When used in this manner, equations state properties that hold between objects. Equations may also be used as definitions; this use is well known in computer science: programs written in applicative languages, abstract interpreter definitions, and algebraic data type definitions are clearly of this nature. When these equations are regarded as oriented "rewrite rules," we may actually use them to compute. In addition to covering these topics, we discuss the problem of "solving" equations (the "unification" problem), the problem of proving termination of sets of rewrite rules, and the decidability and complexity of word problems and of combinations of equational theories. We restrict ourselves to first-order equations, and do not treat equations which define non-terminating computations or recent work on rewrite rules applied to equational congruence classes.
Cited By
Groce A, Holmes J and Kellar K One test to rule them all Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, (1-11)- Aoto T and Stratulat S Decision Procedures for Proving Inductive Theorems without Induction Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, (237-248)
- Boady M, Grinfeld P and Johnson J A term rewriting system for the calculus of moving surfaces Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, (69-76)
- Verma R (2019). Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems, Fundamenta Informaticae, 92:1-2, (145-168), Online publication date: 1-Jun-2009.
- Roy P, Bouchard B, Bouzouane A and Giroux S (2018). A hybrid plan recognition model for Alzheimer's patients: Interleaved-erroneous dilemma, Web Intelligence and Agent Systems, 7:4, (375-397), Online publication date: 1-Dec-2009.
- Verma R (2019). Complexity of Normal Form Properties and Reductions for Term Rewriting Problems Complexity of Normal Form Properties and Reductions for Term Rewriting Problems, Fundamenta Informaticae, 92:1-2, (145-168), Online publication date: 1-Jan-2009.
- Pérez Velasco P and de Lara J (2019). Using Matrix Graph Grammars for the Analysis of Behavioural Specifications, Electronic Notes in Theoretical Computer Science (ENTCS), 206, (133-152), Online publication date: 1-Apr-2008.
- Bouchard B, Bouzouane A and Giroux S A smart home agent for plan recognition Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems, (320-322)
- Hutter D (1997). Coloring Terms to Control Equational Reasoning, Journal of Automated Reasoning, 18:3, (399-442), Online publication date: 1-Jun-1997.
- Rönn S (1996). Invariants and closures in the theory of rewrite systems, Formal Aspects of Computing, 8:4, (463-478), Online publication date: 1-Jul-1996.
- Nakagawa A and Futatsugi K Stepwise refinement process with modularity Proceedings of the 11th international conference on Software engineering, (166-177)
- Nakagawa A, Futatsugi K and Tomura S Algebraic specification of Macintosh's Quickdraw using OBJ2 Proceedings of the 10th international conference on Software engineering, (334-343)
- Giegerich R (1988). Composition and evaluation of attribute coupled grammars, Acta Informatica, 25:4, (355-423), Online publication date: 1-May-1988.
- Futatsugi K, Goguen J, Jouannaud J and Meseguer J Principles of OBJ2 Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, (52-66)
- Thiel J Stop losing sleep over incomplete data type specifications Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, (76-82)
- Givler J and Kieburtz R Schema recognition for program transformations Proceedings of the 1984 ACM Symposium on LISP and functional programming, (74-84)
- Futatsugi K and Okada K A hierarchical structuring method for functional software systems Proceedings of the 6th international conference on Software engineering, (393-402)
- Remy J and Veloso P (1981). An economical method for comparing data type specifications, ACM SIGPLAN Notices, 16:5, (39-42), Online publication date: 1-May-1981.
Recommendations
From rewrite rules to bisimulation congruences
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a ...
On accurate product integration rules for linear fractional differential equations
This paper addresses the numerical solution of linear fractional differential equations with a forcing term. Competitive and highly accurate Product Integration rules are derived by starting from an equivalent formulation in terms of a Volterra integral ...
A numerical method based on quadrature rules for ψ-fractional differential equations
AbstractThis paper presents a numerical method for the solution of a class of ψ-fractional differential equations involving Caputo derivative with respect to a function. Initial value problem for the certain ψ-fractional differential equation ...