<figure><img src="image_1.png" /></figure>

HAL
open science

# Description par attributs semantiques de lisp pur et preuve de l'équivalence de la définition traductive et de l'évaluateur

Pierre Deransart

<figure><img src="image_2.png" /></figure>

To cite this version:

Pierre Deransart. Description par attributs semantiques de lisp pur et preuve de l'équivalence de la définition traductive et de l'évaluateur. [Rapport de recherche] IRIA-RR-220, IRIA. 1977, pp.26. hal-04716478

HAL Id: hal-04716478

https://inria.hal.science/hal-04716478v1

Submitted on 1 Oct 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
IRIA

laboria

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
B. P. 105 78150 - Le Chesnay
France
Tél.: 954 90 20

laboratoire de recherche
en informatique
et automatique

DESCRIPTION PAR
ATTRIBUTS SÉMANTIQUES
DE LISP PUR ET
PREUVE DE L'ÉQUIVALENCE
DE LA DÉFINITION TRADUCTIVE
ET DE L'ÉVALUATEUR

<figure><img src="image_4.png" /></figure>

Pierre DERANSART

Rapport de Recherche N° 220

Mars 1977
DESCRIPTION PAR ATTRIBUTS SÉMANTIQUES DE LISP PUR
ET PREUVE DE L'ÉQUIVALENCE DE LA DÉFINITION
TRADUCTIVE ET DE L'ÉVALUATEUR

Pierre Deransart

Résumé :

La définition de Lisp pur est donnée à partir de sa traduction dans le langage des formes, langage aisément implantable dans une machine à pile. La preuve est faite de l'équivalence de cette définition avec la définition par l'évaluateur Lisp pur. La démonstration sert d'exemple à la mise en place d'une preuve d'un compilateur Lisp à partir de sa définition par la méthode des attributs sémantiques. Le but de ce rapport est de montrer ce qu'est la description par attributs et d'illustrer son utilité. L'étude plus complète d'une preuve de compilateur fera l'objet d'un autre rapport.

Abstract :

This report gives a pure Lisp definition using a translation to a form-language. This object lan-
guage is easy to implement in a stack-machine. The equivalence between the translation and the
pure lisp evaluator is proved. This demonstration is an example of proof of a Lisp compiler defi-
ned by the method of semantic attributes. The goal of this report is to show an attribute descrip-
tion of a compiler and to illustrate one of its uses. The more complete study of compiler proof
by this method will be published in further report.

Mots clé

Lisp pur — Définition — Traduction — Preuve — Compilateur — Attributs sémantiques.

Pure Lisp — Translation — Correctness — Compiler — Semantic attributes.
TABLE DES MATIERES

1. Attributs sémantiques : définition, notations, dépendance et décoration

1.1. Notations syntaxiques

1.2. Attributs

1.3. Définition sémantique

2. Description de l'évaluateur Lisp pur par les attributs sémantiques

2.1. Principe

2.2. Le langage des formes

2.3. Le langage sémantique (traduction)

2.4. Attributs utilisés

2.5. La traduction

2.6. Définition de l'évaluateur EV

3. Preuve de l'équivalence de la définition traductive et de l'évaluateur Lisp pur

3.1. Principe de la preuve

3.2. L'évaluateur Lisp pur

3.3. Preuve
# INTRODUCTION

L'objet de ce rapport est de montrer la possibilité, sur le cas très simple de Lisp pur, de réaliser la preuve d'un compilateur défini par la méthode des attributs sémantiques. Un autre aspect d'une telle description est de dégager les vérifications syntaxiques opérées au cours de l'évaluation d'expressions Lisp, et donc de mettre clairement en évidence les aspects syntaxiques et interprétés du langage.

Trois parties composent ce rapport : une brève présentation de la méthode de description par attributs, la traduction d'expressions Lisp pur dans le langage des formes, langage dans lequel sont explicités tous les calculs de l'évaluateur, et la preuve proprement dite.

Un autre rapport présentera cette méthode pour un Lisp plus élaboré.
# 1. Attributs sémantiques : définition, notation, dépendance et décoration

## 1.1 Notations syntaxiques

Une grammaire hors contexte est définie par :

$$G = \{N, T, Z, P\}$$

où

* N est l'ensemble fini des symboles non terminaux

* T est l'ensemble fini des symboles terminaux

* Z ∈ N est l'axiome de la grammaire

* P est l'ensemble fini des règles de grammaire.

Toute règle de P s'écrit sous la forme :

$$X \to X_1 X_2 \dots X_n$$

où X est un symbole de N et $X_1, X_2, \dots, X_n$ des symboles de N ∪ T.

## 1.2 Attributs

A chaque symbole X on associe un ensemble fini d'attributs A(X).

Si $X \in N$, A(X) est partagé en deux sous-ensembles H(X) et S(X) dont les éléments sont respectivement attributs hérités et attributs synthétisés de X.

Si $X \in T$, A(X) contient un seul attribut standard noté TEXT(X) qui permet d'accéder au texte symbolique du terminal X.

Plus généralement, on note les attributs d'un symbole X sous la forme a(X) où a est un nom d'attribut pouvant être utilisé pour divers symboles.

## 1.3 Définition sémantique

Pour chaque règle $X_o \to X_1 X_2 \dots X_n$ on définit le calcul des attributs synthétisés de $X_o$ et les attributs hérités de chaque symbole $X_i$ en partie droite, par une fonction dont les arguments sont les attributs de $X_o$ ou des $X_i$.

Afin d'illustrer un tel calcul nous allons traiter un bref exemple. Pour ceci nous nous donnons un langage très simple d'expressions écrites selon une syntaxe de type Lisp. Ces expressions sont appelées des "formes" ; leur syntaxe est décrite à la figure 1.
1. `<Prog>` = `<Forme>`

