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
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 29 Avr 2014 02:12
Message Re: Les logiques : notes en vrac
Peut‑être une différence qui distingue clairement la sémantique axiomatique ou la dénotationnelle de la sémantique opérationnelle…

Si j’écris par exemple 1/0 - 1/0, chacune des deux divisions ne peut être calculée, mais la différence peut l’être symboliquement, et le résultat me semble pouvoir être 0 (mais ça dépend probablement aussi de l’interprétation du résultat).

Sûrement que pour la sémantique opérationnelle, cette expression est toujours invalide, tandis qu’elle peut l’être pour la sémantique axiomatique ou la dénotationnelle.

Est‑ce ça la différence ? Ou peut‑être un exemple de différence et qu’il y en a d’autres…

Il faudra d’ailleurs que je poste un message dédié aux différentes formes de sémantiques, mais pas encore assez de matière pour le moment.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mar 24 Juin 2014 09:32
Message Re: Les logiques : notes en vrac
Un article qui essaie d’expliquer pourquoi la pratique des preuves formelles, qui auraient dut être vues comme d’une évidente nécessité depuis les débuts de l’informatique, ne se sont pas vu attribuées leurs places jusque maintenant. L’auteur suppose que la situation pourrait changer à l’avenir.

Lire : Formal methods start to add up again (computing.co.uk). Janvier 2004. Auteur non‑mentionné.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Mer 25 Juin 2014 08:31
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
  • […];
  • Sémantique, axiomatique vs dénotationnelle vs opérationnelle (axiomatic vs denotational vs operational semantic);
  • […].

Il y a encore plus de types de sémantiques que ça.

Programming Language Semantics (cs.ucf.edu) [PDF]. David A. Schmidt, Kansas State University, 2012.

Chapitre 6 a écrit : 
  • Axiomatic semantics: The meaning of a program as a property or specification in logic;
  • Denotational semantics: The meaning of a program as a compositional definition of a mathematical function from the program’s input data to its output data;
  • Fixed-point semantics: A denotational semantics where the meaning of a repetitive structure, like a loop or recursive procedure, is expressed as the smallest mathematical function that satisfies a recursively defined equation;
  • Natural semantics: A hybrid of operational and denotational semantics that shows computationsteps performed in a compositional manner. Also known as a “big‑step semantics;
  • Operational semantics: The meaning of a program as calculation of a trace of its computation steps on input data;
  • Strongest postcondition semantics: A variant of axiomatic semantics where a program and an input property are mapped to the strongest proposition that holds true of the program’s output;
  • Structural operational semantics: A variant of operational semantics where computation steps are performed only within prespecified contexts. Also known as a “small‑step semantics;
  • Weakest precondition semantics: A variant of axiomatic semantics where a program and an output property are mapped to the weakest proposition that is necessary of the program’s input to make the output property hold true.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 26 Juin 2014 08:37
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Il y a encore plus de types de sémantiques que ça.

Apparemment, des types de sémantiques par domaines ou par logiques.

Deux autres, spécifiques à la logique du second ordre : sémantique standard et sémantique de Henkin.

La logique du premier ordre, n’a qu’une sémantique, la sémantique standard.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
zen
Modératrice
Avatar de l’utilisateur
  • Genre : Fille
  • Age : 55
  • Localisation : Un pied dans l'eau et un sur le mont.
  • Messages : 11010
Jeu 26 Juin 2014 18:26
Message Re: Les logiques : notes en vrac
J’y crois pas
A chaque fois que je passe par ici je me demande si tu parles français.
A chaque fois que je passe par ici je tire la même tête J’y crois pas et je repars.
Profil
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Jeu 26 Juin 2014 20:15
Message Re: Les logiques : notes en vrac
zen a écrit : 
A chaque fois que je passe par ici je me demande si tu parles français.
A chaque fois que je passe par ici je tire la même tête J’y crois pas et je repars.

Tout n’est pas encore clair pour moi non‑plus Oops, n’a fait une bêtise .

J’essaie de baliser un sujet. Je le fais sur le forum, parce que c’est pas plus inapproprié que de prendre des notes tout seul dans un fichier texte, et aussi au cas où ça intéresse quelques rares gens de passage, qui pourraient aussi peut‑être vouloir faire remarquer des erreurs.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 30 Juin 2014 09:41
Message Re: Les logiques : notes en vrac
Ce sujet qui essaie de baliser le vaste thème de la logique, appliquée à l’informatique et aux preuves de fiabilité des logiciels, suppose à priori, que l’usage de démonstrations qu’une implémentation satisfait une spécification, est une bonne chose.

Ci‑dessous, un article qui met en question cet à priori. Il le fait néanmoins en se posant des questions seulement sur le rapport qualité / cout, et non‑pas en mettant en question le bénéfice de s’assurer par des démonstrations, un bénéfice que l’auteur de la question juge indiscutable… il s’interroge donc seulement sur le cout, cependant aussi sur les — pressenties faibles — opportunités d’adoption de cette manière de concevoir les logiciels.

On the — Alleged — Value of Proof for Assurance (lambda-the-ultimate.org). Mars 2010.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 30 Juin 2014 21:24
Message Re: Les logiques : notes en vrac
Il a surtout été question de HOL, à cause de la correspondance de Curry‑Howard, dont découle directement cette logique (HOL, c’est typiquement un modèle du lambda calcul simplement typé). Mais ce n’est pas la seule, il existe le Calcul des Construction (Calculus of Construction — CoC), sur lequel repose le système de démonstration Coq.

Deux documents intéressant établissant une relation et une comparaison des deux. Le premier compare les systèmes HOL en général et le système Coq. Le second, discute d’une interprétation de HOL dans Coq.

Je me demande par ailleurs si on peut aussi interpréter Coq dans HOL, ou si Coq est plus expressif que HOL sans tenir compte des aspects pratiques (les types dépendants par exemple, pratiques, et non directement disponibles avec HOL). J’essaierai d’en savoir plus à ce sujet, plus tard.

A comparative study of Coq and HOL (kar.kent.ac.uk) [PDF]. Vincent Zammit. 2009.

Interpreting HOL in the Calculus of Constructions (people.uleth.ca) [PDF]. Jonathan P. Seldin. 2004.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 30 Juin 2014 21:58
Message Re: Les logiques : notes en vrac
Interestingly, il semble exister deux versions de la logique intuitionniste : la logique intuitionniste « normale », la version dite « forte », et une version Russe de la logique intuitionniste, semblant être moins fiable.

Je le tiens d’un commentaire à cette question : How true are theorems proved by Coq? (mathoverflow.net). Mars 2011.

Commentaire à la question a écrit : 
As far as I have been taught, Coq proofs are pretty much the best proofs you can get: they just require intuitionistic logic in the strong sense (not the Russian one). […]

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Ric
Débateur
Débateur
Avatar de l’utilisateur
  • Genre : Garçon
  • Age : 71
  • Localisation : la Gaume, région de la Lorraine belge
  • Messages : 1730
Mar 1 Juil 2014 16:56
Message Re: Les logiques : notes en vrac
Sincèrement Ô Image,

J'ai essayé de suivre mais je suis largué !

J'avais eu bien difficile il y a quelques années comprendre
les bases de la logique booléenne, à ce jour soit 15 ans plus
tard, non seulement je ne m'en souviens que très peu mais
j'ai grand mal à comprendre, que dis-je. . . je n'arrive pas
du tout à comprendre ce que tu as écrit dans les pages
précédentes, pardonnes-moi, mon quotient intellectuel est
vraiment trop bas pour suivre. Rougi

Image
....Je suis de là-bas !
Profil