SÉMANTIQUES OPÉRATIONNELLES DE BSML

 SÉMANTIQUES OPÉRATIONNELLES DE BSML

Substitutions explicites

Le λ-calcul ne définit qu’une seule forme de transformation,la β-réduction. Celle-ci remplace l’application d’une fonction sur un argument par la valeur en résultant. Cette transformation est basée sur la substitution de l’argument aux variables le référençant.

Elle n’est d’ailleurs pas définie dans le λ-calcul mais plutôt représentée comme une méta-opération du langage dont la complexité n’est pas constante : la complexité dépend du terme auquel la substitution est appliquée.

En conséquence, sa transposition dans le code objet d’un programme (code machine) ne se résume pas à une simple séquence d’instructions à effectuer, mais à tout un mécanisme (difficile à prouver) que le code objet doit implanter. Pour cette raison, et bien qu’il décrive le code source des programmes fonctionnels, le λ-calcul n’est pas adapté parce que trop imprécis.

Les λ-calculs avec substitutions explicites vont fournir une réponse formelle à ce problème. Dans ces calculs, la substitution n’est plus une méta-opération mais une réduction (voire plusieurs en pratique) au même titre que la β-réduction.

Ceci a pour conséquence que la substitu tion devient une opération atomique. Outre une atomicité des opérations, les λ-calculs avec substitutions explicites amènent à se poser des questions sur la nature des composantes du calcul.

En particulier, ils nous obligent à préciser ce qu’est une variable (son instanciation), une substitution et une réduction (parallèle ou non). Les noms devariables posent problème dès qu’il s’agit d’implanter le λ-calcul : à chaque β-réduction,

le système doit gérer le renommagedes variables. Alors que pour un être humain, le renommagedes variables n’est qu’un détail (une α-conversion), une machine passerait une trop grande partie de son temps de calcul à changer ces noms.

C’est pourquoi, durant le développement de l’assistant de preuves AUTOMATH, De Bruijn [88] a été amené à décrire un λ-calcul où les variables sont remplacées par des entiers et où le renommageest une incrémentation (ou une décrémentation) de ces entiers. Le principe des indices de De Bruijn est de remplacer une variable par le nombre de λ qui la sépare du λ qui la lie.

Il n’est alors plus besoin d’étiqueter le λ par une variable, puisque cette information est déjà contenue dans chaque variable. Par exemple le λ-terme λx.((λy.(y x)) x) devient λ.((λ.(1 2)) 1) (voir à la figure 3.1). Notons que les entiers (en tant que variables) sont notés avec une barre afin de ne pas être confondus avec des entiers d’un langage de programmation.

De Bruijn présente alors un λ-calcul appelé λDB-calcul, confluent et isomorphe au λ-calcul [200]. Malgré tout, la substitution y reste une opération extérieure (et insécable) au calcul, et cela quelle que soit la complexité des termes manipulés. Pour remédier à ce défaut, de nombreuxauteurs ont proposé des λ-calculs où les substitutions font partie intégrante des termes.

Ces calculs fournissent une atomicité des opérations de substitution à base d’envi ronnements qui sont adjoints aux indices de De Bruijn. Les présenter tous serait fastidieux1, et nous allons simplement définir le λσw-calcul [216] muni d’une stratégie faible d’appel par valeur

 Langages fonctionnels et sémantiques opérationnelles

Le λ-calcul présente l’avantage d’avoir une sémantique propre ce qui représente un atout considérable pour le développement (et la certification) de programmes. En plus de sa simplicité, il offre une grande expressivité calculatoire (il est Turing-complet). Malgré tout, il est inefficace algorithmiquement parlant et inutilisable pour le commun des programmeurs : écrire une fonction «utile» en λ-calcul est un travail titanesque.

Les langages fonctionnels sont des extensions du λ-calcul permettant une programmation simple et ef f icace des fonctions. Ils sont donc des langages réalistes pour la programmation2. Ils conservent une sé mantique propre et l’introduction de structures de données permet la facilité d’écriture des programmes. La clarté de la sémantique des langages fonctionnels et leurs ressemblances avec les mathématiques ont fait qu’ils se sont imposés comme langages de base pour l’enseignement,

la recherche et, à moindre mesure, l’industrie (bien que leur utilisation dans ce domaine s’accroît). Les intérêts de définir la sémantique d’un langage de programmation sont : 1. De spécifier le sens des programmesécrits (ce qu’ils calculent); 2. De définir formellement le fonctionnement (le comment) de leurs calculs; 3. De préciser quels sont les programmes qui sont syntaxiquement corrects mais sémantiquement ab surdes : 1 + (λx.x);

. De permettre des études formelles sur les programmes; par exemple, une étude des coûts des pro grammes : quel programmesera alors le plus efficace? 5. De permettre des optimisations (au niveau des algorithmes ou de la modularité du code). Dans la littérature, nous trouvons trois méthodes pour spécifier la notion de programme absurde.

La pre mière est la sémantique à grands pas (aussi appelée sémantique naturelle) où les programmes absurdes sont ceux qui ne s’évaluent pas. Mais cette sémantique ne permet pas de différencier les programmes absurdes des programmes qui bouclent (qui ne se terminent pas).