Les logiques : notes en vrac

La différence entre un théorème et une démonstration, c’est que la démonstration est un théorème potentiel, et ne peut être « convertie » en théorème qu’après validation.

Le terme « théorème » est malheureusement parfois utilisé quand il s’agit d’axiome.

Une citation importante, de Program verification using Hoare logic (inf.ed.ac.uk), Petros Papapanagiotou, 2013-2016.



Il existe en effet et malheureusement, une croyance selon laquelle, quand on utilise des preuves de fonctionnement, on a plus besoin de tests. Cette croyance est répandue chez les gens qui n’ont pas d’expérience dans les preuves ou qui n’ont pas l’intuition de ce qu’elles sont.

Une spécification peut signifier autre chose que ce que l’humain croit comprendre. L’inconsistance de Pollack en est un peu un exemple particulier. Une spécification peut être mal posée ou mal comprise, même si sa formalisation est bien comprise. Une spécification peut être partielle, ne pas couvrir tout le programme ou toute la réalité pratique.

Trois concepts à aborder :

• Program analysis (analyse de programme).
• Model checking (vérification de modèle).
• Abstract interpretation (interprétation abstraite).

Et aussi, clarifier la différence entre analyse de programme et vérification de modèle, parce que je le comprends comme si la vérification de modèle était un cas particulier d’analyse de programme, alors que les deux semble être distinctes.

Les deux grandes familles de logiques les plus courantes, sont les logiques provenant de la théorie des ensembles et les logiques provenant de la théorie des types.

Je crois que la logique classique tient surtout de la première, la théorie des ensembles. Ce qui me le fait penser, c’est que je me souviens qu’à l’école primaire, une certaine importance était donnée à l’instruction de la notion d’ensemble et d’opération sur les ensembles. Une autre chose, est que dans la théorie des ensembles, les connecteurs logiques sont des choses distinctes de la notion d’ensemble, tandis que dans la théorie des types, les connecteurs logiques sont des types et dans la culture populaire, les connecteurs logiques appartiennent à une domaine autre que ce sur quoi on les applique.

Un livre intéressant, surnommé « la Bible » dans certains milieux, est “ The lambda calculus, its syntax and semantics ” de H.P. Barendregt. Mais il est cher, alors mieux vaut chercher dans l’occasion. Faire attention aussi à l’édition, comme il en existe plusieurs éditions.

Attention aussi au fait que ce livre semble surtout traiter du lambda calcul non‑typé.

Un wiki sur les mathématiques, la physique et la philosophie, qui a des entrées concernant les logiques : ncatlab.org.

Ces termes anglophones, semblent être synonymes :

• Formal system ;
• Logical calculi ;
• Logical system.

Un système logique (je préfère cette expression) est composé de :

• Un alphabet, qui est un ensemble fini de symboles.
• Une grammaire, définissant comment construire une formule bien formée (il y en a typiquement une infinité).
• Un ensemble de règles d’inférence qui sont souvent elles‑mêmes des formules valides selon la grammaire, mais pas toujours.
• Un ensemble d’axiomes qui sont eux‑mêmes des formules valides selon la grammaire (un axiome est souvent comme une règle d’inférence sans prémisse, mais pas toujours).

Un système logique a les propriétés (vérifiées ou non) suivantes :

• Consistency (cohérence) ;
• Validity (validité) ;
• Completeness (complétude) ;
• Soundness (solidité ou correction).

Pour comprendre HOL, je recommande cette lecture : Higher‑order logic (tuwien.ac.at) [PDF], Stefan Hetzl, 2017. Il explique simplement le passage de la logique du premier ordre à la logique d’ordres supérieurs.

Elle est aussi ajoutée à la bibliographie à la deuxième page de ce sujet.

Il y a deux définitions de l’égalité entre deux fonctions dans le lambda calcul utilisé comme système déductif. La première, dite en intention, tient pour égales deux fonctions qui mises sous formes canoniques, ont la même structure. La deuxième, dite en extension, tient pour égales deux fonctions qui établissent la même correspondance (leur application).

Les deux, en intention et en extension, ne sont pas nécessairement équivalente, elles peuvent différer selon le typage (non‑typé, simplement typé, polymorphique, etc).

En Anglais ont dit Intensional lambda calculus et Extensional lambda calculus.