A partial evaluation framework for order-sorted equational programs modulo axioms

M. Alpuente, A. Cuenca-Ortega, S. Escobar, J. Meseguer

Research output: Contribution to journalArticle

Abstract

Partial evaluation is a powerful and general program optimization technique with many successful applications. Existing PE schemes do not apply to expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: 1) rich type structures with sorts, subsorts, and overloading; and 2) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity. In this paper, we develop the new foundations needed and illustrate the key concepts by showing how they apply to partial evaluation of expressive programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on high-performance order-sorted equational least general generalization and order-sorted equational homeomorphic embedding algorithms for ensuring termination. We show that our partial evaluation technique is sound and complete for convergent rewrite theories that may contain various combinations of associativity, commutativity, and/or identity axioms for different binary operators. We demonstrate the effectiveness of Maude's automatic partial evaluator, Victoria, on several examples where it shows significant speed-ups.

Original languageEnglish (US)
Article number100501
JournalJournal of Logical and Algebraic Methods in Programming
Volume110
DOIs
StatePublished - Jan 2020

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'A partial evaluation framework for order-sorted equational programs modulo axioms'. Together they form a unique fingerprint.

  • Cite this