Partial evaluation of order-sorted equational programs modulo axioms

María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Partial evaluation (PE) is a powerful and general program optimization technique with many successful applications. However, it has never been investigated in the context of expressive rule-based languages like Maude, CafeOBJ, OBJ, ASF+SDF, and ELAN, which support: rich type structures with sorts, subsorts and overloading; and equational rewriting modulo axioms such as commutativity, associativity– commutativity, and associativity–commutativity–identity. In this paper, we illustrate the key concepts by showing how they apply to partial evaluation of expressive rule-based programs written in Maude. Our partial evaluation scheme is based on an automatic unfolding algorithm that computes term variants and relies on equational least general generalization for ensuring global termination. We demonstrate the use of the resulting partial evaluator for program optimization on several examples where it shows significant speed-ups.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Revised Selected Papers
EditorsManuel V. Hermenegildo, Pedro Lopez-Garcia
PublisherSpringer-Verlag
Pages3-20
Number of pages18
ISBN (Print)9783319631387
DOIs
StatePublished - Jan 1 2017
Event26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016 - Edinburgh, United Kingdom
Duration: Sep 6 2016Sep 8 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10184 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016
CountryUnited Kingdom
CityEdinburgh
Period9/6/169/8/16

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Alpuente, M., Cuenca-Ortega, A., Escobar, S., & Meseguer, J. (2017). Partial evaluation of order-sorted equational programs modulo axioms. In M. V. Hermenegildo, & P. Lopez-Garcia (Eds.), Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Revised Selected Papers (pp. 3-20). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10184 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-63139-4_1