Les logiques : notes en vrac

Une série d’articles de blog sur la théorie des catégories, appliquée à l’informatique : Category theory for programmers (bartoszmilewski.com), Bartosz Milewski, 2014.

C’est en plusieurs pages. Si la première page est longue, ce n’est pas parce que tout y est, c’est parce que chaque page se termine par une discussions dans les commentaires.

Il semble que ce qui est appelé kind, est le type d’un type.

Au cas où, attention à ne pas comprendre « imprédicatif » comme « inductif ».

Une proposition, c ’est un prédicat sans variable libre ou dont toutes les variables sont liées à un quantificateur : Quantification — forming propositions from predicates (cs.odu.edu).

Je dis « ou », parce que bien les deux points de vue donnent généralement une vision identique, il y a une ambiguïté sur la qualification d’un prédicat ne contenant que des constantes. Est‑ce un prédicat ou une proposition ? Il n’y a pas de variable libre, donc c’est une proposition, mais il n’y a pas de variable liées non‑plus, donc c’est un prédicat. Ce cas particulier pourrait s’appeler expression constante, mais ce serait encore ambiguë dans certains autres contexts.

Je me demande s’il y a un lien entre proposition et imprédicativité.

Les types algébriques, n’ont pas de quantificateurs.

L’axiome du choix et l’axiome de l’infini, ne sont pas considérés comme des axiomes purement logiques ; ils ne valent pas par leur forme (leur écriture) mais par leur contenu (ils sont une vue, une interprétation), c’est à dire qu’il ne sont pas purement abstraits. Ils sont pourtant assez incontournables …

C’est expliqué dans la vidéo ci‑dessous, qui au passage, rappel comment la logique est le fondement des mathématiques et non‑pas un branche des mathématiques.

Crisis in the foundation of mathematics — PBS Infinite Series — 2017

HOL est une extension de la STT ; plutôt extensions au pluriel, car il existe plusieurs HOL.

Pour l’HOL la plus fondamentale, on passe de la théorie des types simples — STT — à HOL, en ajoutant à STT, l’égalité, c’est à dire la possibilité de poser l’égalité entre deux termes. L’égalité ne peut pas être posée dans le lambda calcul avec les types simples, c’est une extension de ce lambda calcul, et cette extension, donne l’HOL basique.

Quand on parle d’HOL à notre époque, c’est implicitement une HOL avec une extension supplémentaire : le typage polymorphique. L’ajout en plus du typage polymorphique, donne la variante d’HOL implémentée dans un logiciel nommé HOL4, ou même HOL tout‑court, tellement cette implémentation est considérée comme standard. Attention : HOL4 est un logiciel, HOL est une logique, bien qu’il y ait un lien entre les deux, il faut éviter d’appeler HOL4, HOL, pour ne pas entretenir la confusion.

Note : SML a un typage polymorphique, mais il ne permet pas de poser l’égalité.
 
Une autre extension encore sur la même trajectoire, donne une version d’HOl qui n’est plus nommée HOL (alors qu’elle le pourrait) : les types dépendants. L’ajout des types dépendants encore en plus, à l’HOL, donne la logique de Coq ou Twelf par exemple. Mais cette extension se fait elle‑même de manière diverse, et n’est pas standard bien que sujet de beaucoup d’intérêt.

Le format OpenTheory, pour la représentation standard de preuves en HOL, est pour une HOL du deuxième type décrit ici, c’est à dire avec le typage polymorphique. Il n’existe pas (ou je l’ignore), d’équivalent d’OpenTheory pour les HOL avec types dépendants ; que les implémentations de cette extension soit nettement divergentes ou même expérimentales, y est probablement pour quelque chose.

Le lambda calcul simplement typé et la théorie des types simples, ne sont pas équivalentes. Le lambda calcul simplement typé est une théorie des types, mais moins expressives que la théorie des types simples.

Avec un système de déduction à types polymorphes, comme l’est l’HOL courant, les preuves sont des expressions booléenne, et pour la démontrer, il faut montrer qu’elle se réduit à vrai.

Avec un système de déduction à types dépendants, comme l’est le calcul des constructions ou la théorie intuitionniste des types, une preuve est un type, et pour la démontrer, il faut montrer que le type est habité.