Substitution explicite

En informatique , les calculs lambda sont dits avoir des substitutions explicites s'ils accordent une attention particulière à la formalisation du processus de substitution . Cela contraste avec le calcul lambda standard où les substitutions sont effectuées par des réductions bêta de manière implicite qui n'est pas exprimée dans le calcul ; les conditions de « fraîcheur » dans de tels calculs implicites sont une source notoire d'erreurs. Le concept est apparu dans un grand nombre d'articles publiés dans des domaines très différents, tels que les machines abstraites , la logique des prédicats et le calcul symbolique .

Un exemple simple de calcul lambda avec substitution explicite est « λx », qui ajoute une nouvelle forme de terme au calcul lambda , à savoir la forme M⟨x:=N⟩, qui se lit « M où x sera substitué par N ». (La signification du nouveau terme est la même que l'idiome courant let x:=N ​​dans M de nombreux langages de programmation.) λx peut être écrit avec les règles de réécriture suivantes :

1. (λx.M) N → M⟨x:=N⟩
2. x⟨x:=N⟩ → N
3. x⟨y:=N⟩ → x (x≠y)
4. (M ₁ M ₂ ) ⟨x:=N⟩ → (M ₁ ⟨x:=N⟩) (M ₂ ⟨x:=N⟩)
5. (λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y et x non libre dans N)

Tout en rendant la substitution explicite, cette formulation conserve la complexité de la « convention des variables » du calcul lambda , nécessitant un renommage arbitraire des variables lors de la réduction pour garantir que la condition « (x≠y et x non libre dans N) » sur la dernière règle soit toujours satisfaite avant d'appliquer la règle. Par conséquent, de nombreux calculs de substitution explicite évitent complètement les noms de variables en utilisant une notation d'indice De Bruijn dite « sans nom » .

Les substitutions explicites ont été esquissées dans la préface du livre de Curry sur la logique combinatoire et sont issues d'une « astuce d'implémentation » utilisée, par exemple, par AUTOMATH , et sont devenues une théorie syntaxique respectable dans le calcul lambda et la théorie de la réécriture . Bien qu'elle soit en fait née avec de Bruijn , l'idée d'un calcul spécifique où les substitutions font partie du langage objet, et non de la méta-théorie informelle, est traditionnellement attribuée à Abadi , Cardelli , Curien et Lévy. Leur article fondateur sur le calcul λσ explique que les implémentations du calcul lambda doivent être très prudentes lorsqu'elles traitent des substitutions. Sans mécanismes sophistiqués de partage de structure, les substitutions peuvent provoquer une explosion de taille, et donc, en pratique, les substitutions sont retardées et explicitement enregistrées. Cela rend la correspondance entre la théorie et l'implémentation très non triviale et l'exactitude des implémentations peut être difficile à établir. Une solution consiste à intégrer les substitutions dans le calcul, c’est-à-dire à avoir un calcul de substitutions explicites.

Une fois la substitution explicitée, les propriétés de base de la substitution passent de sémantiques à syntaxiques. Un exemple très important est le « lemme de substitution », qui avec la notation de λx devient

• (M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (où x≠y et x non libre dans P)

Un contre-exemple surprenant, dû à Melliès, montre que la manière dont cette règle est encodée dans le calcul original de substitutions explicites n'est pas fortement normalisante . Suite à cela, une multitude de calculs ont été décrits essayant d'offrir le meilleur compromis entre les propriétés syntaxiques des calculs de substitutions explicites.