@article {150, title = {A Condensed Goal-Independent Fixpoint Semantics Modeling the Small-Step Behavior of Rewriting}, year = {2013}, month = {02/2013}, type = {Technical Report}, abstract = {It is well known that it does not exist a condensed goal-independent bottom-up semantics for the full class of term rewriting systems. This kind of semantics is essential for the development of efficacious semantics- based program manipulation tools (e.g. automatic program analyzers and debuggers). The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many {\textquotedblleft}semantically useless{\textquotedblright} elements that can be retrieved from a smaller set of terms. In this paper we present a novel condensed narrowing-like semantics that contains the minimal information which is needed to describe compo- sitionally all possible rewritings. We provide its goal-dependent top-down definition and, more importantly, an equivalent goal-independent bottom- up fixpoint characterization. We prove soundness and completeness w.r.t. the small-step behavior of rewriting for the full class of term rewriting systems. This semantics constitutes the first step for the development of a condensed goal-independent bottom-up fixpoint semantics fully abstract w.r.t. the big-step behavior of rewriting (an ongoing work).}, keywords = {property-oriented specifications, semantics-based inference methods, TRS}, author = {Marco Comini and Luca Torella} } @proceedings {149, title = {TRSynth: a Tool for Automatic Inference of Term Equivalence in Left-linear Term Rewriting Systems}, journal = {ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM{\textquoteright}13)}, year = {2013}, abstract = {In this paper we propose a parametric technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of most general equations relating terms that rewrite, for all possible instantiations, to the same set of normal forms. The semantic-based inference method that we propose can cope with non-constructor-based TRSs, and considers non-ground terms. Particular emphasis is posed to avoid the generation of {\textquotedblleft}redundant{\textquotedblright} equations that can be a logical consequence of other ones. To experiment on the validity of our proposal we have considered an instance of the method employing a novel (condensed) semantics for left-linear TRSs and we have implemented a {\textquotedblleft}proof of concept{\textquotedblright} prototype in Haskell which is available online.}, author = {Marco Comini and Luca Torella} }