Les logiques : notes en vrac

Par exemple un langage avec lequel il est nécessaire de démontrer que les fonctions se terminent, cependant que ce langage est dit à types dépendants, ce langage n’est pas vraiment à types dépendants, parce qu’avec de vrais types dépendants, il est impossible d’écrire le type d’une fonction qui ne se termine jamais.

Il existe une version relationnelle de HOL, dans ce contexte, pour la distinguer, celle dont on parle ici est appelée la version fonctionnelle de HOL.

La documentation sur le format SMT‑Lib mentionne cette différence :

Comme son nom l’indique, le lambda calcul non‑typé n’est pas typé. Mais je me demandais quand‑même à quoi pourrait correspondre une erreur de type, dans l’évaluation d’une expression en LCNT.

Je l’imagine comme ça : l’expression n’est pas réductible ou ne l’est pas jusqu’au bout. Par exemple, si on applique une opération sur des entiers, à deux caractères, la somme par exemple, alors l’expression ne sera pas réductible et restera l’expression d’une somme de deux caractères. C’est à dire que s’il n’y a pas d’erreur de type, le type serait comme la forme normale attendue d’une expression. En disant cela, je n’exclus pas que cette forme normale soit encore réductible.

Du coup, ça définie aussi ce qu’est un type : la forme normale attendue pour une expression.

On peut noter qu’une chose peut avoir plusieurs représentations, donc plusieurs forme, et qu’un type n’est alors pas purement sémantique, il n’est qu’une question de forme. Il y a nécessairement quelque chose en commun, entre ces différentes formes. Qui dit réduire à une chose en commun, dit abstraction, ce qui amène à naturellement à l’idée d’abstraction de plusieurs types, c’est à dire à l’idée de type abstrait.

En résumé : un type est une forme non‑purement significative, un type abstrait est purement significatif, et une erreur de type, c’est une impossibilité à réduire à la forme normale définie par un type.

Quand je dis plus haut que la forme normale définie par un type, peut éventuellement être encore réductible (ce qui signifie qu’il ne faut pas toujours chercher à réduire jusqu’au bout), je pense par exemple à un type dont la forme serait l’application d’une fonction. Une telle forme qui vaut alors pour elle‑même, est encore réductible, même s’il arrivait que ce soit l’expression d’une application qui ne se termine jamais, raison de plus pour dire qu’il ne faut plus réduire dès qu’on arrive à la forme normale définie par le type. Ce qui amène à la question de choisir le bon chemin pour la réduction, s’il arrive qu’il y a plusieurs solutions possibles.

Il existe cependant un type spécial de fonction dans certains langages, qui est le constructeur de type. Les applications de ces fonctions là, sont irréductibles : l’expression vaut pour elle‑même, jamais au delà.

Si un type est une forme normale d’une expression, rien de plus, alors on peut comprendre que la sémantique du LCT soit celle du LCNT.

Un cas tordu serait celui où une expression est déjà sous une forme trop réduite. Par exemple si la forme normale attendue est l’expression d’une somme de deux entier et qu’on a un entier, par exemple si la forme normale attendue est de la forme x + y et qu’on a 2, alors il faut marcher en arrière, par exemple créer 0 + 2 à partir de 2. Dans ce cas là aussi, il y a plusieurs solutions.

Parfois même, plusieurs formes en même temps. Par exemple une recherche dichotomique dans un tableau à une dimension, c’est comme voir le tableau à une dimension, comme un arbre aussi, en même temps.

Il semble que l’application d’une fonction, telle‑quelle, non‑réduite, n’est pas considérée comme une valeur. Je me demande pourquoi et je me demande si ça poserait un problème logique.

En tous cas, il faut lire certains précédents messages en notant ce point, parce que je supposais que l’expression de l’application d’une fonction, est une valeur.

Ça me surprend que ça ne le soit pas, j’ai toujours supposé que toute expression écrite, dans le lambda calcul, est une valeur, c’est à dire que je n’ai jamais distinguer les deux.

Il ne faut pas confondre “ type soundness ” et “ logical soundness ”. Un système de typage peut être cohérent, mais il peut être incohérent quand il est utilisé comme système logique.

Dans la terminologie HOL, “ Γ ⊢ p ” signifie « p a été prouvé sous Γ » tandis qu’en logique plus en général, la même expression signifie « p peut être prouvé sous Γ ».

Par convention, souvent :

• Γ désigne un ensemble d’hypothèses (peut être vide).
• Δ désigne un second ensemble d’hypothèses (peut être vide).
• tₙ désigne un terme.
• xₙ désigne une variable (substituable à un terme)
• γₙ ou τₙ désigne un type.
• αₙ désigne une variable de type (substituable à un type).