@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}
}
