Proof that the Elegance Transformations are a Complete Set of Reductions

          First in thread      Previous in thread

This is an excerpt from my doctoral dissertation and was written in 1990.

A gentle warning - This proof gave me serious headaches in 1990 and they came rushing back as I started transcribing it for this post.

This should be the densest and hardest-to-read bit of writing that I'll post. I'm including it for completeness, but it can be accidentally overlooked without shame.

I'd still encourage the brave and curious to read through the proof, even a few of the 36 mind-numbing cases in the proof of Lemma 2.

Introduction

A set of transformations is a complete set of reductions (CSR) if and only if it is both noetherian and confluent. A set of transformations is said to be noetherian if every possible sequence of transformation applications to every structure in the set's domain is finite in length. One method for establishing the noetherianity of a set is to show that each transformation in the set necessarily reduces a particular measure of the structures in the set's domain. A set of transformations is said to be confluent if an exhaustive application of the transformations in the set to a structure in the set's domain will result in a unique normal form for that structure regardless of the order in which the applications are applied.

Demonstrating that a set of transformations is a complete set of reductions is highly desirable for, once a set has been shown to be a CSR, we need only be concerned with the efficiency of the algorithm for applying the transformations exhaustively.

Definition 1 - A set of transformations is a complete set of reductions iff it is both noetherian and confluent.

Definition 2 - A rewriting system is locally confluent iff

where M, M1, M2, and P are terms. (Le Chenadac 1986:17).

For our purposes, a constraint tree is a term. Observe that, while M₁ is not equal to M₂, P may be M₁, M₂, or neither. It is possible for the application of one transformation to both obviate and preclude the application of a second application.

Lemma 1 - The elegance transformations are noetherian.

Proof. Each of the eight elegance transformations reduces the weight of a constraint tree by some combination of releasing nodes, releasing constraints, and moving constraints closer to the root of the tree.

An application of the Delete-Inconsistent-Handle transformation results in the relase of at least one AND node and one constraint.

An application of the Promote-Common-Constraints transformation results in a reduction of the distance from the root to at least one constraint by two edges.

An application of the Subtract-Redundant-Constraints transformation results in the release of at least one constraint.

An applicationof the Cut-Unnecessary-OR transformation results in the release of one OR node and one AND Node. In addition, constraints may be released, and nodes and constraints may be moved closer to the root.

An application of the Cut-Unnecessary-AND transformation results in the release of one OR node and one AND node. In addition, nodes and constraints may be moved closer to the root.

An application of the 0-Constraint-Subsumption transformation results in the release of at least one AND node and one OR node. In addition, any nodes or constraints which are in the tree rooted at the POA's parent will be released.

An application of the 1-Constraint-Subsumption transformation results in the release of at least one constraint.

Since the weight of a constraint tree is finite, and the application of any of the elegance transformations necessarily reduces the weight of a constraint tree, there exists an upper bound on the number of times that any of the elegance transformations may be applied to a constraint tree, regardless of the transformations selected, or the order in which they are applied. Q.E.D.

Two applications will be said to interact iff the intersection of the critical set of one application and the modification set of the other application is not empty. If APP₁ and APP₂ do not interact, then <APP₁, APP₂> = <APP₂, APP₁>

Lemma 2 - The elegance transformations are locally confluent.

Proof - By Definition 2, the elegance transformations are locally confluent iff, for every pair R₁ and R₂ of transformations selected from the elegance transformations, every constraint tree T, every POA₁ in T at which R₁ may be applied, and every POA₂ in T at which R₂ may be applied, there exist two sequences of applications, S₁ and S₂, such that the first application in S₁ is R₁:POA₁, the first application in S₂ is R₂:POA₂, S₁ and S₂ both contain zero or more additional applications of an elegance transformation to a POA in T, and S₁ applied to T is equal to S₂ applied to T.

In order to prove that the elegance transformations are locally confluent, we will consider each of the 36 distinct pairs of transformations drawn from the elegance transformations. For each pair of transformations, we will identify the conditions under which applications of these transformations interact, and exhibit, for each case, sequences of applications which allow the different paths to converge.

For each pair of transformations discussed, the following notation will be used:

