Leertaak 4
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
Instructie