2. `<Forme>` = `(opé <listarg>)`

3. `<listarg>` = `<listarg'> <arg>`

4. = $ε$

5. `<arg>` = `<Forme>`

6. = <Fquanté>

<caption>Fig.1 : Syntaxe des formes</caption>

Une expression de ce langage est par exemple :

(+(+’2’3) (+’4’5)’6)

L'évaluation d'une telle expression se fait de la manière suivante :
les arguments sont évalués et leurs valeurs empilées jusqu'à ce que, tous
les arguments ayant été empilés, on applique l'opérateur à l'ensemble des
arguments qui sont alors dépilés et remplacés en sommet de pile par la
valeur obtenue. Le schéma de la figure 2 illustre ce fonctionnement.

<figure><img src="image_5.png" /><figcaption>Fig.2 : Méthode d'évaluation des formes</figcaption></figure>

Nous allons chercher la hauteur de pile nécessaire pour évaluer une
forme, utilisant deux attributs :

L : hauteur maximale de la pile (synthétisé)

NARG : nombre d'arguments (synthétisé)

A chaque règle nous associons les modèles sémantiques donnés à la
figure 3.

1. L(Prog) = L(Forme)

2. L(Forme) = L(Listarg)

3. L(Listarg) = max(L(Listarg'), NARG(Listarg') + L(arg))
NARG(Listarg) = NARG(Listarg') + 1

4. L(Listarg) = 0
NARG(Listarg) = 0

5. L(arg) = L(Forme)

6. L(arg) = 1

<caption>Fig.3 : Modèles sémantiques associés à chaque règle (1 à 6)</caption>
Ces modèles définissent les calculs qui devront être effectués sur
les attributs. L'analyse de la forme :

(+(+’a’b) (+’c’d) ’e)

fournit l'arbre syntaxique de la figure 4.

<figure><img src="image_6.png" /><figcaption>fig 4 : arbre syntaxique décoré obtenu après analyse et numérotation.</figcaption></figure>
Cet arbre est _décoré_ par numérotation des noeuds ainsi que le montre la figure 4. A chaque noeud il est possible d'écrire l'ensemble des équations correspondant aux modèles sémantiques. Ainsi, au noeud 17 de la figure 4 qui correspond à l'application de la règle 3 correspondra le système suivant :

L17 = max(19, NARG9 + L16)

NARG17 = NARG9 + 1

L'ensemble des systèmes d'équations issues de l'arbre de la figure 4 constitue un seul système d'équations écrites dans un langage à assignation unique dans lequel la valeur recherchée est l'attribut synthétisé de la racine <Prog>, soit L21 sur cet exemple, qui vaut 3.

D'une manière générale on cherche à calculer un attribut synthétisé de l'axiome de la grammaire (Prog) correspondant au code objet généré.

## 2. Description de LISP pur par les attributs sémantiques

### 2.1 Principe

Le principe de la méthode de définition traductive par attributs consiste à définir la sémantique d'un programme par sa traduction dans un autre langage, en langage objet, considéré comme plus simple.

Nous utiliserons comme langage objet, le _langage des formes_ proche de celui utilisé dans certaines présentations de Lisp [1], [2]. Ce langage consiste à explicitier tous les calculs qui sont faits dans une S-expression de Lisp.

Exemple 1 :

en Lisp : (CAR(CDR(QUOTE(A B))))

en "Forme" : car [cdr [(A B)]]

où (A B) est une donnée, car et cdr des fonctions dans le langage objet. Le langage des formes a une sémantique simple : chaque programme de ce langage a une valeur, indépendante de son contexte d'exécution.

Toute fonction du langage des formes sera soulignée, ainsi que tous les mots-clé (si, alors, sinon, vide ...).
En général, le langage des formes est calqué sur la syntaxe de Lisp.
Nous ferons quelques entorses à cette règle en traduisant une expression
conditionnelle sous la forme *si ... alors ... sinon ... fsi*.
Ce langage
est d'autre part aisément évaluable, à l'aide d'une machine à piles par
exemple.

La description de Lisp pur par les attributs sémantiques consiste
alors à se donner :

- une syntaxe de Lisp pur

- une description du langage objet (langage des formes)

- une traduction par attributs dans le contexte de chaque règle de la
grammaire, du langage source dans le langage objet.

La traduction et l'évaluation se font selon le schéma suivant :
la traduction, comme l'évaluateur, partent d'un programme source et
d'un contexte d'exécution pour obtenir un programme objet.

<figure><img src="image_7.png" /></figure>

où

C est le contexte d'exécution du programme P.

P est le programme exprimé en langage source (S-expression de Lisp pur)

TR est la traduction de P en S dans le contexte C, cette traduction
s'exprime par une description par attributs écrite dans un langage
dit "langage sémantique".

S est la représentation sémantique exprimée en langage objet ou
langage des formes (LF).

EV est l'évaluateur du langage des formes, évaluateur simple explicité
plus loin (§3).

R le résultat de l'évaluation du texte objet.

L'obtention du programme objet se fait par la résolution d'un système
d'équations exprimé en langage sémantique et dont le résultat correspond
à la valeur calculée de l'attribut synthétisé (CEVAL ou CAPPLY) de la
racine de l'arbre d'analyse.

Nous allons donc exposer ici :

- le langage objet

- le langage sémantique ou forme d'écriture du système d'équations de traduction

- les attributs utilisés dans la définition traductive

- l'évaluation du langage objet.
## 2.2 Le langage objet : langage des formes

Sa syntaxe et des exemples sont fournis à l'annexe 1. L'axiome de la grammaire est <LF>. Une expression dans le langage des formes correspond à la S-expression de Lisp initiale, réécrite d'une part en mettant les arguments d'une fonction entre crochets :

Exemple 2: `(CONS(QUOTE X) (QUOTE Y)) -> cons[X, Y]`
d'autre part en faisant intervenir de manière explicite les fonctions appelées par l'évaluateur et le contexte d'évaluation.

Exemple 3: `(CONS X Y) -> cons[assoc[X, Co], assoc[Y, Co]]`
où Co est le contexte initial représenté par une aliste (1)
et `assoc` la fonction qui donne la valeur d'une variable dans le contexte fourni en argument de cette fonction.

Dans ce langage les seules fonctions qui apparaissent sont : les cinq fonctions de base (`car`, `cdr`, `cons`, `eq` et `atom`) et les 3 fonctions appelées par l'évaluateur Lisp pur : `assoc`, `pairlis`, `apply` (cf. Annexe 2-C). Les fonctions `eval` et `evlis` n'apparaissent pas car en Lisp pur ne sont acceptées en position de fonction que des label, λ-expressions, des variables ou les 8 fonctions précédentes. Quant aux occurrences de `eval` dans `apply`, elles correspondent à l'analyse d'une forme prise en compte dans l'analyse syntaxique et ne nécessitent donc pas de générer un appel à l'évaluateur.

Exemple 4: la S-expression

((LAMBDA(X)(X X)) (QUOTE(LAMBDA(X) (X X))))
où X est une variable fonctionnelle, correspond à l'expression
`apply[assoc[X, C1], [assoc[X, C1]], C1]` où

C1 = pairlis[[X], [(LAMBDA(X)(X X)), Co]

eval n'apparaît pas car chaque élément `<Forme>` a pu être analysé et traduit.

## 2.3 Le langage sémantique

C'est le langage dans lequel sont exprimés les calculs sur les attributs sémantiques. Le langage des formes étant assez proche des S-expressions, peu d'opérations sont nécessaires. La seule utilisée est la concatenation des chaînes générées exprimée par la juxtaposition des éléments générés.

Exemple 5: (Annexe 4, règle 2)

CEVAL(Forme) = assoc[TEXT(Ident) , C(Forme)]
où les parties soulignées correspondent aux éléments générés entre lesquels s'intercaleront les valeurs des attributs (à calculer) TEXT(Ident) et C(Forme).

<footnote>(1) La liste est une liste formée de couples composés du nom d'une variable et de la valeur associée. Elle est toujours enrichie par la gauche à chaque déclaration de variables et la valeur locale d'une variable est donc la valeur figurant dans le premier couple ayant le nom de cette variable rencontré à partir de la gauche.</footnote>
## 2.4 Les attributs

Chaque attribut représente un concept utile pour générer le texte objet. A chaque noeud de l'arbre syntaxique où il est défini, l'attribut a une valeur calculée. Ainsi l'attribut CAPPLY dénote le code généré aux noeuds `<Fatom>` et `<Fnatom>` (règles 1bis, 7 à 14 de l'annexe 4).

Il y a trois ensembles d'attributs :

a) CEVAL, CAPPLY, CEVLIS, CEVCON : 4 noms pour le même concept : le texte généré. Ces quatre dénominations sont utilisées pour rendre plus aisé le rapprochement avec l'évaluateur (Annexe 5).

