Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFormalizing the Confluence of Orthogonal Rewriting Systems
113
0
0.0
(
0
)
Added by
EPTCS
Publication date
2013
fields
Informatics Engineering
and research's language is
English
Authors
Ana Cristina Rocha Oliveira
Ask ChatGPT about the research
No Arabic abstract
Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the existence of different rules that specify the same function and that may apply simultaneously (non-ambiguity), and, on the other side, it eliminates the possibility of occurrence of repetitions of variables in the left-hand side of these rules (left linearity). In the theory of term rewriting systems (TRSs) determinism is captured by the well-known property of confluence, that basically states that whenever different computations or simplifications from a term are possible, the computed answers should coincide. Although the proofs are technically elaborated, confluence is well-known to be a consequence of orthogonality. Thus, orthogonality is an important mathematical discipline intrinsic to the specification of recursive functions that is naturally applied in functional programming and specification. Starting from a formalization of the theory of TRSs in the proof assistant PVS, this work describes how confluence of orthogonal TRSs has been formalized, based on axiomatizations of properties of rules, positions and substitutions involved in parallel steps of reduction, in this proof assistant. Proofs for some similar but restricted properties such as the property of confluence of non-ambiguous and (left and right) linear TRSs have been fully formalized.
rate research
Read More
Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical branching lemma that characterizes local confluence from confluence of the critical branchings. The analysis of local confluence of rewriting systems on algebraic structures, such as groups or linear algebras, is complicated because of the underlying algebraic axioms, and in some situations, local confluence properties require additional termination conditions. This article introduces the structure of algebraic polygraph modulo that formalizes the interaction between the rules of an algebraic rewriting system and the inherent algebraic axioms, and we show a critical branching lemma for algebraic polygraphs. We deduce from this result a critical branching lemma for rewriting systems on algebraic objects whose axioms are specified by convergent modulo rewriting systems. We illustrate our constructions for string, linear, and group rewriting systems.
We present some contributions to the theory of infinitary rewriting for weakly orthogonal term rewrite systems, in which critical pairs may occur provided they are trivial. We show that the infinitary unique normal form property fails by an example of a weakly orthogonal TRS with two collapsing rules. By translating this example, we show that this property also fails for the infinitary lambda-beta-eta-calculus. As positive results we obtain the following: Infinitary confluence, and hence the infinitary unique normal forms property, holds for weakly orthogonal TRSs that do not contain collapsing rules. To this end we refine the compression lemma. Furthermore, we establish the triangle and diamond properties for infinitary multi-steps (complete developments) in weakly orthogonal TRSs, by refining an earlier cluster-analysis for the finite case.
In this paper, we study how graph transformations based on sesqui-pushout rewriting can be reversed and how the composition of rewrites can be constructed. We illustrate how such reversibility and composition can be used to design an audit trail system for individual graphs and graph hierarchies. This provides us with a compact way to maintain the history of updates of an object, including its multip
Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (eg, winds). Moreover, goals are often specified using explicit time constraints which must be satisfied by the system emph{perpetually}. For example, drones carrying out the surveillance of some area must always have emph{recent pictures}, ie, at most $M$ time units old, of some strategic locations. This paper proposes a Multiset Rewriting language with explicit time for specifying and analysing TSDSes. We introduce two properties, emph{realizability} (some trace is good) and emph{survivability} (where, in addition, all admissible traces are good). A good trace is an infinite trace in which goals are perpetually satisfied. We propose a class of systems called emph{progressive timed systems} (PTS), where intuitively only a finite number of actions can be carried out in a bounded time period. We prove that for this class of systems both the realizability and the survivability problems are PSPACE-complete. Furthermore, if we impose a bound on time (as in bounded model-checking), we show that for PTS, realizability becomes NP-complete, while survivability is in the $Delta_2^p$ class of the polynomial hierarchy. Finally, we demonstrate that the rewriting logic system Maude can be used to automate time bounded verification of PTS.
A key component of mathematical reasoning is the ability to formulate interesting conjectures about a problem domain at hand. In this paper, we give a brief overview of a theory exploration system called QuickSpec, which is able to automatically discover interesting conjectures about a given set of functions. QuickSpec works by interleaving term generation with random testing to form candidate conjectures. This is made tractable by starting from small sizes and ensuring that only terms that are irreducible with respect to already discovered conjectures are considered. QuickSpec has been successfully applied to generate lemmas for automated inductive theorem proving as well as to generate specifications of functional programs. We give an overview of typical use-cases of QuickSpec, as well as demonstrating how to easily connect it to a theorem prover of the users choice.
suggested questions
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
