Symbolic evaluation with structural recursive symbolic constants

DOI10.1016/0167-6423(87)90031-1MaRDI QIDQ1101205zbMATH OpenOpenAlexFDO

Authors F. Giannotti, Attilio Matteucci, Dino Pedreschi, Franco Turini

Publication date 1987

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0167-6423(87)90031-1

zbMATH Keywords

Symbolic evaluationtransformation rules

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Symbolic evaluation is a technique used for many termination of associative commutative (AC in short) rewriting systems. This ordering is based on a transformation of the terms by a rewriting system with rules similar to distributivity. We show this is a reduction ordering which works in the AC case since it is AC-commuting, and which provides an automatizable termination tool, since it is stable by instantiation. Thereafter, we show cases where this ordering fails, and propose an extension of this method to other transformation rules such as endomorphism.

Recommendations

• Towards specifying symbolic computation
• Symbolic computation in automated program reasoning
• Symbolic computation via program transformation
• Compilation and evaluation of linear mutual recursions
• Synthesising programs with non-trivial constants
• Symbolic computing
• scientific article; zbMATH DE number 5572668
• Algebra and Coalgebra in Computer Science

Cited in

(3)

• Annotated bibliography on partial evaluation and mixed computation
• scientific article; zbMATH DE number 2010094 (Why is no real title available?)
• Fixing code that explodes under symbolic evaluation

This page was built for publication: Symbolic evaluation with structural recursive symbolic constants

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