Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Ven 8 Sep 2017 16:08
Message Re: Les logiques : notes en vrac
Il semble exister deux grandes approches dans la formalisation et les preuves de fonctionnement des logiciels, et on pourrait leur donner des noms connus : bottom-up et top‑dow. Top‑down, serait l’approche de Z, VDM, B, et d’autres, c’est l’approche qui défini des valeurs et des relations entre des valeurs et les opérations sur les valeurs (voir plus loin) ; cette approche est dite orienté modèle. Bottum‑up, serait l’approche de CASL et peut‑être d’autres, c’est l’approche qui défini des constructeurs avec lesquels on construit des valeurs, certains constructeurs sans argument pouvant être assimilés à des valeurs ; cette approche est dite algébrique.

Les deux approches semblent portées sur les états.

Pour expliquer ce qui distingue l’approche orientée valeur et l’approche orienté constructeur, on peut prendre l’exemple des entiers naturels. L’approche orientée valeurs va définir un type de donné pour les nombres, déclarer des opérations sur ces nombres, comme l’addition, la soustraction, la multiplication, la division, et définira des relations comme “ sub(add(a, b), b) = a ” dont il faudra démontrer qu’elles sont respectées par une implémentation. L’approche orientée constructeurs, va définir des fonctions créant des nombres, comme le constructeur du zéro et le constructeur successeur, de l’arithmétique de Peano et interférera des propriétés comme “ pred(succ(n)) = n ” à partir desquelles elle composera des opérations respectant certaines relations. Si je ne dis pas de bêtises plus haut, il faut souligner « définira des relations dont il faudra démontrer … » et « interférera des propriétés […] à partir desquelles elle composera … ».

Z, VDM et B, sont tellement orientés types et opérations, qu’il existe une extension objet de VDM. C’est probablement la raison pour laquelle elles ont eu du succès auprès des auteur et éditeurs utilisant des langages courants : Z a été utilisée avec le C, VDM a été utilisée avec Modula‑2 et B a été utilisée avec Ada. Une autre raison, est que ces méthodes me semble mieux s’accommoder d’un pré‑existant dont on déclarera les propriétés pour ensuite démontrer qu’il les a bien, tandis que l’autre approche me semble plus appropriés pour concevoir à partir de rien, bien que les deux approches soient capable des deux, même si pas aussi directement.

Cette distinction ne tient pas compte d’autres caractéristiques, comme le fait d’utiliser une logique du premier ordre ou une logique d’ordre variable comme HOL.

Cette distinction ne dit pas que certains domaines applications ne peuvent pas être approchés avec l’une ou l’autre méthode, et il faut souligner « méthode », parce que c’est une différence de méthode.

Personnellement, je crois préférer l’approche top‑down avec les spécifications informelles (mais néanmoins normatives), pour en tirer un formalisme orienté constructeur à partir duquel j’aurais une approche bottom‑up. Je le dis, non‑pas pour dire que c’est le mieux — c’est une affinité personnelle — mais seulement pour dire que bottom‑up n’exclus par top‑down par ailleurs, et réciproquement.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Mer 25 Oct 2017 22:59
Message Re: Les logiques : notes en vrac
Les types inductifs et les types algébriques sont désignés chacun avec leur nom, mais en pratique, les types inductifs sont aussi algébriques, sinon ils ne seraient pas expressifs, et les types algébriques seraient assez limités. On peut parler de types inductifs tout court avec la supposition implicite qu’ils sont algébriques.

Les types co‑inductifs et inductifs, peuvent être, eux, concrètement désignés séparément, même si les premiers sont une extension des seconds.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Jeu 26 Oct 2017 03:14
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Dans HOL4 (hol-theorem-prover.org), un assistant de démonstration, on dispose de huit primitives pour créer des théorèmes dérivés et donc des preuves :

  • ASSUME (introduction d’une supposition);
  • REFL (réflexivité);
  • BETA_CONV (béta‑conversion);
  • SUBST (substitution);
  • ABS (abstraction);
  • INST_TYPE (instanciation d’un type);
  • DISCH (décharge de supposition);
  • MP (modus‑ponem).

On peut reconnaitre des similitudes avec les dix règles d’inférence de HOL‑Light et les dix règles d’inférence de OpenTheory, tout en notant qu’il n’y en a ici que huit, au lieu de dix.

Je commenterai plus, plus tard, en ajoutant seulement pour le moment que quatre de ces huit règles, sont considérées comme des axiomes du système de déduction, et ces quatre axiomes, sont en fait eux‑mêmes une généralisation d’une logique de base.

On peut retrouver ces théorèmes fondamentaux ici, suivis de règles d’inférence dérivées mais néanmoins considérées comme primitives : FinalThm (hol-theorem-prover.org).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Jeu 26 Oct 2017 19:07
Message Re: Les logiques : notes en vrac
Quand dans un texte parlant de logique, il est question d’aller du général au particulier (“ general to specific ” en Anglais) ou le sens inverse, il faut comprendre le général comme étant le fondamental et le particulier comme étant une des conséquences de ce qui est fondamental. Par « général », il ne faut pas comprendre les observations en général, c’est le contraire, il faut comprendre ce qui est universelle et fondamentale, qui en est la cause.

On parle de raisonnement déductif ou de déduire, quand on part d’un ensemble d’axiomes le plus souvent pas trop grand, pour aller vers des conséquences, le plus souvent plus nombreuses.

On parle de raisonnement inductif ou d’induire, quand on part de phénomènes posés ou observés, pour tenter de trouver ce qui en est la cause, le fonde, le plus souvent, plus fondamental que ce qui est observé.

Ces deux nuances valent autant en Anglais qu’en français.

Si je ne me trompe pas, on peut dire que la physique fondamentale a une démarche inductive, tandis que les sciences appliquées ont une démarche déductive.

