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 : 17500
Dim 27 Juil 2014 19:28
Message Re: Les logiques : notes en vrac
J’ajoute au message bibliographique, ce lien : Mathematical proof and computer science (uchicago.edu) [PDF]. Sneha Popley, Texas Christian University, Mai 2010.

C’est une perle. En 15 pages (c’est court, comparé aux documents typiques sur le sujet), et sans notations trop obscures, ce document présente les plus grandes lignes du paysage actuel, les plus importants systèmes de déduction et modèles des domaines fondamentaux utilisés dans les preuves mathématiques appliquées à l’informatique, et les plus importantes mises en œuvre concrètes, pour se faire une idée des points forts et des points faibles de chaque.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Lun 28 Juil 2014 01:23
Message Re: Les logiques : notes en vrac
Une phrase à creuser, à propos de la complétude d’une théorie (au sens général).

Citation : 
[…] complete in the sense that semantic truth implies provability […]


Je l’ai trouvé dans une discussion sur l’arithmétique de Peano du premier‑ordre versus l’arithmétique de Peano du second‑ordre. Quelqu’un disait que celle du premier ordre est complète, mais pas celle du second (d’après Gödel), et en discutant du sens du qualificatif « complète » dans ce contexte, quelqu’un(e) a eu la phrase que je cite.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Lun 28 Juil 2014 23:34
Message Re: Les logiques : notes en vrac
Bien en arrière dans ce sujet, il était dit que les systèmes à la Hilbert, sont peu commodes, car comprenant un grand nombres d’axiomes et un petit nombre de règles de déduction, comparé aux favoris des systèmes de déductions contemporains, partant d’un petit nombre d’axiomes et d’un un‑peu plus grand nombre de règles de déduction, formant un système dont certaines caractéristiques sont démontrées, pour ensuite plutôt démontrer un grand nombre d’axiomes au lieu de les poser et admettre à priori.

Je ne sais pas quel cas Hilbert faisait des caractéristiques de son système, comme la correction (soundness), alors je ne sais pas si c’est lié : il semble qu’il y avait un autre problème encore avec le programme de Hilbert (j’imagine, lié à sa manière de penser les systèmes de déduction). Je n’en sais pas plus, mais Gödel a mis fin à une illusion que se faisait Hilbert.

Proof Assistants and The Rise of Type Theory: Circa 1912 ‑ 2012 (cs.cmu.edu) [PDF]. Robert L. Constable, Cornell University, Mars 2012.

Robert L. Constable a écrit : 
Gödel thus showed that PA is consistent iff HA is consistent. This kind of result led him to think that Hilbert’s program was doomed.

Traduction a écrit : 
Gödel à ainsi démontré que la PA est cohérence ssi l’HA est cohérente. Ce genre de résultat l’a amené à se dire que le programme de Hilbert était anéanti.


Rappel. PA signifie Peano Arithmetic, HA signifie Heyting Arithmetic, et ssi signifie si‑et‑seulement‑si.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mar 29 Juil 2014 00:11
Message Re: Les logiques : notes en vrac
J’ajoute au premier message, « théorie des domaines ». Ça a l’air important, autant en théorie qu’en pratique.

Du même lien que précédemment, Proof Assistants and The Rise of Type Theory: Circa 1912 ‑ 2012 (cs.cmu.edu) [PDF]. Robert L. Constable, Cornell University, Mars 2012.

Robert L. Constable a écrit : 
What else can we do with MetaPRL? We can also formulate incompatible theories in logical frameworks. For example, in Nuprl, our theory of partial recursive functions using bar types is incompatible with classical mathematics whereas most of Nuprl is compatible. So MetaPRL can isolated those results, which are a constructive version of Scott’s domain theory, related to Edinburgh LCF.

Traduction a écrit : 
Que pouvons nous faire encore, avec MetaPRL ? Nous pouvons aussi formuler des théories incompatibles dans des cadriciels logiques. Par exemple, dans Nuprl, notre des fonctions partielles récursives utilisant des types brutes, est incompatibles avec les mathématiques classiques, avec lesquelles Nuprl est cependant compatibles. MetaPRL peut donc isoler ces résultats, qui sont des versions constructive de la théorie des domaines, de Scott, lié à la LCF d’Édimbourg.


Remarque. LCF signifie Logic of Computable Functions.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mar 29 Juil 2014 02:07
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Je ne sais pas quel cas Hilbert faisait des caractéristiques de son système, comme la correction (soundness), […]

Il en faisait un certain cas quand‑même :

De la même source.

Robert L. Constable a écrit : 
Formal axiomatic systems were the key to showing the consistency of mathematics according to Hilbert […]

Ça peut se comprendre comme « la cohérence, des mathématiques selon Hilbert » ou comme « la cohérence des mathématiques, selon Hilbert » et ça n’a pas le même sens, mais je crois quand‑même que c’est la seconde interprétation qui est la bonne et qu’il en faisait cas.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mar 29 Juil 2014 02:34
Message Re: Les logiques : notes en vrac
Une note importante sur l’intention de la logique intuitionniste de pas intégrer le tiers‑exclus.

De la même source.

Robert L. Constable a écrit : 
Denying the validity of P v ¬P is a consequence of constructive semantics, not a definition of intuitionism or constructivity.

Traduction a écrit : 
La non‑reconnaissance de la validité de P v ¬P est une conséquence de la sémantique constructiviste, ce n’est pas par définition de l’intuitionnisme ou du constructivisme.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mar 29 Juil 2014 16:34
Message Re: Les logiques : notes en vrac
Intuitionnisme et constructivisme, semble bien être synonymes.

Constructive Type Theory and Interactive Theorem Proving (jaist.ac.jp) [PDF]. 2005.

Citation : 
Now it is the contention of the intuitionists (or the constructivists, I shall use these terms synonymously) […]


— 2014-09-30. ’tite correction ici : Re: Les logiques : notes en vrac.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mar 29 Juil 2014 19:54
Message Re: Les logiques : notes en vrac
Les symboles suivants sont présentés, et désambiguïsés (waw, le mot Hahaha! ) :

  • → Unicode : U+2191, rightwards arrow
  • ↦ Unicode : U+21A6, rightwards arrow from bar
  • ⇒ Unicode : U+21D2, rightwards double arrow
  • ⇝ Unicode : U+21DD, rightwards squiggle arrow
  • ⊂ Unicode : U+2282, subset of
  • ⊃ Unicode : U+2283, superset of
  • ⊢ Unicode : U+22A2, right tack / turnstile
  • ⊧ Unicode : U+22A7, models
  • ⊨ Unicode : U+22A8, true
  • ⊭ Unicode : U+22AD, not true
  • ⟶ Unicode : U+27F6, long rightwards arrow
  • ⟹ Unicode : U+27F9, long rightwards double arrow
  • ⟼ Unicode : U+27FC, long rightwards arrow from bar
  • ⟿ Unicode : U+U27FF, long rightwards squiggle arrow

Les noms et numéros Unicode des caractères, ont été déterminé à l’aide de ShapeCatcher.com et Unicode Character Search (fileformat.info).

Message en cours d’édition, pas encore terminé
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Mer 17 Sep 2014 13:22
Message Re: Les logiques : notes en vrac
Les axiomes du lambda‑calcul dans un diaporama présentant les grandes lignes de l’inférence de types. C’est de troisième main, ces axiomes sont repris et repris… une source parmi d’autres.

An Introduction to Type Inference (cs.columbia.edu) [PDF], Alfred V. Aho, Novembre 2011.

À la diapositive № 5.

Citation : 
Axioms of lambda calculus
  • α‑equivalence: change of bound variable name, e.g., λx.E = λ y.E[y/x]
  • β‑equivalence: application of function to arguments, e.g., (λx.E)y = E[y/x]
  • η‑equivalence: elimination of redundant lambda‑abstractions, e.g., if x is bound in E, λx.(Ex) = E

Traduction a écrit : 
Axiomes du lambda‑calcul
  • α‑équivalence : renommage de variable liée, ex. λx.E = λ y.E[y/x]
  • β‑équivalence: application de fonction à des arguments, ex. (λx.E)y = E[y/x]
  • η‑équivalence: élimination de lambda‑abstractions redondantes, ex. si x est liée dans E, λx.(Ex) = E


C’est simplifié, au moins pour le premier axiome, qui nécessite de s’assurer qu’une variable liée n’est pas renommée avec le nom d’un variable pré‑existante dans l’expression. Pour plus de détails, voir le sujet dans le sous‑forum sur SML, Le lambda‑calcul, purement et en général.

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 : 17500
Mer 17 Sep 2014 16:05
Message Re: Les logiques : notes en vrac
Peter Aczel's topics (cs.man.ac.uk)

Peter Aczel a écrit : 
This topic originated at the turn of the century with Russell's attempt to resolve his paradox through his “vicious Circle Principle” that “no totality can contain members defined in terms of itself”.

Traduction a écrit : 
Ce sujet a pris naissance au tournant du siècle avec la tentative de Russel de résoudre son paradoxe qui par son « principe du cercle vicieux » fait que « aucune totalité ne peut être constituée d’élément définis en termes d’elle‑même ».

Quand il parle du tournant du siècle, il parle de celui du ⅩⅩᵉ siècle, pas de celui récent du ⅩⅪᵉ siècle, dans lequel nous sommes.

Il y a sûrement une relation entre cette citation de Russel (« aucune totalité ne peut être constituée d’élément définis en termes d’elle‑même »), et le traitement de la récursivité dans le lambda‑calcul typé. Ce serait intéressant de connaitre explicitement la réponse que Hindley et Milner ont donné à cette question dans leur système de typage.

À noter aussi, la page que je cite commence par ce petit titre : “Impredicativity”. L’ imprédicativité, … une notion à ajouter à la liste du premier message.

Image
Hibou57

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