Comment lire les règles de frappe?

18

J'ai commencé à lire de plus en plus d'articles de recherche linguistique. Je trouve cela très intéressant et un bon moyen d'en savoir plus sur la programmation en général. Cependant, il y a généralement une section avec laquelle je me bats toujours (prenez par exemple la troisième partie de cela ) car je n'ai pas la formation théorique en informatique: les règles de type.

Existe-t-il de bons livres ou des ressources en ligne pour commencer dans ce domaine? Wikipédia est incroyablement vague et n'aide pas vraiment un débutant.

logic reference-request terminology type-theory suls
la source

1

Avez-vous lu l'article lié sur les règles d'inférence ?

Raphael

2

Le TAPL de Benjamin Pierce est vraiment bon.

Gilles 'SO- arrête d'être méchant'

25

Dans la plupart des systèmes de types, les règles de type fonctionnent ensemble pour définir des jugements de la forme:

Γ ⊢ e : τ

$\Gamma\vdash e:\tau$

Cela indique que dans le contexte l'expression a le type . est une cartographie des variables libres de à leurs types. $\Gamma$ $e$ $\tau$
$\Gamma$ $e$

Un système de types consistera en un ensemble d'axiomes et de règles (un système formel de règles d'inférence , comme le souligne Raphaël).

Un axiome est de la forme

\frac{}{Γ ⊢ e : τ}

$\dfrac{}{\Gamma \vdash e:\tau}$

Cela indique que le jugement est (toujours). $\Gamma \vdash e:\tau$

Un exemple est

\frac{}{X : τ ⊢ X : τ}

$\dfrac{}{x:\tau\vdash x:\tau}$

qui stipule que dans l'hypothèse où le type de variable est , alors l'expression a le type . $x$ $\tau$ $x$ $\tau$

Les règles d'inférence prennent des faits qui ont déjà été déterminés et en construisent des faits plus larges. Par exemple, la règle d'inférence

\frac{Γ ⊢ e_{1} : τ \to τ^{'} Γ ⊢ e_{2} : τ}{Γ ⊢ e_{1} e_{2} : τ^{'}}

$\dfrac{\Gamma\vdash e_1:\tau\to\tau' \quad \Gamma\vdash e_2:\tau}{\Gamma\vdash e_1\ e_2:\tau'}$

dit que si j'ai une dérivation du fait et une dérivation du fait , alors je peux obtenir une dérivation du fait . Dans ce cas, c'est la règle pour taper l'application de fonction. $\Gamma\vdash e_1:\tau\to\tau'$ $\Gamma\vdash e_2:\tau$ $\Gamma\vdash e_1\ e_2:\tau'$

Il existe deux manières de lire cette règle:

de haut en bas - étant donné deux expressions (une fonction et une autre expression) et quelques contraintes sur leur type, nous pouvons construire une autre expression (l'application de la fonction à l'expression) avec le type donné.
de bas en haut - étant donné une expression qui est, dans ce cas, l'application d'une fonction à une expression, la façon dont elle est typée est en tapant d'abord les deux expressions, en s'assurant que leurs types satisfont à certaines contraintes, à savoir que la première est un type de fonction et que le second a le type d'argument de la fonction.

Certaines règles d'inférence manipulent également en y ajoutant de nouveaux ingrédients (vue de bas en haut). Voici la règle pour -abstraction: $\Gamma$ $\lambda$

\frac{Γ X : τ ⊢ e : τ^{'}}{Γ ⊢ λ X . e : τ \to τ^{'}}

$\dfrac{\Gamma x:\tau\vdash e:\tau'}{\Gamma\vdash \lambda x.e:\tau\to \tau'}$

Les règles d'inférence sont appliquées de manière inductive en fonction de la syntaxe de l'expression considérée pour former un arbre de dérivation. Aux feuilles de l'arbre (en haut) seront des axiomes, et des branches seront formées en appliquant des règles d'inférence. Tout en bas de l'arborescence se trouve l'expression que vous souhaitez saisir.

Par exemple, une dérivation du typage de l'expression est $\lambda f.\lambda x.f\ x$

\frac{\frac{}{F : τ \to τ^{'}, X : τ ⊢ F : τ \to τ^{'}} \frac{}{F : τ \to τ^{'}, X : τ ⊢ X : τ}}{\frac{F : τ \to τ^{'}, X : τ ⊢ F X : τ^{'}}{\frac{F : τ \to τ^{'} ⊢ λ X . F X : τ^{'}}{⊢ λ F . λ X . F X : τ^{'}}}}

$\dfrac{\dfrac{}{f:\tau\to\tau',x:\tau\vdash f:\tau\to\tau'} \qquad \dfrac{}{f:\tau\to\tau',x:\tau\vdash x:\tau}} {\dfrac{f:\tau\to\tau',x:\tau\vdash f\ x:\tau'}{ \dfrac{f:\tau\to\tau'\vdash \lambda x.f\ x:\tau'}{\vdash \lambda f.\lambda x.f\ x:\tau'}}}$ Deux très bons livres pour apprendre sur les systèmes de types sont:

Types et langages de programmation par Benjamin Pierce
Fondements pratiques des langages de programmation par Robert Harper

Les deux livres sont très complets, mais ils commencent lentement, construisant une base solide.

Dave Clarke
la source

8

Il existe un joli didacticiel interactif en ligne sur le calcul séquentiel, qui peut aider à construire certaines intuitions et à ressentir le fonctionnement de l'inférence: Un didacticiel interactif du calcul séquentiel

aemxdp
la source

3

C'est vraiment cool.

Dave Clarke

1

Impressionnant. Je dois trouver un wiki de balises pour y mettre ça.

Raphael

5

Dans cette page Wikipédia, il est recommandé de " Type Systems, Luca Cardelli, ACM Computing Surveys ", qui est une enquête de 2 pages qui peut vous aider à comprendre comment lire une règle. Quoi qu'il en soit, la façon de lire une règle est parfaitement expliquée dans cette page Wikipédia (ou encore mieux dans l'enquête de 2 pages). Cependant, pour comprendre le tout, vous devez comprendre ce qu'est un système de frappe (composé de plusieurs règles), pour lequel l'article Wikipedia " Type system " est un bon début (et vous avez plusieurs livres dans la section " Références " de ce page si vous voulez aller plus loin).

Alejandro DC
la source

Comment lire les règles de frappe?

Réponses: