| Auteur | Message |
|---|---|
|
Administrateur
 |
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. |
|
|
|
Administrateur
|
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é. |
|
|
|
|
Administrateur
|
Hibou a écrit :
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 :
|
|
|
|
|
Administrateur
|
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. |
|
|
|
|
Modératrice
 |
 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 et je repars.
|
|
|
|
|
Administrateur
|
zen a écrit : A chaque fois que je passe par ici je me demande si tu parles français. Tout n’est pas encore clair pour moi non‑plus  .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. |
|
|
|
|
Administrateur
|
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. |
|
|
|
|
Administrateur
|
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. |
|
|
|
|
Administrateur
|
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). […] |
|
|
|
|
Débateur
 |
Sincèrement Ô
 ,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. 
|
|
|
|
