Partial evaluation of order-sorted equational programs modulo axioms

DOI10.1007/978-3-319-63139-4_1MaRDI QIDQ2409722zbMATH OpenOpenAlexFDO

Authors María Alpuente, A. Cuenca-Ortega, Santiago Escobar, José Meseguer

Publication date 13 October 2017

Full work available at URL https://arxiv.org/abs/1608.03424

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

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: 1) rich type structures with sorts, subsorts and overloading; 2) equational rewriting modulo axioms such as commutativity, associativity-commutativity, and associativity-commutativity-identity. In this extended abstract, 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.

Recommendations

• A partial evaluation framework for order-sorted equational programs modulo axioms
• Optimization of rewrite theories by equational partial evaluation
• Partial evaluation of multi-paradigm declarative languages: Foundations, control, algorithms and efficiency
• scientific article; zbMATH DE number 1950450
• scientific article; zbMATH DE number 1692905

Cited in

(7)

• Efficient safety enforcement for Maude programs via program specialization in the \textsf{ÁTAME} system
• Programming and symbolic computation in Maude
• A partial evaluation framework for order-sorted equational programs modulo axioms
• Optimization of rewrite theories by equational partial evaluation
• Safety enforcement via programmable strategies in Maude
• E-unification based on generalized embedding
• Symbolic Specialization of Rewriting Logic Theories with Presto

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Partial evaluation of order-sorted equational programs modulo axioms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2409722)