Talk:Confluence (abstract rewriting)

I am not a Wiki-LaTeX expert, but this code may work for the article

I am not an expert in all bells and whistles, but this code may make more easy to embed the diagrams compared to upload a picture:

${\begin{array}{ccccc}{}&{}&{(11+9)\times (2+4)}&{}&{}\\{}&{\swarrow }&{}&{\searrow }&{}\\{20\times (2+4)}&{}&{}&{}&{(11+9)\times 6}\\{}&{\searrow }&{}&{\swarrow }&{}\\{}&{}&{20+6}&{}&{}\\\end{array}}$

If someone knows how to use \xymatrix, in wiki, it should look better.

Please feel free to use it (or \xymatrix if possible) to draw the examples of semi-confluent and local-confluent diagrams.

Can you talk about the link with other systems please

Is there any link with lattices or with domains in type theory?

suggestion

IMHO the motivating example given in the article is not term rewriting. A better example would be

$(11+9)\times 2+(11+9)\times 4$

versus

$11\times (2+4)+9\times (2+4)$

Please change if you agree.

91.23.255.99 (talk) 19:57, 25 November 2007 (UTC)

I don't agree; the original example is certainly term rewriting and is preferable because it is simpler. --Daira Hopwood ⚥ (talk) 16:28, 8 September 2013 (UTC)

What is the difference in the shape of the corresponding diagrams?

Do you mean it is better because $20\times 6$ is reductible?

I do not see the difference in the diagram of both reductions. Could you please be more explicit in why it is a better example.

Or are you thinking that it is better to first present some rules like $a\to bc,b\to c,c\to d,\ldots$ or something alike before presenting the diagram?

self-motivating variations

The article said "A number of variations on the idea of confluence exist. These are important since they enable us to draw equivalences between confluence in the sense above and these variations." It doesn't make much sense for the variations to be important because they enable us to do something that we would have had no reason to want to do if they hadn't existed in the first place. Unfortunately I don't know the real reason for their importance; this should perhaps be added. Joriki 03:53, 8 July 2006 (UTC)

Well, perhaps a good illustration of local confluence's important is in Newman's lemma: if we have strongly normalizing elements and local confluence we have confluence. I'm sure I remember reading elsewhere that the concept is important and why, but I'll need to go hit the books and get back to you on that one. Dysprosia 08:36, 8 July 2006 (UTC)

Local confluence is also important in the Knuth-Bendix procedure, since "local confluence" is decidable, whereas "confluence" is not. 133.6.205.147 (talk) 02:24, 8 April 2008 (UTC)

Local confluence is a weaker property than confluence. Thus for a given relation it at most as hard to prove/decide local confluence as to prove confluence. Proving local confluence is indeed often much easier. If we know in addition that the given relation is terminating, then we can use Newman's Lemma to show that the relation is not only locally confluent, but in fact confluent.Hermel (talk) 13:25, 13 July 2009 (UTC)

Confusion between defintions and equivalence of notions

The Church-Rosser property and confluence are equivalent, but in order to have some equivalence to show, the definitions must differ. In Terese the authors define them to be the same (and make note of it on p.11) from the way more common definitions of Church-Rosser and confluence that appear in all other sources cited in the abstract rewriting system article.

In general, it's not a good idea to follow Terese for definitions here because of the way complicated fashion in which they define an ARS, i.e. with indexed relations; that generates way more notions than needed in this presentation. Those notions are actually useful later in the book for defining say rewriting modulo an equivalence relation, but none of that stuff appears in this wiki article. Terese also uses unusual notations, like double-headed arrows for the reflexive transitive closure, and I don't see that convention followed in this article. Pcap ping 00:57, 12 August 2009 (UTC)

Wrong diamond diagram

The diamond diagram is wrong in that it does not follow (let alone explain) the convention used universally in this area of using dashed arrows for existential quantification and solid arrows only for universal quantification. Pcap ping 00:57, 12 August 2009 (UTC)