Qu'est-ce qu'une sorte de sémantique de langage de programmation?

9

Dans le chapitre 1 de Foundations pratiques pour les langages de programmation , l'auteur mentionne que les arbres de syntaxe abstraite sont associés aux tris .

Intuitivement, les tris sont comme des types, mais j'aimerais savoir s'ils ont une définition précise. Je serais heureux si certaines références sont également fournies.

rslima
la source

Réponses:

4

Cela dépend de la sémantique que nous prendrions pour les types et les sortes. - Cependant, des définitions brèves - peu informelles - pourraient être - Les tris sont des classes d'AST et les types sont des classes de valeurs .

Numéro47
la source
4

Il existe en fait beaucoup de similitudes entre les tris pour la syntaxe abstacte et les types tels qu'ils sont généralement compris. Mais les tris sont un concept syntaxique formel , et les arbres AS sont également une syntaxe, tandis que les types sont un concept sémantique .

La terminologie vient des algèbres terminales (également appelées algèbres libres ) et de l'algèbre universelle . Ce sont essentiellement des théories syntaxiques des structures algébriques, analysées indépendamment de toute interprétation. Ils ont été développés dans la première moitié du 20e siècle.

Un terme peut être vu comme un arbre, où les nœuds sont étiquetés à partir d'un ensemble fini d'opérateurs, chaque opérateur ayant une arité fixe qui spécifie le nombre de filles dans l'arbre. L'arité 0 est pour les feuilles. Dans les algèbres multi-triées, cela est affiné avec des tris, de sorte que chaque opérateur appartient à un tri, et les arités sont remplacées par une liste ordonnée de tris, qui fixe pour chaque fille le type de son opérateur principal. Le type d'un opérateur, avec la liste des types de sa fille, est appelé la signature de l'opérateur.

Dans les algèbres universelles, cela est encore affiné en introduisant des relations d'équivalence définies équativement entre les termes.

Bien qu'ils semblent s'être un peu estompés, ces concepts étaient assez populaires et beaucoup étudiés en informatique à la fin du XXe siècle, en tant qu'algèbres abstraites où ils étaient ensuite considérés comme une base pour les types de données abstraits, qui est, en partie, précurseur de ce qui est nos classes en programmation orientée objet.

Les algèbres universelles sont liées au développement de la théorie des catégories, qui est également fondamentale dans la vision actuelle des types et des langages de programmation.

Les algèbres sont des objets syntaxiques et sont destinées à être utilisées avec une interprétation dans certains domaines sémantiques correspondant à des types. Une interprétation est un homomorphisme qui mappe les tris en domaines de valeurs (types) et les opérateurs en fonctions entre ces domaines, afin que les signatures soient respectées, et les équations aussi dans le cas d'une algèbre équationnelle. C'est ainsi que vous pouvez appliquer les résultats de la théorie des groupes à n'importe quel domaine avec une opération qui respecte la définition d'un groupe.

Cette organisation a été jugée très pratique par les premiers chercheurs en langages de programmation, en particulier ceux concernés par la formalisation des langages de programmation. Il avait l'avantage d'isoler la syntaxe et la sémantique, et d'être mathématiquement bien compris.

Une autre raison de son adoption était le souci de développer des outils pour manipuler les programmes, soit dans des environnements de développement, soit dans des systèmes formels pour prouver les propriétés des programmes (qui se sont avérés être de plus en plus des problèmes jumeaux).

Cela a conduit à l'émergence du concept d' arbre de syntaxe abstraite (AST) pour les langages de programmation, qui sont essentiellement des termes d'une algèbre multi-triée (parfois affinée avec l'utilisation de l'union de tri dans certains systèmes). L'AST est la syntaxe de référence pour un langage, à partir duquel la sémantique peut être définie par homomorphisme comme dans la sémantique dénotationnelle.

Non seulement cela est pratique pour étudier la sémantique des langages, mais les arbres sont mieux structurés que les chaînes et donc une meilleure base pour développer des outils de programmation et des environnements de programmation.

Il permet d'isoler l'analyse qui était traditionnellement une partie désordonnée car les limites de la technologie d'analyse ont forcé l'utilisation de grammaires déformées. Il prend également en compte les problèmes de présentation.

Il permet de multiples représentations concrètes (chaîne ou graphique) des programmes, ce qui peut parfois être pratique (il n'y a aucune raison pour que l'utilisation de la ponctuation plutôt que des tabulations, ou l'inverse, dans la syntaxe du programme soit imposée aux personnes).

Il permet de définir facilement de nombreuses interprétations de programmes, et en quelque sorte , afin d'analyser les propriétés des programmes avec des interprétations abstraites.

Il est pratique pour écrire des outils de manipulation de programmes (semi-) automatisés, par exemple pour des transformations de programmes automatiques ou des traductions entre langues.

Les choses peuvent parfois être un peu plus compliquées dans la pratique, car certaines formes de syntaxe abstraite permettent à certains opérateurs de créer des arbres (expressions) qui appartiennent à plusieurs sortes (une manière informelle de les regarder). Par exemple, il pourrait y avoir un tri pour les constructions syntaxiques qui représentent des variables (entités assignables) et un autre pour les expressions. Mais toute variable peut être utilisée comme expression, l'inverse étant faux.

Les premiers articles sur ce sujet, pour les langages de programmation, remontent au milieu des années 70. La conceptualisation de l'époque était destinée à la production d'environnements de programmation soucieux de la syntaxe (le mot «dirigé» était alors utilisé). Recherchez Mentor et Centaur en Europe et Cornell Program Synthesizer aux États-Unis. Ils étaient les deux premiers systèmes à utiliser ces concepts de manière pratique. Beaucoup d'autres ont été développés par la suite.

Mais la syntaxe abstraite est antérieure à ces systèmes. Le langage Lisp (1958) avait une syntaxe abstraite, ce qui n'est pas surprenant car il a été développé par un logicien, et dans le but de créer des programmes qui manipulent des programmes (voir aussi ML et LCF ... qui sont venus plus tard). Mais Lisp n'était pas trié: tout était syntaxiquement une liste et une structure plus raffinée dépendait essentiellement de la sémantique. Cela a amené certaines personnes à considérer, quelque peu à tort, que Lisp n'avait pas de syntaxe.

babou
la source
Diriez-vous qu'il existe 2 hiérarchies différentes, l'une dans le pays de syntaxe et l'autre dans le pays de sémantique. En syntaxe, nous avons comme vous des AST et des sortes et des classes de sortes. En sémantique, nous avons des valeurs, des types, des sortes ... etc. N'y a-t-il pas des langages qui unissent les deux en un seul environnement de développement comme Twelf ou Coq?
CMCDragonkai
@CMCDragonkai Je dirais (sauf erreurs possibles) précisément ce que j'ai dit. Je n'appellerais pas ces hiérarchies, mais plutôt des domaines de (méta) discours. La séparation syntaxique-sémantique distingue ce dont nous parlons et comment nous le faisons, ce qui nécessite une représentation. Vous ne devriez pas vouloir mélanger la syntaxe et la sémantique d'une même langue, mais la syntaxe d'une langue peut être un objet de discours, donc appartenir à la sémantique d'une autre langue. En ce sens, vous pourriez voir une certaine unification, à manipuler avec soin. La syntaxe est toujours générée de manière finie, tandis que la sémantique n'a pas une telle contrainte.
babou
2

Il apparaît au chapitre quatre que les tris sont pour la syntaxe et les types pour la sémantique.

L'exemple de tableau de syntaxe à la page 40 traite des tris dans la langue L {num str}. Apparemment, les tris sont des catégories dans la syntaxe du langage.

En particulier, "plus" a une sorte, qui est la catégorie syntaxique de son résultat. Le type de l'opérateur "plus" est nommé "Exp". Cela représente le fait que syntaxiquement, une invocation de l'opérateur "plus" est une expression. Une invocation de l'opérateur "plus" peut remplir une position dans une arborescence de syntaxe abstraite où une expression est autorisée. C'est ce genre de construction qui est un «plus». C'est ainsi qu'il s'intègre dans la structure d'un texte qui représente un programme.

Le système de typage de la page 41 traite des types dans la langue L {num str}. Le type d'opérateur "plus", étant donné que ses opérandes ont le type "num", est "num". Ce jugement est une description partielle de la sémantique de l'opérateur "plus". Autrement dit, une partie de la signification de l'opérateur "plus" est la combinaison de deux nombres pour produire un nombre. Cette signification distingue "plus" des autres expressions.

En outre, il existe un tri nommé "Typ" qui contient les deux types, "num" et "str".

minopret
la source
1
Eh bien, il l'utilise dans ce concept, mais il ne le définit pas clairement. J'ai trouvé le terme «logique à plusieurs types» qui me semble que les sortes et les types sont des concepts liés vraiment fermés. Je voulais juste connaître une définition claire des deux.
rslima
C'est quelque chose à voir avec les "systèmes de type pur". Je soupçonne que nous pourrions considérer la présentation dans " Lambda Calculi with Types " comme conventionnelle. Mais ce n'est pas concis. Je n'ai pas encore trouvé de référence fournissant des définitions claires et concises de terme, type, type et tri.
minopret
Qu'en est-il des têtes de production dans un analyseur? Beaucoup de fois vous finissez par classer des grammaires sous des noms similaires comme Expression ou Type.
CMCDragonkai
1

Au début du chapitre 1, Harper donne un indice sur ce qu'il entend par le mot tri :

La syntaxe d'un langage spécifie les moyens par lesquels diverses sortes de phrases (expressions, commandes, déclarations, etc.) peuvent être combinées pour former des programmes.

Il définit l' expression de mot comme un arbre de syntaxe abstrait, dont il discute ensuite.

jcora
la source
Il me semble que «sortes» a été utilisé avec son sens anglais habituel ici, synonyme de «sortes».
Raphael
@Raphael Oui, mais il semble que ce sens soit cohérent avec ce dernier usage formel, n'êtes-vous pas d'accord?
jcora
Pas assez. L'expression "ce genre de X" peut apparaître souvent dans le livre; cette phrase ne signale aucunement que quelque chose est en train d'être défini. (De plus, ce passage ne correspond pas à la façon dont je comprends le terme «trier»).
Raphael
@Raphael OK, veuillez expliquer en quoi cet usage particulier est incohérent, cela m'informerait certainement, car c'est ainsi que je le comprends actuellement.
jcora
La notion de «tri» que je connais est associée à des nœuds individuels de l'AST, pas à un arbre entier (c'est ce que vous dites «expression» signifie dans votre source).
Raphael