• T will denote an arbitrary constraint tree
• APP₁ will denote the application of the first transformation to a point of application in T which is denoted by POA₁
• APP₂ will denote the application of the second transformation to a point of application in T which is denoted by POA₂
• DSN₁ will denote the deletion-separation node for POA₁ in T
• DSN₂ will denote the deletion-separation node for POA₂ in T

Note that APP₁ may equal APP₂, POA₁ may equal POA₂, and DSN₁ may equal DSN₂.

Case 1 : InconHandle and InconHandle Interactions

APP₁ and APP₂ interact iff the parent of the DSN of one application is in the handle of the other.

If DSN₁ and DSN₂ coincide, then <APP₁> = <APP₂>.

If DSN₁ dominates DSN₂, then <APP₁> = <APP₂, APP₁>.

Similarly, if DSN₂ dominates DSN₁, then <APP₂> = <APP₁, APP₂>.

By Lemma 1, if DSN₁ and DSN₂ are siblings, then <APP₁, APP₂> = <APP₂, APP₁>.

If the parent of one DSN dominates, but is not the parent of, the other, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 2 : InconHandle and Promote Interactions

APP₁ and APP₂ interact if DSN₁'s parent and POA₂'s parent share a branch.

If DSN₁ dominates POA₂, then <APP₁> = <APP₂, APP₁>.

If POA₂ dominates DSN₁, but does not coincide with DSN₁'s parent, then <APP₁, APP₂> = <APP₂, APP₁>.

If DSN₁'s parent and POA₂ coincide, then there are two subcases to consider. Performing APP₁ first will remove one of POA₂'s children, but the intersection of the guard sets of POA₂'s children will still not be empty. Performing APP₂ first will not alter POA₁'s handle set. Therefore, the two applications may be performed independently, and <APP₁, APP₂> = <APP₂, APP₁>.

Case 3 : InconHandle and Redundant Interactions

APP₁ and APP₂ interact if DSN₁'s parent and POA₂ share a branch. However, since only one application involves deletion, we need only consider cases where DSN₁ and POA₂ share a branch.

If DSN₁ dominates or coincides with POA₂, then <APP₁> = <APP₂, APP₁>.

If POA₂ dominates DSN₁, then APP₂ will not alter the handle set of POA₁, and APP₂ does not obviate APP₁. Therefore, <APP₁, APP₂> = <APP₁>.

Case 4 : InconHandle and OrCut Interactions

APP₁ and APP₂ interact if DSN₁'s parent and POA₂'s parent share a branch. However, since only one application involves deletion, we need only consider cases wehre DSN₁ and POA₂'s parent share a branch.

If DSN₁ dominates POA₂, then APP₁ obviates, but is not obviated by, APP₂.

Since OrCut does not alter any branch sets, if POA₂'s parent dominates DSN₁, then <APP₁, APP₂> = <APP₂, APP₁>. Note that POA₂ can not be DSN₁'s parent, since POA₂ only has one child, and a DSN must either have a sibling or be the root of the tree.

Case 5 : InconHandle and AndCut Interactions

APP₁ and APP₂ interact if DSN₁'s parent and POA₂'s parent share a branch. However, since only one application involves deletion, we need only consider cases where DSN₁ and POA₂'s parent share a branch.

If POA₁ and POA₂ coincide, then POA₁'s grandparent's handle is inconsistent, since POA₁ contributes no constraints to its handle set. Therefore, POA₁'s grandparent is a site for InconHandle, and <APP₁, InconHndle:POA₁'s grandparent> = <APP₂, InconHandle:POA₁'s grandparent>.

If DSN₁ and POA₂ coincide, and POA₁ and POA₂ do not coincide, then performing APP₂ first will change the DSN for APP₁, but the new DSN will have the same parent as the prior DSN, and the effect of the deletion will be the same. Therefore, <APP₁> = <APP₂, APP₁>.

If DSN₁ dominates POA₂, and POA₁ and POA₂ do not coincide, then <APP₁> = <APP₂, APP₁>.

If POA₂ dominates DSN₁, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 6 : InconHandle and 0Subsume Interactions

APP₁ and APP₂ interact if DSN₁'s parent and POA₂'s parent share a branch. However, since only one application involves deletion, we need only consider the case where DSN₁ and POA₂'s parent share a branch.

