A modular equational generalization algorithm

María Alpuente, Santiago Escobar, José Meseguer, Pedro Ojeda

Research output: Contribution to journalConference articlepeer-review

Abstract

This paper presents a modular equational generalization algorithm, where function symbols can have any combination of associativity, commutativity, and identity axioms (including the empty set). This is suitable for dealing with functions that obey algebraic laws, and are typically mechanized by means of equational atributes in rule-based languages such as ASF+SDF, Elan, OBJ, Cafe-OBJ, and Maude. The algorithm computes a complete set of least general generalizations modulo the given equational axioms, and is specified by a set of inference rules that we prove correct. This work provides a missing connection between least general generalization and computing modulo equational theories, and opens up new applications of generalization to rule-based languages, theorem provers and program manipulation tools such as partial evaluators, test case generators, and machine learning techniques, where function symbols obey algebraic axioms. A Web tool which implements the algorithm has been developed which is publicly available.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'A modular equational generalization algorithm'. Together they form a unique fingerprint.

Cite this