Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userConfluence of algebraic rewriting systems
73
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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.
We generalize the notion of identities among relations, well known for presentations of groups, to presentations of n-categories by polygraphs. To each polygraph, we associate a track n-category, generalizing the notion of crossed module for groups, in order to define the natural system of identities among relations. We relate the facts that this natural system is finitely generated and that the polygraph has finite derivation type.
A coherent presentation of an n-category is a presentation by generators, relations and relations among relations. Completions of presentations by rewriting systems give coherent presentations, whose relations among relations are generated by confluence diagrams induced by critical branchings. This article extends this construction to presentations by polygraphs defined modulo a set of relations. Our coherence results are formulated using the structure of n-category enriched in double groupoids, whose horizontal cells represent rewriting sequences, vertical cells represent the congruence generated by relations modulo and square cells represent coherence cells induced by confluence modulo. We illustrate these constructions for rewriting modulo commutation relations in monoids and isotopy relations in pivotal monoidal categories.
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.
Many years ago, Rota proposed a program on determining algebraic identities that can be satisfied by linear operators. After an extended period of dormant, progress on this program picked up speed in recent years, thanks to perspectives from operated algebras and Grobner-Shirshov bases. These advances were achieved in a series of papers from special cases to more general situations. These perspectives also indicate that Rotas insight can be manifested very broadly, for other algebraic structures such as Lie algebras, and further in the context of operads. This paper gives a survey on the motivation, early developments and recent advances on Rotas program, for linear operators on associative algebras and Lie algebras. Emphasis will be given to the applications of rewriting systems and Grobner-Shirshov bases. Problems, old and new, are proposed throughout the paper to prompt further developments on Rotas program.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