If DSN₁ either dominates or coincides with POA₂'s parent, then <APP₁> = <APP₂, APP₁>.

If POA₂ dominates DSN₁, then APP₂ obviates APP₁, and <APP₂> = <APP₁, APP₂>.

Case 7 : InconHandle and 1Subsume Interactions

APP₁ and APP₂ interact iff the parent of the DSN of one application is in the handle of the other.

If DSN₁ and DSN₂ coincide, then the two applications have identical effects, and each obviates the other. Therefore, <APP₁> = <APP₂>.

If DSN₁ dominates DSN₂, then APP₁ obviates, but is not obviated by, APP₂. Therefore, <APP₁> = <APP₂, APP₁>.

Similarly, if DSN₂ dominates DSN₁, then <APP₂> = <APP₁, APP₂>.

By Lemma 1, if DSN₁ and DSN₂ are siblings, then <APP₁, APP₂> = <APP₂, APP₁>.

If the parent of one DSN dominates, but is not the parent of, the other, then the two applications may be performed independently, and <APP₁, APP₂> = <APP₂, APP₁>.

Case 8 : InconHandle and 1CCSubtract Interactions

APP₁ and APP₂ interact if the parent of DSN₁ is in the handle of POA₂. However, since only one application involves deletion, we may consider only the cases where DSN₁ is in the handle of POA₂.

We shall assume that APP₂ is supported by the constraint X in the guard set of node COM₂. The guard set of POA₂ contains the opposite of X.

If POA₁'s hand set is inconsistent only because it contains both X and the opposite of X, then there are two subcases to consider. If COM₂'s dominant set contains X, then COM₂'s parent is a site for 0Subsume, and <APP₁, 0Subsume:COM₂'s parent> = <APP₂, 0Subsume:COM₂'s parent>. If COM₂'s dominant set does not contain X, then COM₂ must command a node (POA₃) in the handle of POA₁ which contains X, in which case this node in the handle of X is a site for 1Subsume. If POA₂ dominates DSN₃, then <APP₁, 1Subsume:POA₃, APP₂> = <APP₂, 1Subsume:POA₃>; otherwise, <APP₁, 1Subsume:POA₃> = <APP₂, 1Subsume:POA₃>.

If POA₁'s handle set is inconsistent on some variable other than that which is constrained by X, then performing APP₂ first can have no effect on the inconsistency of POA₁'s handle. If it is also the case that POA₂ dominates DSN₁, then <APP₁, APP₂> = <APP₂, APP₁>; otherwise, <APP₁> = <APP₂, APP₁>.

Case 9 : Promote and Promote Interactions

APP₁ and APP₂ interact if POA₁ and POA₂ coincide, or if either POA is the grandparent of the other.

If POA₁ and POA₂ coincide, then <APP₁, APP₂> = <APP₂, APP₁>.

If POA₁ is the grandparent of POA₂, then APP₂ may raise one or ore constraints which will permit a new constraint to be promoted by APP₂. Therefore, either <APP₁, APP₂> = <APP₂, APP₁>, or <APP₁, APP₂, APP₁> = <APP₂, APP₁>.

Similarly, if POA₂ is the grandparent of POA₁, then either <APP₁, APP₂> = <APP₂, APP₁> or <APP₁, APP₂> = <APP₂, APP₁, APP₂>.

Case 10 : Promote and Redundant Interactions

APP₁ and APP₂ interact if POA₁ is the parent of POA₂.

If POA₁ is the parent of POA₂, then either the intersection of the set of constraints being promoted and the set of redundant constraints being subtracted is empty, or it is not. If the intersection set is empty, then <APP₁, APP₂> = <APP₂, APP₁>. If the intersection set is not empty, then POA₁'s parent may be a site for Promote, and <APP₁, APP₂, Promote:POA₁'s parent> = <APP₂, APP₁>, or <APP₁, APP₂, Promote:POA₁'s parent> = <APP₁, APP₂, Promote:POA₁'s parent>, or <APP₁, APP₂> = <APP₂, APP₁>, depending on whether POA₁'s parent was previously a site for Redundant, and whether any new constraints were added to POA₁'s parent's guard set by APP₁.

Case 11 : Promote and OrCut Interactions

App₁ and APP₂ interact if POA₁ and POA₂ coincide, or if either POA is the grandparent of the other.

