Les logiques : notes en vrac

Essentiel, toujours implicite, utile à dire explicitement :

Le lambda calcul lui‑même, est un système déductif (comme tous les langages). Sa version non‑typée est incohérente (comme tous les langages non‑typés ou faiblement typés), sa version typé est cohérente.

Comme dit précédemment, le lambda calcul a en fait plusieurs versions typés.

La lettre gamma majuscule, Γ, est parfois utilisée pour signifier un ensemble de prémisses ou suppositions ; la lettre delta majuscule, Δ, est parfois utilisée pour signifier un ensemble de théorèmes découlant des prémisses, comme si Γ était en haut sur un séquent et Δ en bas sur le séquent.

Essentiel, toujours implicite, utile à dire explicitement :

Même s’il est moins célèbre, le paradoxe du Russel est autant important que les deux théorèmes de Gödel.

Essentiel, toujours implicite, utile à dire explicitement :

Une preuve est une évaluation d’une expression, typiquement une réduction.

Ceci signifie qu’un calcul symbolique, un calcul exacte (ex. sans approximation numérique), sont aussi des preuves.

Un livre référence, sur le lambda calcul non‑typé : “ Lambda Calculus: its Syntax and Semantics ”, par Henk Barendregt. La première édition est de 1984, il y en a eu d’autres, la dernière en 1987, je crois.

La notation de la substitution de a par b dans e, varie selon les auteurs, de ces différentes manières :

• E[b/a]
• [b/a]E
• E[a := b]
• E[a ↦ b]
• [a ↦ b]E

Le lambda calcul simplement typé, n’est pas Turing complet ; sa forme non‑typée, l’est, mais elle est inconsistante.

C’est Church aussi, qui a inventé le lambda calcul simplement typé, pas seulement le non‑typé. Il a inventé la forme typée après qu’il ait été montré que la version non‑typé est inconsistante.

Le lambda calcul non‑typé est inconsistant, parce qu’il permet d’exprimer des choses qui n’existent pas, sous forme de récursion infinie. Le lambda calcul avec un typage à la Hindley‑Milner, qui donne un type a toutes les expressions, est inconsistant, parce qu’il permet de donner un type non‑habité à une expression. Un type non‑habité, c’est un type de quelque chose qui n’existe pas. Typiquement, un type non‑habité, est comme avec le lambda calcul non‑typé, une récursion qui ne se termine jamais. Le typage à la Hindley‑Milner permet de poser des choses indémontrables, alors qu’un type est censé, dans la correspondance de Curry‑Howard, être l’affirmation d’une chose vraie, existante.

D’après ce que je comprend, c’est la seule cause d’inconsistance dans le lambda calcul (permettre de poser une chose dont il est impossible de démontrer qu’elle est vraie, c’est à dire poser une chose fausse). Le lambda calcul simplement typé ne souffre pas de ce problème, mais il n’est pas Turing Complet et ne permet pas d’exprimer la récursion. On peut cependant prouver qu’une récursion se termine, en utilisant une logique propre à cette finalité.

Avant de considérer que le type d’une fonction est vrai (le type de la fonction, le “ arrow type ”, pas le type renvoyé par la fonction), il faudrait d’abord définir une fonction de ce type et démontrer qu’elle se termine. Dit autrement, avant d’utiliser un type dans une inférence logique, il faudrait d’abord démontrer que le type est habité. Dit autrement encore, un type comme prémisse, devrait toujours lui‑même avoir comme prémisse, une instance de ce type ; ce qui n’est pas contradiction si on défini cette instance sans poser le type comme prémisse à ce moment là.

J’insiste sur le type d’une fonction, parce qu’en pratique, c’est avec seulement les types de fonctions que ce problème se pose.

Tout ceci vaut au moins pour tout langage dans la sémantique est exprimée en termes de lambda calcul.

Le lambda calcul avec les types dépendants (les vrais, pas des pseudos types dépendants) ne permet pas de formuler des types non‑habités, sans avoir besoin de prouver qu’une fonction de ce type se termine. Mais je trouve que les types dépendants ne sont pas commodes, qu’il est plus facile de s’exprimer avec la sémantique opérationnelle. En plus, les vrais types dépendants sont apparemment internals à implémenter dans un langage ; en fait, on ne peut pas supprimer les types à la compilation, c’est à dire que ce sont des langages typés qui ne peuvent être au mieux que aussi peu efficaces que les langages à typage dynamique.

Parce que typiquement, on peut toujours écrire une constante, même si elle d’un type structuré.

Cependant, si on étend les types en leur ajoutant des axiomes vérifiés par les valeurs de ce type (des axiomes attachés aux types), alors le problème se pose avec tous les types, pas seulement avec les types arrow. Par exemple si on posait un type en le définissant comme étant un entier, en ajoutant l’axiome que la valeur est supérieure à 5 et inférieure à 2, on poserait un type qui ne peut pas être habité, et il faudrait exposer une constante de ce type, pour montrer que ce type est habité.

Les types dépendants, sont essentiellement des types indexés. Un exemple simple d’index, est un entier. Pour cette raison, l’exemple est souvent pris, d’un type liste dont le type est indexé par la longueur. Mais en pratique, cette catégorisation est sans intérêt, et on s’intéressera plutôt à un type liste dont la longueur est compris dans un interval. Plus encore, si on prend l’exemple d’une chaîne de caractère dont tous les mots commence par une majuscule, l’index est beaucoup moins évident et sûrement pas supporté par des languages supportant des pseudos types dépendants. Sans compter que si on catégorise parfois ce type par sa longueur, on devra avoir deux index, en fait autant d’indexe que de caractéristiques possibles, même si elles ne pas toujours importantes.

Les types dépendants sont puristes, mais pas commodes. Ils sont intéressants dans le cadre de la théorie des types, mais moins intéressants dans la cadre d’un langage, surtout quand il existe d’autres moyens de faire ce que permettent les types dépendants, comme attacher un axiome à un type ou démontrer qu’une fonction se termine.