Dynamically-Typed Computations for Order-Sorted Equational Presentations

Claus Hintermeier 1 Claude Kirchner Hélène Kirchner
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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 few restrictions on the allowed presentations. We adopt the G-algebra framework, where equational, membership and existence formulas can be expressed, and that provides a complete deduction calculus which incorporates the interaction between all these formulas. To practically deal with this calculus, we introduce an operational semantics for G-algebra using rewrite systems over so-called decorated terms, that have assertions concerning the sort membership of any subterm in its head node. Decorated rewrite rules perform equational replacement, decoration rewrite rules enrich the decorations and record sort information. Therefore we use the semantic sort principle, i.e. equal terms belong to equal sorts, rather than the syntactic sort principle that does not use the equational part of a presentation. In order to have a complete and decidable unification on decorated terms, we restrict to sort-inheriting theories. Then a completion procedure on decorated terms is designed to compute all interactions between equational and membership formulas. When the completion terminates, the resulting set of rewrite rules provides a way to decide equational theorems of the form $(t = t')$ and typing theorems of the form $(t : A)$. The sort inheritance property is undecidable in general but we propose a test to check it on a given presentation. The test provides information on how to extend the presentation in a model conservative way, in order to obtain sort-inheritance.
Type de document :
Article dans une revue
Journal of Symbolic Computation, Elsevier, 1998, 25 (4), pp.455-526
Liste complète des métadonnées

https://hal.inria.fr/inria-00098625
Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:04:02
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00098625, version 1

Collections

Citation

Claus Hintermeier, Claude Kirchner, Hélène Kirchner. Dynamically-Typed Computations for Order-Sorted Equational Presentations. Journal of Symbolic Computation, Elsevier, 1998, 25 (4), pp.455-526. 〈inria-00098625〉

Partager

Métriques

Consultations de la notice

193