Equational presentations with ordered sorts encompass partially defined functions and subtyping information in an algebraic framework. In this work we address the problem of computing in order-sorted algebras, with very few restrictions on the allowed presentations. We adopt an algebraic framework where equational, membership and existence formulas can be expressed. A complete deduction calculus is provided to incorporate the interaction between all these formulas. The notion of decorated terms is proposed to memorize local sort information, dynamically changed by a rewriting process. A completion procedure for equational presentations with ordered sorts computes a set of rewrite rules with which not only equational theorems of the form (t=t′), but also typing theorems of the form (t:A), can be proven.
CITATION STYLE
Hintermeier, C., Kirchner, C., & Kirchner, H. (1994). Dynamically-typed computations for order-sorted equational presentations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 820 LNCS, pp. 450–461). Springer Verlag. https://doi.org/10.1007/3-540-58201-0_89
Mendeley helps you to discover research relevant for your work.