b) ARG, C : arguments et contexte évalués. Ces deux attributs hérités correspondent au texte décrivant le calcul des listes d'arguments (ARG est initialisé avec CEVLIS - règles 5 et 6 de l'annexe 4) et les modifications de contexte (règles 13 et 14).

c) LIST, TEXT deux attributs utilitaires : le premier relevant la liste de variables d'une $\lambda$-expression afin de la mettre en argument de pairlis, le second dénotant le texte du langage source correspondant au terminal (Ident ou S-expr).

## 2.5 La traduction

Le calcul des attributs synthétisés de la racine et hérités des non terminaux du membre droit est donné pour chaque règle à l'annexe 4. Pour comprendre la traduction il suffit de suivre la circulation des attributs qui traduit les relations de dépendance entre attributs et donne l'ordre dans lequel ceux-ci devront être calculés (ordre d'évaluation des attributs). Nous illustrerons ceci par un seul exemple, tiré de la règle 15 (Annexe 4), reproduit à la figure 5 :

<figure><img src="image_8.png" /><figcaption>Fig.5 : Circulation des attributs CEVCON et C.</figcaption></figure>
Le calcul de l'attribut CEVCON au noeud <Listcond> dépend dans ce cas des attributs CEVAL aux noeuds <Forme> et de l'attribut CEVCON au noeud <Listcond>. Le résultat est en effet :

CEVCON(Listcond) = si CEVAL(Forme) alors CEVAL(Forme') sinon CEVCON(listcond) fsi où les primes correspondent aux occurrences plus à droite des non terminaux <Forme> et <Listcond> et où les occurrences CEVAL(Forme), CEVAL(Forme') et CEVCON(Listcond) doivent être remplacées par leur valeur calculée.

Dans cette règle on voit que le contexte est hérité sans calcul supplémentaire (identités de la règle 15) et que le texte généré est une expression si alors sinon fsi.

D'une manière générale, dans toutes les règles, contexte et arguments évalués sont hérités alors que le texte objet est synthétisé.

## 2.6 Définition de l'évaluation EV

La définition est fournie à l'annexe 6 et s'appuie sur la syntaxe du langage des formes fournie à l'annexe 1. Elle repose sur l'identité, admise comme postulat, des fonctions du langage des formes et de la fonction correspondante de l'évaluateur.

Ainsi :

car [suite d'expressions] est identique à (car suite de S-expr)
cdr [suite d'expressions] est identique à (cdr suite de S-expr)
cons [suite d'expressions] est identique à (cons suite de S-expr)
eq [suite d'expressions] est identique à (eq suite de S-expr)
atom [suite d'expressions] est identique à (atom suite de S-expr)
assoc [suite d'expressions] est identique à (assoc suite de S-expr)
pairlis [suite d'expressions] est identique à (pairlis suite de S-expr)
apply [suite d'expressions] est identique à (apply suite de S-expr)

L'évaluation de liste d'expressions du langage des formes (liste décrite avec des crochets et virgules) est la liste (décrite avec des parenthèses et sans virgule) des expressions évaluées. Si cette liste est vide, le résultat est nil, suivant en cela la fonction evlis de Lisp pur. (décrite à l'annexe 5).

Enfin l'évaluation des expressions si alors sinon fsi correspond à la définition de la fonction evcon de Lisp pur :
```
evcon(clauses, aliste)
    if eq(clauses, nil)
    then nil
    else if eq(eval(caar(clauses), aliste), nil)
        then evcon(cdr(clauses), aliste)
        else eval(cadar(clauses), aliste)
    fi
fi
```

sachant que chaque clause est traduite par une expression `si alors sinon fsi`
pour laquelle le prédicat est vrai dès que EV(LF) correspondant est différent
de nil, faux dans le cas contraire.

## 3. Preuve de la correction de la traduction

### 3.1 Principe de la preuve

Nous voulons montrer que le traducteur du langage des formes est correct, c'est-à-dire que le programme objet associé à une forme et un contexte est évalué en le même résultat que celui que donne l'évaluateur Lisp pur (eval) appliqué à cette forme et à ce contexte. Nous voulons donc montrer que le schéma de la figure 6 est commutatif :

<figure><img src="image_9.png" /><figcaption>Fig.6 : Schéma de la preuve</figcaption></figure>

La forme est une S-expression à évaluer, le contexte est la aliste initiale. La traduction TR est initialisée, dans la règle 1, avec ce contexte (Co).

Le programme objet est donné par l'attribut CEVAL(Forme). Le résultat peut être obtenu en calculant CEVAL(Forme). Cet évaluateur du texte objet (EV) peut être défini très simplement : il identifie les fonctions du texte objet avec celles utilisées dans l'évaluateur eval.
La preuve consiste alors à montrer que, pour toutes les formes et pour tous les contextes initiaux possibles, l'assertion suivante est toujours vérifiée aux noeuds <Forme> :

```
EV(CEVAL(Forme)) = eval(Forme, EV(C(Forme)))
```
où Forme est le texte terminal correspondant au noeud <Forme> de l'arbre syntaxique.

La preuve complète nécessite d'utiliser d'une part les axiomes de définition de l'évaluateur EV, d'autre part une série d'assertions analogues à la précédente, en particulier une égalité analogue sur les fonctions, qui fait appel aux arguments obtenus grâce à l'attribut ARG :

```
EV(CAPPLY(Fonction)) = apply(Fonction, EV(ARG(Fonction)), EV(C(Fonction)))
```

La preuve se fait par récurrence synthétisée [3], c'est-à-dire que pour chaque règle de grammaire, on admet les propriétés à démontrer pour la partie droite et on les montre pour la partie gauche.

## 3.2 L'évaluateur Lisp pur

C'est celui défini à l'annexe 5. Il correspond à l'évaluateur Lisp pur de Mc Carthy. Son écriture diffère seulement par le fait de considérer les 5 fonctions de base ainsi que quote et cond comme des fonctions dont on lance l'exécution par l'appel de exec. Pour COND, une telle exécution correspond à la fonction evcon du § 2.6.

## 3.3 Preuve

La preuve est établie in extenso à l'annexe 4. Elle utilise les règles sémantiques décrites dans la traduction de l'annexe 4, la définition de l'évaluateur du langage des formes EV, décrit à l'annexe 6, et l'évaluateur Lisp pur décrit à l'annexe 5.

Pour chaque règle de grammaire nous indiquons :

- les hypothèses : identités satisfaites aux non terminaux des membres droits

- l'identité à démontrer

- la démonstration, s'il y a lieu, qui utilise les hypothèses et les règles de définitions sémantiques.

Nous traitons ici un seul exemple, celui de la règle 13 :

```
Règle 13 : <Fnatom> = (LAMBDA(<Listvar>) <Forme>)
```

Définitions sémantiques :

S1 `CAPPLY(Fnatom) = CEVAL(Forme)`

S2 `C(Forme) = pairlis[LIST(Listvar), ARG(Fnatom), C(Fnatom)]`
**Hypothèse unique :**

$$EV(CEVAL(Forme)) = eval(Forme, EV(C(Forme)))$$

**Conclusion :**

$$EV(CAPPLY(Fnatom)) = apply(Fnatom, EV(ARG(Fnatom)), EV(C(Fnatom)))$$

**Preuve :**

On montre que les deux membres sont égaux. Partant du membre droit :

$$\begin{align*} \text{apply}(Fnatom, EV(ARG(Fnatom)), EV(C(Fnatom))) &= \\ &\quad \text{eval}(Forme, \text{pairlis}((\text{Listvar}), EV(ARG(Fnatom)), EV(C(Fnatom)))) \\ &\text{d'après la définition de apply dans le cas d'une } \lambda\text{-expression.} \end{align*}$$

Forme réfère le texte correspondant au non terminal <Forme>

Listvar réfère la séquence correspondant au non terminal <Listvar>,
l'argument de pairlis est donc bien (Listvar) avec parenthèses (cadr
dans apply pour une fonction répondant à cette syntaxe).

Par ailleurs, le 2è argument de eval correspond à $EV(C(Forme))$.

En effet :

$$\begin{align*} EV(C(Forme)) &= (\text{pairlis } \text{LIST}(\text{Listvar}) \ EV(\text{ARG}(\text{Fnatom})) \ EV(C(\text{Fnatom}))) \\ \text{LIST}(\text{Listvar}) \ \text{produit} \ (\text{Listvar}) \ \text{que l'évaluateur EV conserve (S-expr).} \\ \text{ARG et C deviennent } EV(\text{ARG}()) \text{ et } EV(C()). \end{align*}$$

L'évaluation de $C(Forme)$ donne donc une expression Lisp avec comme fonction pairlis non soulignée et les arguments évalués mis en séquence.
Ceci est équivalent à l'expression de pairlis dans eval indiquée ci-dessous.

Ainsi peut-on prouver que le texte généré reproduit bien la démarche de l'évaluateur de Lisp pur, ce texte étant en quelque sorte la trace du fonctionnement de l'évaluateur. Si cette trace ne comporte aucun appel à apply, le déroulement de l'évaluation peut être analysé de manière statique, la compilation complète de l'expression est possible.

L'exemple de preuve exposé ici montre qu'en généralisant cette démarche et qu'en utilisant toute la récursivité donnée par les attributs et les règles syntaxiques, il doit être possible de produire des preuves de compilateurs plus complexes définis par la méthode des attributs.
Remerciements

Je tiens à remercier MM. Lorho et Pair ainsi que Mme Dendien-Gaudel
pour l'aide qu'ils m'ont apportée dans ce travail.

Bibliographie

[1] Mc CARTHY & al. LISP 1.5 Programmer's Manual, The MIT Press, Cambridge, Mass. 1962.

[2] D. RIBBENS. Programmation non numérique Lisp 1.5. Dunod 1969, 141 p.

[3] C. PAIR, M. AMIRCHAHY, D. NEEL. Preuves de descriptions de traitements de textes par attributs. IRIA-LABORIA - Avril 1976

[4] B. LORHO. De la définition traductive des langages de programmation : méthode des attributs sémantiques. Thèse Université Paul Sabatier de Toulouse - 29 Novembre 1974.

[5] D.E. KNUTH. Semantics of Context-Free Languages - John Wiley & Sons, Inc.
New-York, 1971.
# ANNEXE I

## Langage des formes : Syntaxe

1. `<LF>` = S-expr
2. = `<Fatom> [<Liste de LF>]
3. = `si <LF> alors <LF> fsi`
4. = `si <LF> alors <LF> sinon <LF> fsi`
5. = [<Liste de LF>]
6. = [ ]
7. `<Liste de LF>` = `<LF>`, `<Liste de LF>`
8. = `<LF>`
9. et
suiv. `<Fatom>` = car | cdr | cons | eq | atom | assoc | pairlis | apply

S-expr correspond à la syntaxe suivante :

`<S-expr> = Ident | ( ) | (<Contenu de Liste>) | (<Contenu de paire pointée>)`

`<Contenu de Liste> = <S-expr> <Contenu de Liste> = <S-expr>`

`<Contenu paire pointée> = <S-expr>.<S-expr>`

S-expr représente une S-expression.

Exemples d'expressions du langage des formes :

* `assoc[X, Co]`

* `apply[assoc[X, Co], [(A.B), assoc[Y, Co]], Co]`

* `si car[assoc[X, Co]] alors cdr[assoc[X, Co]] fsi`

* `apply[assoc[X, pairlis[[X Y][assoc[X, Co], assoc[Z, Co]], Co]], [(A.B), (E F G), assoc[X, Co]], pairlis[[X Y][assoc[X, Co], assoc[Z, Co]], Co]]]`

La syntaxe du langage des formes est plus générale que ce qui sera généré par la définition traductive (cf. Annexe 4). En effet une traduction ne comportera que des expressions du type `apply[assoc[...](cf. règle 12.A4).`
ANNEXE 2

Attributs

<table><thead><tr><td>Attributs</td><td>Circulation*</td><td>Type</td><td>Signification</td></tr></thead><tbody><tr><td>CEVAL</td><td>S</td><td>Texte objet</td><td>Texte correspondant à une forme</td></tr><tr><td>CAPPLY</td><td>S</td><td>Texte objet</td><td>Texte correspondant à une fonction</td></tr><tr><td>CEVLIS</td><td>S</td><td>Texte objet</td><td>Texte correspondant à une liste d'arguments</td></tr><tr><td>CEVCON</td><td>S</td><td>Texte objet</td><td>Texte correspondant à une liste de clauses conditionnelles</td></tr><tr><td>ARG</td><td>H</td><td>Texte objet</td><td>Texte correspondant aux arguments</td></tr><tr><td>C</td><td>H</td><td>Texte objet</td><td>Texte correspondant au contexte</td></tr><tr><td>LIST</td><td>S</td><td>Texte objet</td><td>Texte correspondant aux variables</td></tr><tr><td>TEXT</td><td>S</td><td>chaîne</td><td>Texte correspondant à un atome ou une S-expression</td></tr></tbody></table>

<footnote>* S : synthétisé, H : hérité</footnote>
ANNEXE 3

## Syntaxe de Lisp pur

Cette syntaxe est déduite de l'évaluateur de l'annexe 5 et étendue aux fonctions autorisées en Lisp pur.

1 `<Prog> = <Forme>`

1 bis `<Prog> = <Fnatom>`

<co> règles utilisées pour initialiser le contexte <co>

2 `<Forme> = Ident`

3 = (QUOTE S-expr)

4 = (COND <Listcond>)

5 = (<Fatom> <Listarg>)

6 = (<Fnatom> <Listarg>)

<co> une fonction évalue toujours ces arguments. Fatom = Fonction atomique, Fnatom = Fonction non atomique <co>

7 `<Fatom> = CAR`

8 = CDR

9 = CONS

10 = ATOM

11 = EQ

<co> 5 fonctions de base de Lisp pur <co>

12 = Ident

<co> argument fonctionnel <co>

13 `<Fnatom> = (LAMBDA (<Listvar>) <Forme>)`

14 = (LABEL Ident <Fnatom>)

<co> légère restriction apportée au label : la fonction ne peut être atomique. Ceci est sans importance pratique <co>

15 `<Listcond> = (<Forme> <Forme'>) <Listcond>`

16 = (<Forme> <Forme'>)

17 `<Listarg> = <Forme> <Listarg>`

18 = empty

19 `<Listvar> = Ident <listvar>`

20 = empty
ANNEXE 4

Traduction de Lisp pur dans le langage des formes

Les attributs sont écrits avec des lettres capitales et le noeud est
écrit en minuscules, entre parenthèses.

Le texte généré est souligné.

Les calculs d'attributs sont écrits en minuscules.

La syntaxe est celle de l'annexe 3.

1 <Prog> = <Forme>

CEVAL(Prog) = CEVAL(Forme)

C(Forme) = Co co contexte du programme co

1 bis <Prog> = <Fnatom>

CEVAL(Prog) = CAPPLY(Fnatom)

C(Fnatom) = Co co contexte de la fonction co

ARG(Fnatom) = ARGo co liste de valeurs des arguments co

2 <Forme> = <Ident>

CEVAL(Forme) = assoc[TEXT(Ident), C(Forme)]

3 <Forme> = (QUOTE S-expr)

CEVAL(Forme) = TEXT(S-expr)

4 <Forme> = (COND <Listcond>)

CEVAL(Forme) = CEVCON(Listcond)

C(Listcond) = C(Forme)

5 <Forme> = (<Fatom> <Listarg>)

S1 CEVAL(Forme) = CAPPLY(Fatom)

S2 C(Fatom) = C(Forme)

S3 C(Listarg) = C(Forme)

S4 ARG(Fatom) = CEVLIS(Listarg)

6 <Forme> = (<Fnatom> <Listarg>)

id. règle 5.

7 <Fatom> = CAR
CAPPLY(Fatom) = car[ARG(Fatom)]

8 <Fatom> = CDR
CAPPLY(Fatom) = cdr[ARG(Fatom)]

9 <Fatom> = CONS
CAPPLY(Fatom) = cons[ARG(Fatom)], ARG(Fatom)]

10 <Fatom> = ATOM
CAPPLY(Fatom) = atom[ARG(Fatom)]
11 <Fatom> = EQ
CAPPLY(Fatom) = eq[ ARG(Fatom)), ARG(Fatom)) ]

12 <Fatom> = Ident
CAPPLY(Fatom) = apply[ assoc[TEXT(Ident), C(Fatom)], ARG(Fatom), C(Fatom) ]

13 <Fnatom> = (LAMBDA(<Listvar>) <Forme>)
CAPPLY(Fnatom) = CEVAL(Forme)
C(Forme) = pairlis[[LIST(Listvar)], ARG(Fnatom), C(Fnatom)]

14 <Fnatom> = (LABEL Ident <Fnatom>)
CAPPLY(Fnatom) = CAPPLY(Fnatom')
C(Fnatom') = pairlis[[TEXT(Ident)], [TEXT(Fnatom')], C(Fnatom)]
ARG(Fnatom') = ARG(Fnatom)

15 <Listcond> = (<Forme> <Forme>) <Listcond>
S1 CEVCON(Listcond) = si CEVAL(Forme)
                  alors CEVAL(Forme')
                  sinon CEVCON(Listond')
                  fsi

S2 C(Forme) = C(Listcond)

S3 C(Forme') = C(Listcond)

S4 C(Listcond') = C(Listcond)

16 <Listcond = (<Forme> <Forme>)
CEVCON(Listcond) = si CEVAL(Forme)
                  alors CEVAL(Forme')
                  fsi

C(Forme) = C(Listcond)

C(Forme') = C(Listcond)

17 <Listarg> = empty
CEVLIS(Listarg) = [ ]

<u>co</u> [] est la représentation d'une liste vide dans le langage
sémantique <u>co</u>

19 <Listvar> = Ident <Listvar>
LIST(Listvar) = ajouter en tête de LIST(Listvar') l'élément TEXT(Ident)

20 <Listvar> = empty
LIST(Listvar) = vide
ANNEXE 5

## Evaluateur Lisp pur

### eval(forme, aliste)

if atom(forme)

then assoc(forme, aliste)

elif atom(car(forme))

then if or (eq(car(forme), 'quote), eq(car(forme), 'cond)

then exec(car(forme), cdr(forme))

fi

else apply(car(forme), evlis(cdr(forme), aliste), aliste)

### apply(fonction, listvarg, aliste)

if atom(fonction)

then if or (eq(fonction, 'car), eq(fonction, 'cdr), eq(fonction, 'cons),
          eq(fonction, 'eq), eq(fonction, 'atom))

then exec(fonction, listvarg)

else apply(assoc(Fonction, aliste), Listvarg, aliste)

fi

elif eq(car(fonction), 'lambda)

then eval(caddr(fonction), pairlis(cadr(fonction), listvarg, aliste)

elif eq(car(fonction), 'label)

then apply(caddr(fonction), listvarg, cons(cons(cadr(fonction),
                                          caddr(fonction)), aliste)))

fi

### pairlis(listvar, listvarg, aliste)

if eq(listvar, nil)

then aliste

else cons(cons(car(listvar), car(listvarg)), pairlis
          (cdr(listvar), cdr(listvarg), aliste)))

fi

### evlis(listarg, aliste)

if eq(listarg, nil)

then nil

else cons.eval(car(listarg), aliste), evlis(cdr(listarg), aliste))

fi
# ANNEXE 6

## Définition de l'évaluateur EV

Cette définition suit la syntaxe donnée en Annexe I pour chaque règle de la syntaxe, EV(LF) est :

<table><thead><tr><th>Règles</th><th>Valeur obtenue</th></tr></thead><tbody><tr><td>&lt;LF&gt; = S-expr</td><td>EV(LF) = S-expr(allouer S-expr)</td></tr><tr><td>= &lt;Fatom&gt;[&lt;Liste de LF&gt;]</td><td>= Fonction &lt;Fatom&gt; non soulignée appliquée à EV(&lt;Liste de LF&gt;)</td></tr><tr><td>= <u>si</u> &lt;LF&gt; <u>alors</u> &lt;LF'&gt; <u>fsi</u></td><td>= <u>si</u>* EV(LF) <u>alors</u> EV(LF') <u>sinon</u> nil <u>fsi</u></td></tr><tr><td>= <u>si</u> &lt;LF&gt; <u>alors</u> &lt;LF'&gt; <u>sinon</u> &lt;LF''&gt; <u>fsi</u></td><td>= <u>si</u>* EV(LF) <u>alors</u> EV(LF') <u>sinon</u> EV(LF'') <u>fsi</u></td></tr><tr><td>= [<Liste de LF>]</td><td>= (EV(<Liste de LF>))</td></tr><tr><td>= []</td><td>= nil</td></tr><tr><td>&lt;Liste de LF&gt; = &lt;LF&gt;, &lt;Liste de LF&gt;</td><td>= EV(LF) EV(Liste de LF)</td></tr><tr><td>= &lt;LF&gt;</td><td>= EV(LF)</td></tr></tbody></table>

Chaque fonction `&lt;Fatom&gt;` non soulignée correspond à car, cdr, cons, eq, atom assoc, pairlis et apply de l'évaluateur `eval`.

L'évaluateur de `[&lt;Liste de LF&gt;]` correspond à une S-expression qui est la liste des éléments évalués.

Exemple :

```
EV(cons[assoc[X, Co], car[(A.B)]])) = en lisp
    (cons(assoc 'X 'Co) (car'(A.B)))
où cons, assoc, car sont les fonctions de Lisp pur, 'X, 'Co, '(A.B)
des constantes non évaluées.
```

<footnote>* Test de non égalité à nil.</footnote>
# ANNEXE 7

## Préuve de la traduction

Pour chaque règle de la grammaire nous indiquons :

- les hypothèses : identités satisfaites aux non-terminaux des membres droits.

- l'identité à démontrer.

- la preuve, s'il y a lieu.

Les définitions sémantiques sont celles de l'annexe 4. La preuve utilise ces définitions et les hypothèses.

Les règles 1 et 1 bis ne comportant que des identités et des initialisations, aucune preuve n'est donnée. Nous admettrons que Co est un contexte donné par une S-expression, la aliste initiale, et que (règle 1bis) ARGo est une S-expression représentant une liste d'arguments évalués. Les démonstrations qui suivent sont encore valables si la aliste et la liste d'arguments ne sont pas des S-expressions, mais contiennent des S-graphes. (1)

### Règle 2 : <Forme> = Ident

C : EV(CEVAL(Forme)) = eval(Forme, EV(C(Forme)))

En effet :

EV(CEVAL(Forme)) = EV(assoc[TEXT(Ident), C(Forme)]) (définition)
= (assoc TEXT(Ident) EV(C(Forme))) (définition de EV)
= eval(Ident, EV(C(Forme))) (définition de eval quand Forme est un atome).

### Règle 3 : <Forme> = (QUOTE S-expr)

C : EV(CEVAL(Forme)) = eval(Forme, EV(C(Forme)))

En effet :

EV(CEVAL(Forme)) = TEXT(S-expr) qui est un pointeur sur S-expr, ce qui est le résultat de eval appliqué à une telle forme.

### Règle 4 : <Forme> = (COND<Listcond>)

Pour cette règle, ainsi que pour les règles 15 et 16, il faut se reporter à la fonction evcon décrite au § 2.6 du chapitre 2. On a alors :

H = EV(CEVCON(Listcond)) = evcon((Listcond)*, EV(C(Listcond)))

C = EV(CEVAL(Forme)) = eval(Forme, EV(C(Forme))) immédiat vu les identités et le fait que l'évaluation de cette forme correspond à un appel de evcon avec pour arguments la liste des clauses et la aliste.

<footnote>(1) S-graphe : représentation interne des S-expression sous forme de graphe. Ces graphes peuvent être plus généraux et posséder des circuits.</footnote>
Règle 5 : `<Forme> = (<Fatom> <Listarg>)`

H1 : `EV(CAPPLY(Fatom))` = `apply(Fatom, EV(ARG(Fatom)), EV(C(Fatom)))`

H2 : `EV(CEVLIS(Listarg))` = `evlis((Listarg)*, EV(C(Listarg)))`

C : `EV(CEVAL(Forme))` = `eval(Forme, EV(C(Forme)))`

`eval(Forme, EV(C(Forme)))` = `apply(Fatom, evlis((Listarg), EV(C(Forme))),
EV(C(Forme)))` d'après la définition de
`eval` dans ce cas, ce qui avec les égalités S1 à S4
de la règle 5 est identique à `EV(CEVAL(Forme))`.

Règle 6 : `<Forme> = (<Fnatom> <Listarg>)`

Même démonstration vu que l'on est ramené au même cas dans `eval`.

Règle 7 : `<Fatom> = CAR`

C : `EV(CAPPLY(Fatom))` = `apply(Fatom, EV(ARG(Fatom)), EV(C(Fatom)))`

En effet :

`EV(CAPPLY(Fatom))` = `(car.EV(ARG(Fatom)))`

`apply( )` = `exec('car, EV(ARG(Fatom)), EV(C(Fatom)))`

qui donnent comme résultat dans les deux cas le car
du premier argument évalué.

Règles 8 à 11 : semblables à la précédente

Règle 12 : `<Fatom> = Ident`

C : `EV(CAPPLY(Fatom))` = `apply(Fatom, EV(ARG(Fatom)), EV(C(Fatom)))`

En effet :

`EV(CAPPLY(Fatom))` = `(apply(assoc 'TEXT(Ident) EV(C(Fatom))),
EV(ARG(Fatom))) EV(C(Fatom)))`

et

`apply(Fatom, EV(ARG(Fatom)), EV(C(Fatom)))` =
`apply.eval('TEXT(Ident), EV(C(Fatom))), EV(ARG(Fatom)), EV(C(Fatom)))`
(définition dans l'évaluateur)

ce qui est identique puisque, selon l'évaluateur :
`eval(Ident, aliste)` = `assoc(Ident, aliste)`.
Règle 13 : `<Fnatom> = (LAMBDA(<Listvar>) <Forme>)`

H : `EV(CEVAL(Forme))` = `eval(Forme, EV(C(Forme)))`
C : `EV(CAPPLY(Fnatom))` = `apply(Fnatom, EV(ARG(Fnatom)) EV(C(Fnatom)))`

En effet :

`apply(Fnatom, EV(ARG(Fnatom)), EV(C(Fnatom)))` =
`eval(Forme, pairlis((Listvar)*, EV(ARG(Fnatom)), EV(C(Fnatom)))))`

or :

`EV(C(Forme)) = (pairlis(LIST(Listvar))^* EV(ARG(Fnatom)) EV(C(Fnatom)))`
ce qui prouve l'identité sachant que `LIST(Listvar)` est l'attribut
donnant la liste des variables de la λ-expression, S-expression conservée
par EV.

Règle 14 : `<Fnatom> = (LABEL Ident <Fnatom'>)

H : `EV(CAPPLY(Fnatom'))` = `apply(Fnatom', EV(ARG(Fnatom')), EV(C(Fnatom')))`

C : `EV(CAPPLY(Fnatom))` = `apply(Fnatom, EV(ARG(Fnatom)), EV(C(Fnatom)))`
identique à la règle précédente.

Règle 15 : `<Listcond> = (<Forme> <Forme'>) <Listcond>'

H1 : `EV(CEVAL(Forme))` = `eval(Forme, EV(C(Forme)))`

H2 : `EV(CEVAL(Forme'))` = `eval(Forme', EV(C(Forme')))`

H3 : `EV(CEVCON(Listcond'))` = `evcon((Listcond')^*, EV(C(Listcond)))`

C : `EV(CEVCON(Listcond))` = `evcon((Listcond)^*, EV(C(Listcond)))`

En effet :

`EV(CEVCON(Listcond))` = `si EV(CEVAL(Forme)) (test de non égalité à nil)
    alors EV(CEVAL(Forme'))
    sinon EV(CEVCON(Listcond'))
    fsi` d'après S1 de la règle 15.

et la définition de EV. Et :

`evcon((Listcond)^*, EV(C(Listcond)))` =
`if eq.eval(Forme), EV(C(Listcond)), nil`
`then evcon((Listcond')^*, EV(C(Listcond)))`
`else eval(Forme', EV(C(Listcond)))`
`fi`

ce qui est identique d'après les hypothèses et S2 à S4 de la règle 15.
Règle 16 : `<Listcond>` = `<Forme> <Forme'>>`

H1 : `EV(CEVAL(Forme))` = `eval(Forme, EV(C(Forme)))`

H2 : `EV(CEVAL(Forme'))` = `eval(Forme', EV(C(Forme)))`

C : `EV(CEVCON(Listcond))` = `evcon((Listcond)*, EV(C(Listcond)))`

La démonstration est semblable à celle de la règle 15. Il faut tenir compte du fait que dans `evcon`, si la liste de clauses est vide (`liste = nil`) le résultat de `evcon` est `nil`.

Règle 17 : `<Listarg>` = `<Forme> <Listarg>'>`

H1 : `EV(CEVAL(Forme))` = `eval(Forme, EV(C(Forme)))`

H2 : `EV(CEVLIS(Listarg'))` = `evlis((Listarg'), EV(C(Listarg)))`

C : `EV(CEVLIS(Listarg))` = `evlis((Listarg)*, EV(C(Listarg)))`

La démonstration est immédiate en tenant compte des identités sémantiques et de la définition de `evlis` (Annexe 5).

Règle 18 : `<Listarg>` = `empty`

immédiat

Règle 19 : `<Listvar>` = `Ident <Listvar>`

Règle 20 : `<Listvar>` = `empty`

immédiat pour ces deux règles, l'attribut `LIST` conservant le texte original.

* Les parenthèses ajoutées ont pour but de transformer la séquence repérée par le non terminal nommé en une liste Lisp.