Abstract
The present paper shows how the idea of equality saturation can be used to build an inductive prover for a non-total first-order lazy functional language. We adapt equality saturation approach to a functional language by using transformations borrowed from supercompilation. A special transformation called merging by bisimilarity is used to perform proof by induction of equivalence between nodes of the E-graph. Equalities proved this way are just added to the E-graph. We also experimentally compare our prover with HOSC and HipSpec.
Cite
CITATION STYLE
Grechanik, S. (2015). Inductive prover based on equality saturation for a lazy functional language. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8974, pp. 127–141). Springer Verlag. https://doi.org/10.1007/978-3-662-46823-4_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