On parle aussi de définition inductive, mais jamais de définition déductive, on parle plutôt dans ce cas, de définition axiomatique, bien que en pratique les définitions inductives reposent aussi sur des axiomes d’une manière ou d’une autre (souvent générés par des règles, automatiquement dans le cas d’un logiciel assistant de preuve).

Par exemple dire « un nombre peut être le produit de la somme de deux nombres », est une définition inductive, parce que le premier nombre est une conséquence des deux nombres qui en sont des causes. La définition « nombre = zéro | successeur(nombre) » est une définition inductive, zéro et « successeur(nombre) » étant des causes. Dans cette notation, la flèche de l’implication irait de la droite vers la gauche. On le comprend mieux si on remarque qu’avec la notation fonctionnelle, on écrirait par exemple « successeur(nombre) => nombre », qui exprime bien que « successeur(nombre) » est une cause et le résultat, une conséquence.

Une définition axiomatique pourrait par exemple être « x + zéro = x », qui pourrait être posée sans même définir ni zéro ni l’opération « + », mais permettrait pourtant de déduire que « a + zéro = a ».

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Jeu 26 Oct 2017 22:30
Message Re: Les logiques : notes en vrac
Edsger W. Dijkstra a écrit : 
Program testing can be used to show the presenceof bugs, but never to show their absence!

Traduction a écrit : 
Tester les logiciels convient pour montrer des bugs, mais ne convient pas pour montrer qu’il n’y en a pas !


Edsger W. Dijkstra était mathématicien et informaticien.

Attention : ça n’implique pas qu’ont peut se passer de tests quand on utilise des preuves formelles. Les tests peuvent permettre de déceler des erreurs de spécification comme par exemple des cas d’inconsistance de Pollack (Pollack inconsistency), des erreurs d’intégration ou même d’utilisabilité (ex. ergonomie), qui sont inaccessibles aux preuves formelles. Cependant, la grande majorité des bugs ne rentrent pas dans ces catégories, pourraient être évités avec des méthodes formelles.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Ven 27 Oct 2017 05:10
Message Re: Les logiques : notes en vrac
Le type des entiers pour HOL4, est num , pour SML c’est int. S’il y a des similitudes entre HOL4 et SML, il y a aussi de nécessaires différences. Les entiers de HOL4 ne sont pas bornés comme ils sont théoriques, ceux de SML le sont comme ils sont concrets. Le type bool au contraire, est le même pour les deux.

D’autres différences sont juste des différences de notation.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Ven 27 Oct 2017 05:15
Message Re: Les logiques : notes en vrac
Une variable libre en HOL, n’est pas nécessairement une variable non‑contrainte. Une variable libre est libre dans le sens de nous échapper, nous échapper dans le sens où on ne peut pas la renommer parce qu’elle a une origine hors de l’expression à laquelle on s’intéresse. Au contraire, avec une variable liée, on a sa déclaration, le point où elle est liée, on peut la renommer.

Si deux expression peut être rendue textuellement égale par un renommage sous la condition plus haut, elles sont dites alpha‑équivalentes.

C’est bien l’alpha‑équivalence (α‑équivalence) introduite dans le message du 17 Septembre 2014 : Re: Les logiques : notes en vrac.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Ven 27 Oct 2017 06:16
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
⊢ s’applique à la syntaxe, et ⊨ s’applique à la sémantique. C’est déjà une différence claire entre les deux. Tous deux sont des conséquences : conséquence syntaxique pour le ⊢ et conséquence sémantique pour le ⊨. L’implication ⇒ (parfois notée ⊃ ou encore parfois assez mal notée →), est un opérateur du calcul des propositions.

[…]

⊢ est parfois aussi utilisé pour dire « démontrable » ou « démontré », les deux ne devant pas être confondus. Le sens est l’un ou l’autre selon l’ouvrage ou le logiciel ou le langage.

Le point commun est le démontrable, ce qui est démontré étant obligatoirement démontrable ; et démontrable sans se soucier de savoir si c’est sémantiquement ou syntaxiquement, comme il peut aussi être utilisé pour dire démontré ou démontrable, sémantiquement.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Ven 27 Oct 2017 23:59
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

On parle de raisonnement déductif ou de déduire, quand on part d’un ensemble d’axiomes le plus souvent pas trop grand, pour aller vers des conséquences, le plus souvent plus nombreuses.

On parle de raisonnement inductif ou d’induire, quand on part de phénomènes posés ou observés, pour tenter de trouver ce qui en est la cause, le fonde, le plus souvent, plus fondamental que ce qui est observé.

[…]

Parallèlement, on parle de preuve en chainage avant (forward proof) quand on va des causes aux conséquences, ou de preuve en chainage arrière (backward proof) quand on va des conséquences aux causes.

En pratique, les deux peuvent être combinées.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
En ligne
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 15684
Dim 29 Oct 2017 12:00
Message Re: Les logiques : notes en vrac
En pratique, les démonstrations en chaînage arrière se confondent avec le découpage du but final ou des buts intermédiaires, en plusieurs sous‑buts. Par exemple “ A ∧ B ” sera démontré en démontrant individuellement A et B (un théorème permettant de revenir au but initial à partir de ces deux sous‑buts) ; les buts simples, non‑décomposables se démontrant au contraire en chaînage avant, par application directe de théorèmes et de règles d’inférence.

Le découpage d’un but en buts intermédiaires, s’appel une tactique  (tactic) ; ces tactiques reçoivent typiquement un nom, car les mêmes reviennent souvent. En particulier, une réécriture (rewrite), est aussi une tactique.

La combinaison d’étapes de démonstration en chaînage avant par application directe de théorèmes, s’appelle une automatisation (automation).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
cron