if POA₁ and POA₂ coincide, then APP₁ and APP₂ result in identical trees, and <APP₁> = <APP₂>.

If POA₁ is the grandparent of POA₂, then it is possible that APP₂ may raise a constraint which would permit a new constraint to be promoted by APP₁. Therefore, either <APP₁, APP₂> = <APP₂, APP₁> or <APP₁, APP₂, APP₁> = <APP₂, APP₁>.

If POA₂ is the grandparent of POA₁, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 12 : Promote and AndCut Interactions.

APP₁ and APP₂ do not interact. Note that POA₁ can not be the parent of POA₂, since each child of the POA of a promotion must contain at least one constraint. Also, POA₂ can not be the parent of POA₁ since, by the definition of AndCut, no child of an AndCut site can be a site for Promote. Therefore, <APP₁, APP₂> = <APP₂, APP₁>.

Case 13 : Promote and 0Subsume Interactions

APP₁ and APP₂ interact if POA₂ dominates POA₁.

If POA₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 14 : Promote and 1Subsume Interactions

APP₁ and APP₂ interact if POA₁ is the parent of COM₂ or if DSN₂ dominates POA₂.

If POA₁ is the parent of COM₂, and the constraint in COM₂ would be promoted by APP₁, then POA₁ would be a site for 0Subsume after APP₁ had been performed. Therefore, <APP₁, 0Subsume:POA₁> = <APP₂, APP₁, 0Subsume:POA₁>.

If DSN₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 15 : Promote and 1CCSubtractInteractions

APP₁ and APP₂ interact if POA₁ is the parent of POA₂.

If POA₁ is the parent of both POA₂ and COM₂, then <APP₁, 0Subsume:COM₂> = <APP₂, APP₁, 0Subsume:COM₂>.

If POA₁ is the parent of POA₂, but not of COM₂, then either <APP₁, APP₂> = <APP₂, APP₁>, or <APP₁> = <APP₁, APP₂>, depending on whether the constraint in COM₂ would be promoted by APP₁.

Case 16 : Redundant and Redundant Interactions

APP₁ and APP₂ interact if either POA is in the handle of the other.

If POA₁ and POA₂ coincide, then <APP₁, APP₂> = <APP₂, APP₁>.

If POA₁ dominates POA₂, then performing APP₁ first will not change the dominant set of POA₂, and <APP₁, APP₂> = <APP₂, APP₁>.

Similarly, if POA₂ dominates POA₁, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 17 : Redundant and OrCut Interactions

APP₁ and APP₂ interact if POA₂ dominates POA₁, or if POA₁ is the parent of POA₂.

If POA₂ dominates POA₁, then <APP₂, APP₁> = <APP₁, APP₂>, for OrCut does not modify any selection sets.

If POA₁ is the parent of POA₂, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 18 : Redundant and AndCut Interactions

APP₁ and APP₂ interact if POA₂ dominates POA₁.

If POA₂ dominates POA₁, then <APP₁, APP₂> = <APP₂, APP₁>, for AndCut does not modify any selection sets.

Case 19 : Redundant and 0Subsume Interactions

APP₁ and APP₂ interact if POA₂ dominates POA₁.

If POA₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 20 : Redundant and 1Subsume Interactions

APP₁ and APP₂ interact if POA₁ and COM₂ coincide, if POA₁ and POA₂ coincide, or if DSN₂ dominates POA₁.

Let X be the constraint which is in the guard set of COM₂.

If POA₁ and POA₂ coincide, then either COM₂ is dominated by a node containing X, or COM₂ commands a node POA₃ containing X which, in turn, dominates POA₁. In the first case, COM₂ is a site for Redundant, after which its parent would be a site for 0Subsume, and <APP₁, Redundant:COM₂, 0Subsume:COM₂'s parent> = <APP₂, Redundant:COM₂, 0Subsume:COM₂'s parent>. In the second case, POA₃ is a site for 1Subsume, which would obviate, but not be affected by, APP₁ and APP₂, so that <APP₁, 1Subsume:POA₃> = <APP₂, 1Subsume:POA₃>.

If DSN₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 21 : Redundant and 1CCSubtract Interactions

APP₁ and APP₂ interact if POA₁ and COM₂ coincide, or if POA₂ is in POA₁'s handle.

