Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Confluence (informatique)
Résumé
In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.
The usual rules of elementary arithmetic form an abstract rewriting system.
For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses;
however, in both cases the same result is eventually obtained.
If every arithmetic expression evaluates to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system.
A second, more abstract example is obtained from the following proof of each group element equalling the inverse of its inverse:
This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting "1" to "a−1 ⋅ a" in the first step of R6's proof. One of the historical motivations to develop the theory of term rewriting was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program .
If a term rewriting system is confluent and terminating, a straightforward method exists to prove equality between two expressions (also known as terms) s and t:
Starting with s, apply equalities from left to right as long as possible, eventually obtaining a term s′.
Obtain from t a term t′ in a similar way.
If both terms s′ and t′ literally agree, then s and t are (not surprisingly) proven equal.
More importantly, if they disagree, then s and t cannot be equal.
That is, any two terms s and t that can be proven equal at all can be done so by that method.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Proximité ontologique
Cours associés (6)
ME-411: Mechanics of slender structures
Analysis of the mechanical response and deformation of slender structural elements.
FIN-609: Asset Pricing (2011 - 2024)
This course provides an overview of the theory of asset pricing and portfolio choice theory following historical developments in the field and putting
emphasis on theoretical models that help our unde
PHYS-425: Quantum physics III
To introduce several advanced topics in quantum physics, including
semiclassical approximation, path integral, scattering theory, and
relativistic quantum mechanics
Séances de cours associées (34)
Définitions de la valeur et conditions
Couvre les expressions conditionnelles et booléennes, les règles de réécriture et les définitions de valeurs.
Fonctions et état
Explore les fonctions, l'état, la réécriture et les objets stateful dans la programmation.
Valeurs propres et vecteurs propres: Comprendre les matrices
Explore les valeurs propres et les vecteurs propres dans les matrices à travers des exemples et des calculs.
Publications associées (36)
Personnes associées (2)
Concepts associés (6)
Abstract rewriting system
In mathematical logic and theoretical computer science, an abstract rewriting system (also (abstract) reduction system or abstract rewrite system; abbreviated ARS) is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set (of "objects") together with a binary relation, traditionally denoted with ; this definition can be further refined if we index (label) subsets of the binary relation.
Normal form (abstract rewriting)
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms. Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term. An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form.
Lemme de Newman
vignette|Confluence. vignette|Confluence locale. En mathématiques et en informatique, plus précisément dans la théorie des relations binaires, le lemme de Newman dit qu'une relation binaire noethérienne est confluente si elle est localement confluente. Une démonstration relativement simple (induction sur une relation bien fondée) est due à Gérard Huet en 1980. La démonstration originale de Newman est plus compliquée, mais la méthode des diagrammes décroissants montre bien comment elle fonctionne.