Les logiques : notes en vrac

La théorie des types simples (STT), n’est pas intuitionniste / constructiviste, elle admet le tiers‑exclus, la preuve par contradiction.

Il faudrait savoir comment et si c’est toujours le cas (existent‑ils plusieurs théories des types simples ou une seule ?).

À la fois dans la ligne du précédent message et en complément du message concluant qu’il existe finalement des différences entre logique intuitionniste et logique constructiviste.

La théorie des types intuitionnistes (ITT) de Martin-Löf, admet tous les algorithmes, même ceux qui ne se terminent pas. Ça n’est certainement pas constructiviste.

Là aussi, il faudrait voir comment et si c’est toujours le cas.

Une citation texte quasi‑fondateur, “The seven virtues of simple type theory”, « Les sept vertus de la théorie des types simples ». C’est au début, sur la seconde page imprimé (j’ai fait imprimer les 15 pages pour l’étudier dans de bonnes conditions).



La première phrase de la partie surlignée, me fait penser à cette histoire de système à la Hilbert. La seconde partie, suggère l’une des principales vertus de la théorie des types simples (et de la logique d’ordre supérieure, HOL) : l’expressivité et une expression plus naturelle.

Un autre formalisme à présenter et débroussailler plus tard : Homotopy Type Theory, ou HoTT. Je viens d’en apprendre l’existence sur un Usenet dédié au langage ATS.

Le titre d’un article m’intrigue :

Whither compositionality: declarative vs. imperative? (lambda-the-ultimate.org), Décembre 2014.

Habituellement, c’est la question « prédicatif vs imprédicatif » qui est posée, et poser la question « déclaratif vs imprédicatif », me laisse l’impression de dire que déclaratif et prédicatif, sont la même chose. Est‑ce que ça l’est ?

Une question à creuser…

Il n’existe pas un, mais deux lambda‑cube :

• The Lambda‑SKI Cube (rbjones.com)
• Barendregt's Lambda Cube (rbjones.com)

Le second, celui de Barendregt, est aussi celui du calcul des constructions, de Coquand. C’est ce qui explique que les logiques dérivées du calcul des constructions soit si bien placé sur ce cube, qui établie une sorte de hiérarchie entre les logiques. Le lambda‑cube n’est en effet pas totalement neutre.

Le premier, porte dans son nom les trois lettres SKI, qui me rappel quelque chose, mais impossible de me souvenir quoi, je me souviens seulement que c’est important.

Un oubli que je ne corrige que maintenant.

Qui dit preuve des propriétés de quelque chose, dit nécessité de la couverture exhaustive des cas possibles sous lesquelles cette chose peut se présenter.

Concernant cette couverture, si on ne veut pas faire d’erreur d’interprétation, il ne faudrait normalement jamais oublier qu’avec les logiques, on est dans ce qui s’appelle l’hypothèse du monde clos (un exemple imagé est donné peu après). C’est une expression utilisée littéralement, et elle avait été rapidement mentionnée dans le sujet des références sur Prolog : Prolog — Les références partielles.

L’hypothèse du monde clos, ça signifie que quand on interprète les conclusions d’un système logique, il faut s’assurer que de toutes les choses essentielles à l’interprétation, aucune n’est ignorée par le système logique.

Un exemple imagé pour comprendre : si vous disposer d’un ensemble de connaissance portant sur la couleur de différentes fleurs, et que vous utilisez un système logique pour poser des questions du style « cette fleur est‑elle de telle couleur ? » et que vous poser la question à propos d’un fleur qui ne fait pas parti des connaissances, certains systèmes logiques vont sembler répondre « Non », alors qu’en fait ils ne peuvent répondre ni « Oui » ni « Non », car la fleur pour laquelle la question est posée, ne fait pas partie des connaissances. C’est cela l’hypothèse du monde clos : pour un système logique, s’il n’a pas de connaissance sur une chose, alors cette chose n’existe pas, même si elle existe en dehors de son monde.

La logique est souvent abordée comme une chose qui répond par « Oui » ou « Non » ou encore par « Vrai » ou « Faux ». C’est une erreur d’interprétation, et dans la plupart des cas (avis personnel), seules les réponses « Oui » ou « Vrai » sont valables, et le « Non » ou « Faux », devraient parfois — mais pas toujours — s’interpréter comme « Je ne sais pas » ou « Je ne peux pas répondre ».

Une conséquence suggérée est qu’il est nécessaire de définir ce que sont logiquement le « Vrai » et le « Faux » ou le « Oui » et le « Non », c’est à dire, qu’est‑ce que l’on interprète de cette manière et comment on aboutit à cette interprétation. L’interprétation comme « Vrai » et « Faux » peut être parfois triviale et même directe, mais pas toujours. Comme remarque personnelle, j’ajoute que c’est surtout avec l’interprétation comme « Non » ou « Faux » que des écueils peuvent se présenter, et un exemple a été donné plus haut ; les interprétations comme « Oui » ou « Vrai » me semblent poser moins de problèmes, mais c’est peut‑être seulement que j’ignore des cas qui me laisseraient avec une autre idée.

Un PDF en Anglais sur la logique dans le langage naturel :
Logic_and_Natural_Language.pdf (umass.edu), Novembre 2005.

J’ajoute cette entrée à la bibliographie de la page 2.

A survey into the Curry‑Howard isomorphism & type systems (ccs.neu.edu) [PDF], Phillip Mates, 2011.

L’isomorphisme de Curry‑Howard, pour les débutant(e)s : The Curry-Howard isomorphism for dummies (rocq.inria.fr) [PDF], Pierre‑Marie Pedrot, Février 2015.

Et à la bibliographie, j’ajoute : Proofs and types (paultaylor.eu) [PDF], Jean‑Yves Girard, Paul Taylor et Yves Lafont (ces deux derniers, pour les annexes), 1989‑2003.

Ce dernier, il est chouette, il couvre tout : déduction naturelle, Cyrry‑Howard, System F, et types linéaires, pour ne dire que les grandes lignes.