Do you want to publish a course? Click here

Guided Unfoldings for Finding Loops in Standard Term Rewriting

56   0   0.0 ( 0 )
 Added by Etienne Payet
 Publication date 2018
and research's language is English
 Authors Etienne Payet




Ask ChatGPT about the research

In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distinguished positions in the rewrite rules. This results in a depth-first computation of the unfoldings, whereas the original technique was breadth-first. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs).



rate research

Read More

We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non-functional rewrite relations. We illustrate the inversion by experiments with full and partial
We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non meaningful compositions of rewrites that otherwise would fail during rewriting at runtime. Furthermore, our type system enables reasoning about how rewriting transforms the shape of the computational program. We present a formalization of our language at its type system and demonstrate its practical use for expressing compiler optimization strategies. Our type system builds the foundation for many interesting future applications, including verifying the correctness of program transformations and synthesizing program transformations from specifications encoded as types.
A rigid loop is a for-loop with a counter not accessible to the loop body or any other part of a program. Special instructions for rigid loops are introduced on top of the syntax of the program algebra PGA. Two different semantic projections are provided and proven equivalent. One of these is taken to have definitional status on the basis of two criteria: `normative semantic adequacy and `indicative algorithmic adequacy.
The notion of compliance in Multiset Rewriting Models (MSR) has been introduced for untimed models and for models with discrete time. In this paper we revisit the notion of compliance and adapt it to fit with additional nondeterminism specific for dense time domains. Existing MSR with dense time are extended with critical configurations and non-critical traces, that is, traces involving no critical configurations. Complexity of related {em non-critical reachability problem} is investigated. Although this problem is undecidable in general, we prove that for balanced MSR with dense time the non-critical reachability problem is PSPACE-complete.
Monads can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of evaluating an expression partially: for example, 2+3 can be obtained as a partial evaluation of 2+2+1. This construction can be given for any monad, and it is linked to the famous bar construction, of which it gives an operational interpretation: the bar construction induces a simplicial set, and its 1-cells are partial evaluations. We study the properties of partial evaluations for general monads. We prove that whenever the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms. In terms of rewritings, partial evaluations give an abstract reduction system which is reflexive, confluent, and transitive whenever the monad is weakly cartesian. For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables. This manuscript is part of a work in progress on a general rewriting interpretation of the bar construction.
comments
Fetching comments Fetching comments
Sign in to be able to follow your search criteria
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا