Leertaak 11

Confluentie in termherschrijfsystemen

Achtergrond

Confluentie (Church-Rosser) is het herschrijf-equivalent van eenduidigheid en gedetermineerdheid in programma-evaluatie. Detectie van confluentie-eigenschappen is in het algemeen echter vaak moeilijk of onmogelijk.

Zwakke confluentie is veel makkelijker te analyseren, en voor terminerende systemen is dit equivalent aan confluentie (Lemma van Newman). Het begrip kritiek paar is de sleutel in de analyse van zwakke confluentie.

Het woordprobleem dat in zijn algemeenheid onbeslisbaar is, blijkt voor terminerende confluente TRSen heel gemakkelijk op te lossen.

Tenslotte geven we een techniek aan (Knuth-Bendix completering) waarmee een stel vergelijkingen dat aanvankelijk niet terminerend en/of confluent is, aangepast kan worden tot een herschrijfsysteem dat dat wel is.

Leerdoel

Na het voltooien van deze taak kunt u

• onderstaande kernbegrippen (zie 'Instructie') verklaren;
• van elke terminerende TRS vaststellen of deze confluent is of niet;
• bij elke tweetal termen vaststellen of ze converteerbaar zijn ten opzichte van een gegeven terminerende confluente TRS.

Instructie

1. Lees het dictaat vanaf pagina 39. Kernbegrippen:
   • confluent, CR
   • zwak confluent, WCR
   • lemma van Newman
   • overlap, kritieke paren, convergentie van kritieke paren
   • woordprobleem
   • Knuth-Bendix completering
2. Maak opgaven 12 tot en met 15 van de bijlage.