Galliblog

The Gallinette blog

Quésaco - Relations Logiques

By Guilhem Jaber, Étienne Miquey.

On 4 November 2019.

Définitions

On se place dans le cadre du $\lambda$-calcul simplement typé, où l'ensemble des types $T$ est défini par:

$$ \sigma,\tau ::= o \mid \sigma \to \tau$$

On définit une structure applicative par :

$$ \mathcal{A} \triangleq \big((A^\sigma)_{\sigma\in T},(\textrm{App}^\sigma)_{\sigma,\tau\in T}\big)$$

où $A^\sigma$ est un ensemble et $\textrm{App}^{\sigma,\tau} : A^{\sigma\to\tau}\to (A^\sigma \to A^\tau)$.

Pour se faire une idée, en sémantique dénotationelle on aurait une interprétation $\llbracket \cdot \rrbracket$ des types (par exemple dans une catégorie) et $\mathrm{App}$ serait alors l'application définie dans la catégorie.

Définition (Relation logique). Une relation logique $n$-aire sur des structures applicatives $ \mathcal{A}_1$,$\ldots$,$\mathcal{A}_n$ est la donnée d'une famille de relation $\mathcal{R}\triangleq (R^\sigma)_{\sigma\in T}$ telle que :

  1. $R^\sigma \subseteq A^\sigma_1\times\dots\times A^\sigma_n$, avec $A^\sigma_i\in\mathcal{A}_i$
  2. $R^{\sigma\to\tau}(f_1,\dots,f_n)$ ssi pour tout $x_1\in A^\sigma_1,\dots,x_n\in A^\sigma_n$, $R^\sigma(x_1,\dots,x_n)$ implique $R^\tau(\textrm{App}^{\sigma,\tau}(f_1,x_1),\dots,\textrm{App}^{\sigma,\tau}(f_n,x_n))$

Intuitivement, 1. correspond à "R est une relation" tandis que 2. exprime "R est logique".

Remarque : cela signifie en pratique qu'une relation logique est entièrement définie par l'interprétation des types atomiques.

Exemple. Dans le cas unaire pour l'application donnée par la syntaxe $\lambda$-calcul, cela signifie simplement que :

$$ R^{\sigma\to\tau}(t)\Leftrightarrow \forall u\in A^\sigma. (R^\sigma(u) \Rightarrow R^\tau(t\,u)) $$

Propriétés & applications

Le lemme fondamental des relations logiques est :

Lemme. Si un terme est bien typé, il est dans la diagonale de la relation correspondant à son type.

Définissabilité

À l'origine, les relations logiques auraient été introduites pour étudier le problème de définissabilité, à savoir : étant donnée une interprétation $ \llbracket \cdot \rrbracket^\sigma:\mathrm{Term}^\sigma \to A^\sigma $, si $d\in A^\sigma$, existe-t-il un terme $M$ de type $\sigma$ tel que $ \llbracket M \rrbracket^\sigma = d $ ?

Adéquation calculatoire

À l'aide des relation logique, on peut montrer que:

Si $\llbracket M \rrbracket = n \in \mathbb{N}$ alors $M \to^* n$.

(Idée : on définit $(u,M)\in R^{\mathrm{Nat}}$ ssi $u=\bot$ ou $u\in \mathbb{N}$ et $M \to^* u$.)

Preuves de normalisation

La définition des candidats de réducibilité, permettant de prouver par exemple la normalisation de système F [1], peut être exprimée à l'aide d'une relation logique unaire. De façon intéressante, on observe que la quantification du second-ordre $\forall \alpha.\tau$ est interprétée sémantiquement en substituant $\alpha$ par toutes les relations possibles (et non par tous les types possibles, ce qui serait mal-fondé).

Plus généralement, on peut utiliser les relations logiques pour des preuves de normalisation de différents calculs.

Équivalence contextuelle

On peut, à l'aide de relations logiques, capturer la notion d'équivalence contextuelle.

Appel par valeur

Enfin, on peut considérer le cas de calculs en appel par valeurs en utilisant une définition par biorthogonalité.




Références

[1] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.