Cours 5: Sémantique dénotationnelle

Introduction

\begin{matrix} A, B ≝ α ∣ A \to B \\ M, N ≝ x^{A} ∣ λ x^{A} . M ∣ M N \end{matrix}

Sémantique dénotationnelle: “modèle” d’une théorie équationnelle:

\begin{matrix} (λ x . M) N = M [N / x] \\ + passage au contexte \end{matrix}

Interprétations:: $\begin{matrix} ⟦ x ⟧ = ensemble quelconque \\ ⟦ A \to B ⟧ = ⟦ B ⟧^{⟦ A ⟧} \\ Si x_{1} : C_{1}, \dots, x_{n} : C_{n} ⊢ M : A alors ⟦ M ⟧ : ⟦ C_{1} ⟧ \times \dots \times ⟦ C_{n} ⟧ ⟶ ⟦ A ⟧ \end{matrix}$

Exemples:

f : A \to A, x : A ⊢ f (f \underset{\in f v (f)}{\underset{⏟}{x}}) : A

⟦ f (f x) ⟧ : {\begin{cases} ⟦ A ⟧^{⟦ A ⟧} \times ⟦ A ⟧ & ⟶ ⟦ A ⟧ \\ (h, a) & \mapsto h (h (a)) \end{cases}

Γ, x : A ⊢ x : A

⟦ x ⟧_{Γ, x : A} ≝ {\begin{cases} ⟦ Γ ⟧ \times ⟦ A ⟧ & ⟶ ⟦ A ⟧ \\ (γ, a) & \mapsto a \end{cases}

\frac{Γ, x : A ⊢ M : B}{Γ ⊢ λ x . M : A \to B}

⟦ λ x . M ⟧_{Γ} ≝ {\begin{cases} ⟦ Γ ⟧ & ⟶ ⟦ B ⟧^{⟦ A ⟧} \\ γ & \mapsto {\begin{cases} ⟦ A ⟧ & ⟶ ⟦ B ⟧ \\ a & \mapsto ⟦ M ⟧_{Γ, x : A} (γ, a) \end{cases} \end{cases}

\frac{Γ ⊢ M : A \to B Γ ⊢ N : A}{Γ ⊢ M N : B}

⟦ M N ⟧_{Γ} ≝ {\begin{cases} ⟦ Γ ⟧ & ⟶ ⟦ B ⟧ \\ γ & \mapsto ⟦ M ⟧_{Γ} (⟦ N ⟧_{Γ} (γ)) \end{cases}

Système T

Pareil, avec l’interprétation en plus du “if then else”

Sytème F

On n’arrive pas à donner une sémantique ensembliste!

En $λ$ -calcul pur

\begin{matrix} ⟦ M ⟧_{x_{1}, \dots, x_{n}} : D^{n} ⟶ D \\ f v (M) \subseteq {x_{1}, \dots, x_{n}} \end{matrix}

Un $λ$ -terme clos est dans:

1 ⟶ D

Problème de cardinalité! Comme les $λ$ -abstractions sont des $λ$ -termes:

D^{D} ↪ D

Donc les théoriciens des modèles ont discrédité pendant longtemps le $λ$ -calcul en avançant qu’il n’a pas de modèles ensemblistes.

Mais arrive la logique catégorique (vision généralisée de la théorie des modèles): il n’y a aucune raison de se restreindre à la catégorie $S e t$ ! Il y a des tas d’autres catégories qui peuvent fournir des modèles!

⟶ Dana Scott: interprétation du $λ$ -caclul dans des treillis au début, puis des Complete Partial Orders (CPOs).

Laissez place à la Logique Catégorique

La sémantique “naïve” précédente peut être définie pour n’importe quelle catégorie cartésienne close (CCC)!

Catégories Cartésiennes Closes (CCC): Rappels de base

Produit $A, B \in 𝒞$ :: Limite du diagramme discret $A B$ , i.e. un triplet $(A \times B, π_{1} : A \times B ⟶ A, π_{2} : A \times B ⟶ B)$ avec $A \times B \in 𝒞$ tel que pour tout $(C, f : C ⟶ A, g : C ⟶ B)$ , le diagramme suivant commute:
$C g f ⟨ f, g ⟩ B A A \times B π_{1} π_{2}$
Objet terminal $1 \in 𝒞$ (produit 0-aire):: limite du diagramme vide; i.e. $𝒞 (A, 1)$ est un singleton pour tout $A \in 𝒞$
Catégorie cartésienne:: lorsqu’elle a tous les produits binaires et un objet terminal, i.e a tous les produits finis

Modulo l’axiome du choix (pour choisir le produit, qui n’est unique qu’à unique isomorphisme près), on a un bifoncteur:

\times : 𝒞 \times 𝒞 ⟶ 𝒞

Qui fait de $𝒞$ une catégorie monoïdale.

Adjonction

Si $F : 𝒞 ⟶ 𝒟, G : 𝒟 ⟶ 𝒞$ sont des foncteurs:

Adjonction à gauche $F ⊣ G$ :: s’il existe un isomorphisme naturel
$𝒟 (F A, B) ≃ 𝒞 (A, G B)$

Exemple: Construction libre

Les structures algébriques libres habituellement sont données par des adjoints à gauche de foncteurs d’oubli:

F ⊣ U

où

$F : S e t ⟶ G r p$ par exemple
$U : G r p ⟶ S e t$ est le foncteur d’oubli

L’adjonction dit qu’un morphisme de groupe entre le groupe libre et $G$ est exactement une fonction des générateurs vers le carrier set de $G$ :

G r p (F X, G) ≃ S e t (X, U G)

Clôture

Soit $𝒞$ une catégorie cartésienne. Soit $A \in 𝒞$ . On pose

R_{A} ≝ ∙ \times A : {\begin{cases} 𝒞 & ⟶ 𝒞 \\ Γ & \mapsto Γ \times A \end{cases}

On dit que $𝒞$ est close si pour tout $A \in 𝒞$ , $R_{A}$ a un adjoint à droite:

R_{A} = ∙ \times A ⊣ A \to ∙

i.e pour tous $A, B$ :

𝒞 (Γ \times A, B) ≃ 𝒞 (Γ, A \to B)

Exemples:

Sont une CCC:

$S e t$
$F i n S e t$ (ensembles finis)

Théorie de Lawvere

Théorie de Lawvere $𝒯$ :: catégorie cartésienne $𝒯$ telle qu’il existe $⋆ \in 𝒯$ tq:
$\forall A \in 𝒯, A ≃ ⋆^{n}$

Il s’agit d’une généralisation des théories équationnelles (qu’on rencontre en algèbre universelle). Les théories de Lawvere sont aussi appelées théories algébriques.

Exemple: Théorie des groupes

Soit $𝒢$ une catégorie cartésienne engendrée par $⋆$ et trois morphismes

$e : 1 ⟶ ⋆$
$m : ⋆^{2} ⟶ ⋆$
$n : ⋆ ⟶ ⋆$

avec la diagonale $δ ≝ ⟨ i d, i d ⟩$

⋆ \times (⋆ \times ⋆) ≃ (⋆ \times ⋆) \times ⋆ m \times i d i d \times m ⋆^{2} m ⋆^{2} m ⋆

1 \times ⋆ ≃ e \times i d ⋆ ⋆ \times 1 ≃ i d \times e ⋆^{2} m ⋆^{2} m

Plus: diagramme de l’inverse

Un modèle de $𝒯$ :: est un foncteur préservant les produits $M : 𝒯 ⟶ 𝒞$ , où $𝒞$ est une catégorie cartésienne close.

La donnée d’un tel foncteur correspond à la donnée de:

$M (⋆) \in 𝒞$

Ici:

un modèle $M : G ⟶ S e t$ de $𝒢$ est exactement un groupe
un modèle $M : G ⟶ T o p$ est un groupe topologique
Argument de Eckman-Hilton: un modèle $M : G ⟶ G r p$ est un groupe abélien
- de même: une catégorie monoïdale dans la catégorie des catégories monoïdales est une catégorie monoïdale symmétrique
- un monoïde dans la catégorie des monoïdes est un monoïde commutatif

Toute théorie équationnelle sans inégalité (donc pas les corps) peut être exprimée en termes de théories de Lawvere!

Ici, $⋆$ est une sorte. Mais on pourrait avoir plusieurs sortes:

Théories multi-sortée (à $r$ sortes):: pour tout $A \in 𝒯$ , il existe $n_{1}, \dots, n_{r}$ tels que
$A ≃ ⋆_{1}^{n_{1}} \times \dots \times ⋆_{r}^{n_{r}}$

Ex: avec une sorte pour les vecteurs, une pour les scalaires:

interprétation dans $S e t$ ⟶ espaces vectoriels
interprétation dans $T o p$ ⟶ espaces topologiques

Modèles du $λ$ -calcul simplement typé

La sémantique du $λ$ -calcul simplement typé peut être défini dans n’importe quelle CCC

C’est une sorte de “théorie de Lawvere” à l’ordre supérieur:

on a des générateurs et les produits finis (théorie de Lawvere)
et en plus: l’exponentielle
- l’adjonction est la règle de la déduction naturelle
  $\frac{Γ, A ⊢ B}{Γ ⊢ A \to B}$
la $β$ -réduction est l’équation
les $λ$ -termes sont les morphismes:
- un $λ$ -terme de type $A$ dont les variables libres sont dans $Γ$ est un morphisme $Γ ⟶ A$

Donc un modèle du $λ$ -calcul simplement typé est un foncteur

M : Λ_{S T} ⟶ 𝒞

préservant le produit et l’exponentielle.

Modèles du $λ$ -calcul pur

Pour avoir un modèle du $λ$ -calcul pur (non typé), il suffit de trouver une CCC $𝒞$ avec un objet $D \in 𝒞$ tq

D ⟶ D f D g

f ◃ g i.e g \circ f = i d_{D ⟶ D}

ce que l’on appelle une rétraction

On appelle alors $D$ un objet réflexif.

CPOs

Soit $(D, \leq)$ un ordre partiel, et $Δ \subseteq D$ .

$Δ$ est filtrant:: si $\forall x, y \in Δ . \exists z \in Δ, x, y \leq z$
Un ordre partiel complet (CPO):: est un ordre partiel $(D, \leq, ⊥)$ avec un plus petit élément $⊥$ et tel que tous les ensembles ensembles filtrants (directed set) ont un sup, dénoté par $\lor Δ$

NB: en topologie, les fonctions continues sont exactement celles qui préservent les limites de suites indexées par les ensembles filtrants.

Si toute fonction continue préserve les limites de suites, la réciproque n’est pas vraie: il ne suffit pas de préserver les limite de suites pour être continue. Les suites indexées par des ensembles filtrants est la bonne notion.

NB: “Domaines de Scott”: CPOs avec des propriétés en plus.

Dans la littérature, on appelle “domaine” un CPO avec des propriétés en plus (les espaces cohérents en sont un cas particulier).

On va les utiliser pour PCF (extension du $λ$ -calcul simplement typé Turing-complète).

Scott-continuité

Soient $D, E$ des cpos.

Une fonction $f : D ⟶ E$ est Scott-continue:: si elle préserve les sups d’ensembles filtrants

Pour tout $Δ \subseteq D$ filtrant:

f (Δ) ≝ {y \in E ∣ y = f (x), x \in Δ} est filtrant

⋁ f (Δ) = f (\lor Δ)

Catégorie des CPOs

On note CPO la catégorie des cpos et des fonctions continues.

Théorème (Scott):

CPO est une CCC.

De plus, elle admet un objet réflexif.

Share on

Twitter Facebook Google+ LinkedIn