If POA₁ and COM₂ coincide, then <APP₁, 0Subsume:POA₁'s parent> = <APP₂, APP₁, 0Subsume:POA₁'s parent>.

If POA₂ dominates POA₁, then <APP₁, APP₂> = <APP₂, APP₁>.

If POA₂ and POA₁ coincide, and the constraint which APP₂ will subtract is among those which APP₁ will subtract, then <APP₁> = <APP₂, APP₁>. If the constraint which APP₂ will subtract is not among those which APP₁ will subtract, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 22 : OrCut and OrCut Interactions

APP₁ and APP₂ interact if POA₁ and POA₂ coincide.

If POA₁ and POA₂ coincide, then <APP₁> = <APP₂>.

Case 23 : OrCut and AndCut Interactions

APP₁ and APP₂ interact if either POA is the parent of the other.

If POA₁ is the parent of POA₂, then APP₁ and APP₂ result in identical trees, and <APP₁> = <APP₂>.

If POA₂ is the parent of POA₁, then APP₁ and APP₂ result in identical trees, and <APP₁> = <APP₂>.

Case 24 : OrCut and 0Subsume Interactions

APP₁ and APP₂ interact if POA₁ and POA₂ coincide, or if POA₂ dominates POA₁.

If POA₁ and POA₂ coincide, the APP₁ and APP₂ result in identical trees, and <APP₁> = <APP₂>.

If POA₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 25 : OrCut and 1Subsume Interactions

APP₁ and APP₂ interact if POA₁ is the parent of POA₂, or if DSN₂ dominates POA₁.

If POA₁ is the parent of POA₂, then DSN₂ must dominate POA₁, and <APP₂> = <APP₁, APP₂>.

If DSN₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 26 : OrCut and 1CCSubtract Interactions

APP₁ and APP₂ interact if either POA is the parent of the other.

If POA₁ is the parent of POA₂, then <APP₁, 1CCSubtract:POA₁'s parent> = <APP₂, APP₁>.

If POA₂ is the parent of POA₁, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 27 : AndCut and AndCut Interactions

APP₁ and APP₂ interact if POA₁ and POA₂ coincide.

If POA₁ and POA₂ coincide, then <APP₁> = <APP₂>.

Case 28 : AndCut and 0Subsume Interactions

APP₁ and APP₂ interact if POA₁ is the parent of POA₂, or if POA₂ dominates POA₁.

If POA₁ is the parent of POA₂, then POA₁ will become a site for 0Subsume after APP₂, so that <APP₁, APP₂> = <APP₂, 0Subsume:POA₁>.

If POA₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 29 : AndCut and 1Subsume Interactions

APP₁ and APP₂ interact if DSN₂ dominates POA₁.

If DSN₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 30 : AndCut and 1CCSubtract Interactions

APP₁ and APP₂ do not interact. Therefore, <APP₁, APP₂> = <APP₂, APP₁>.

Case 31 : 0Subsume and 0Subsume Interactions

APP₁ and APP₂ interact if POA₁ and POA₂ coincide, or if either POA dominates the other.

If POA₁ and POA₂ coincide, then <APP₁> = <APP₂>.

If POA₁ dominates POA₂, then <APP₁> = <APP₂, APP₁>.

Similarly, if POA₂ dominates POA₁, then <APP₂> = <APP₁, APP₂>.

Case 32 : 0Subsume and 1Subsume Interactions

APP₁ and APP₂ interact if POA₁ and DSN₂ share a branch.

If POA₁ dominates DSN₂, then <APP₁> = <APP₂, APP₁>.

If DSN₂ dominates or coincides with POA₁, then POA₂ dominates POA₁ and <APP₂> = <APP₁, APP₂>.

Case 33 : 0Subsume and 1CCSubtract Interactions

APP₁ and APP₂ interact if POA₁ dominates POA₂.

If POA₁ dominates POA₂, then <APP₁> = <APP₂, APP₁>.

Case 34 : 1Subsume and 1Subsume Interactions

APP₁ and APP₂ interact if DSN₁ and DSN₂ share a branch or a parent, or if either POA and the COM for the other POA coincide.

If DSN₁ and DSN₂ coincide, then <APP₁> = <APP₂>.

If DSN₁ dominates DSN₂, then <APP₁> = <APP₂, APP₁>.

If DSN₂ dominates DSN₁, then <APP₂> = <APP₁, APP₂>.

If DSN₁ and DSN₂ are siblings, then <APP₁, APP₂> = <APP₂, APP₁>.

If POA₁ and COM₂ coincide, then COM₁ and COM₂ have the same constraint, COM₁ commands POA₂, and <APP₁, APP₂> = <APP₂, APP₁>.

Similarly, if POA₂ and COM₁ coincide, then <APP₁, APP₂> = <APP₂, APP₁>.

Case 35 : 1Subsume and 1CCSubtract Interactions

APP₁ and APP₂ interact if DSN₁ is in POA₂'s handle, or if POA₂ and COM₁ coincide.

If DSN₁ dominates POa₂, then APP₁ obviates but is not affected by APP₂, and <APP₁> = <APP₂, APP₁>.

If DSN₁ and POA₂ coincide, but DSN₁ and POA₁ do not coincide, then APP₁ obviates but is not affected by APP₂, and <APP₁> = <APP₂, APP₁>.

If POA₁ and POA₂ coincide, then either the constraint in COM₁ is the negation of the constraint in COM₂, or it is not. If COM₁ and COM₂ have opposing constraints, then APP₂ will preclude APP₁. If this happens, however, then COM₁ commands COM₂, COM₂ commands COM₁, or they command each other, and the COM which is closer to POA₁ will be a site for 1CCSubtract, and its parent will be a site for a subsequent application of 0Subsume, so that <APP₁> = <APP₂, 1CCSubtract:lower COM, 0Subsume:parent of lower COM>. However, if COM₁ and COM₂ do not have opposing constraints, then APP₁ obviates but is not afffected by APP₂, and <APP₁> = <APP₂, APP₁>.

If POA₂ and COM₁ coincide, then APP₂ will cause COM₁'s parent ot be a site for 0Subsume, which obviates APP₁, so that <APP₁, APP₂, 0Subsume:COM₁'s parent> = <APP₂, 0Subsume:COM₁'s parent>.

Case 36 : 1CCSubtract and 1CCSubtract Interactions

APP₁ and APP₂ interact if if POA₁ and POA₂ coincide, or if either POA coincides with the other POA's COM.

If POA₁ and POA₂ coincide and APP₁ and APP₂ subtract the same constraint, then APP₁ obviates and is obviated by APP₂, and <APP₁> = <APP₂>.

If POA₁ and POA₂ coincide and APP₁ and APP₂ do not subtract the same constraint, then the two applications may be applied independently, and <APP₁, APP₂> = <APP₂, APP₁>.

If POA₁ and COM₂ coincide, then APP₁ precludes, but is not affected by, APP₂. However, POA₂ must be a site for Redundant, so that <APP₁, Redundant:POA₂> = <APP₂, APP₁>.

Similarly, if POA₂ and COM₁ coincide, then <APP₂, Redundant:POA₁> = <APP₁, APP₂>.

Since each of the 36 distinct pairs of transformation drawn from the elegance transformations supports the criterion for local confluence stated in Definition 2, the elegance transformations are locally confluent. Q.E.D.

Lemma 3 (Newman) - Let R be a noetherian rewriting system, then: R is confluent iff R is locally confluent.

A discussion of Huet's proof of Newman's lemma may be found in (Le Chenandec 1986:17).

Lemma 4 - The elegance transformations are confluent.

Proof. By Lemma 1, the elegance transformations are noetherian. By Lemma 2, the elegance transformations are locally confluent. Since the elegance transformations are both noetherian and locally confluent, the the elegance transformations are confluent, by Lemma 3. Q.E.D.

Theorem - The elegance transformations are a complete set of reductions.

Proof. By definition, a set of transformation sis a complete set of transformations iff the set of transformations is both noetherian and confluent. Since the elegance transformations are noetherian, by Lemma 1, and confluent, by Lemma 4, the elegance transformations are a complete set of reductions. Q.E.D.

References

Le Chenandec, P. Canonical Forms in Finitely Presented Algebras. John Wiley & Sons, New York, N.Y., 1986.

          First in thread      Previous in thread

Copyright and Legal Notices

All Rights Reserved.