Propriété d'un système de réécriture ou de réduction affirmant que chaque fois qu'un terme peut être réduit par deux suites (éventuellement distinctes) en des termes s et t, il existe un terme u vers lequel s et t peuvent encore réduire (c.-à-d. s ↓ u et t ↓ u). La confluence est souvent appelée propriété de Church–Rosser.

Principe

Les chemins de réduction différents à partir d'un même point peuvent être rassemblés : la divergence locale est sans conséquence puisque les réductions se rejoignent en un descendant commun, ce qui assure la cohérence du raisonnement équationnel et des résultats canoniques quand des formes normales existent.

Démonstration

Dans le lambda-calcul avec β-réduction, le théorème de Church–Rosser montre que si deux termes sont β-convertibles, ils ont un réduct commun. Concrètement, cela signifie que différents choix d'ordre d'évaluation (lorsque les réductions terminent) conduisent à la même forme normale à conversion près.

Mauvaise application

Supposer que la confluence implique la terminaison (c.-à-d. que toute suite de réduction atteint une forme normale) est incorrect. De même, présumer la confluence dans des systèmes avec effets de bord, règles sensibles au contexte ou opérations non déterministes peut conduire à des conclusions non valides.

Conséquence

Garantit l'unicité des formes normales à conversion près et permet d'interchanger les stratégies de réduction : le raisonnement équationnel et la transformation de programmes deviennent sûrs parce que différentes suites de réécriture ne produisent pas de résultats irréconciliables.

Inversion

Les systèmes non confluent admettent des divergences critiques où des suites de réduction différentes conduisent à des formes normales irréconciliables ou à des termes sans réduct commun, rendant le résultat dépendant du choix de réduction.

Limite

La confluence est une propriété de la relation de réduction et peut ne pas tenir en présence d'effets de bord, de réécritures sensibles au contexte non restreintes ou lorsque les réductions ne sont pas closes sous les propriétés de la relation. Le lemme de Newman relie la confluence locale plus la terminaison à la confluence globale.

Tension sémantique

Tension entre la confluence comme garantie de correction et des préoccupations pratiques telles que l'efficacité d'évaluation ou l'utilisation des ressources : un système confluent peut malgré tout admettre des chemins de réduction coûteux ou non terminants, donc la confluence n'implique pas la terminaison ni la performance.

Synthèse

La Confluence (propriété de Church–Rosser) garantit que des suites de réduction divergentes à partir d'un même terme peuvent être rassemblées en un réduct commun, assurant la cohérence des réécritures et des transformations de programmes tout en demeurant distincte des propriétés de terminaison ou de complexité.