Pourquoi η est-elle une expansion ?
Réductions:
Dans le \(\lambda\)-calcul pur, on peut définir les deux règles suivantes:
Jusqu'ici, tout va bien : le système reste confluent.
Le problème apparaît dès lors qu'on veut introduire une règle de η-réduction pour la paire:
On a alors un pattern non-linéaire à gauche, et l'on perd normalisation et confluence.
Expansion
Dans le papier de Jay & Ghani, ils montrent comment dans un cadre 2-catégoriel, la règle η doit être une expansion. En particulier la règle d'η-expansion fonctionne bien pour la conversion.
Dans un cadre non-typé, on a:
L'article de Støvring [2] résoud le problème de confluence de l'η-expansion dans un cadre non-typé. Il montre que si l'on a :
alors on peut toujours se ramener à un réduit $v'$ pour lequel les réductions ne font pas apparaître de règle η pour la paire.
Remarques :
- L'η-expansion pour les paires est aussi appelée surjective pairing puisque cette règle permet de convertir tout terme en une paire.
- Le focusing correspond exactement au fait de considérer des formes β-normales η-longues.
Références
[1] C. Barry Jay & N. Ghani. The virtues of η-expansion pdf
[2] K. Støvring . Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative pdf