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 : 17807
Dim 28 Sep 2014 22:44
Message Re: Les logiques : notes en vrac
Un message de retour sur la relation entre logique et typage.

Même si le typage, surtout lorsqu’il est simple ou en général peu expressif, montre des limites pour exprimer des démonstrations ou des invariants précis, il permet au moins d’éviter des erreurs basiques; ceci pourrait être un bilan pratique des usages du typage simple dans les langages simplement typés (les plus courants).

Il fait de même avec la formulation de question en logique et dans les mathématiques, en ne permettant peut‑être pas de répondre à toutes les questions, mais en prévenant au moins de formuler des questions n’ayant pas de sens.

C’est ce que résume l’introduction de cet article sur les types dépendants (un typage plus expressif que le typage simple) : In Praise of Dependent Types (golem.ph.utexas.edu), Mike Shulman, Mars 2010.

Mike Shulman a écrit : 
I’ve written before about “structural” foundations for mathematics, which can also be thought of as “typed” foundations, in the sense that every object comes with a type, and typing restrictions prevent us from even asking certain nonsensical questions. For instance, whether the cyclic group of order 17 is equal to the square root of 2 is such a nonsensical question, since the first is a group while the second is a real number, and only things of the same type can be compared for equality.

Traduction a écrit : 
J’ai précédemment écrit à propos de fondations « structurelles » pour les mathématiques, qui peuvent aussi être comprises comme des fondations « typées », dans le sens ou chaque objet a son type, et que les règles de typage nous gardent de poser des questions insensées. Par exemple, se demander si le groupe cyclique d’ordre 17 est égale à la racine carrée de 2, est un exemple de question sans aucun sens, vu que le premier est un groupe tandis que le second est un nombre réel, et que seulement des choses du même type peuvent être dites égales.

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 : 17807
Dim 28 Sep 2014 23:42
Message Re: Les logiques : notes en vrac
De la même source, plus loin dans la page, une description intuitive et correcte de ce qu’est un type dépendant. Il prend un exemple issu du langage naturel.

Mike Shulman a écrit : 
Dependent types are also everywhere in natural language. One standard example is that for any month m, there is a type (or set) D(m) of the days in that month. Since different months have different numbers of days, the cardinality of D(m) is different for different m. Of course, because of leap years, D actually depends not only on m but also on a year y. David gave a couple of nice examples here of the need for dependent types in expressing quantifiers in everyday language.

Traduction a écrit : 
Les types dépendants sont aussi présents partout dans le langage naturel. Un exemple standard est celui est que à tous mois m, est associé un type (ou ensemble) D(m) des jours dans le mois. Comme les différents mois ont différents nombres de jours, le cardinal de D(m) est différent pour les différents m. Bien sûr, en conséquence des années bissextile, D ne dépend pas seulement de m, mais aussi de l’année y. David a donné un ensemble de beaux exemples ici, de l’utilité des types dépendants pour exprimer les quantificateurs du langage de tous les jours.

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 : 17807
Lun 29 Sep 2014 01:58
Message Re: Les logiques : notes en vrac
Différence et similitudes à éclaircir : CIC (Calculus of Inductive Constructions) vs CTT (Computational Type Theory) vs ITT (Intuitionistic Type Theory).

Tous semble liés, mais suffisamment différents. Et aussi, quel est le rapport de chacune de ses théorie avec les types dépendants ?

Ajouté à la liste du premier message.

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 : 17807
Lun 29 Sep 2014 04:33
Message Re: Les logiques : notes en vrac
HOL a un problème avec le polymorphisme ? C’est ce que dit ce papier, et le phénomène est connu sous le nom de « paradoxe de Girard ».

(In)consistency of extensions of Higher Order Logic and Type Theory (cs.ru.nl) [PDF], Herman Geuvers, date inconnue, Université de Radboud.

Herman Geuvers a écrit : 
It is well-known, due to the work of Girard and Coquand, that adding polymorphic domains to higher order logic, HOL, or its type theoretic variant λHOL, renders the logic inconsistent. This is known as Girard’s paradox. But there is also a another presentation of higher order logic, in its type theoretic variant called λPREDω, to which polymorphic domains can be added safely. Both λHOL and λPREDω are well-known type systems and in this paper we study why λHOL with polymorphic domains is inconsistent and why and λPREDω with polymorphic domains remains consistent. We do this by describing a simple model for the latter and we show why this can not be a model of the first.

Traduction a écrit : 
Il est connu, depuis les travaux de Girard et Coquand, qu’étendre aux domaines du polymorphisme, la logique d’ordre supérieur, HOL, ou sa variante de la théorie des types, λHOL, rend cette logique incohérente. Ce phénomène est connu comme paradoxe de Girard. Mais il existe une autre forme de logique d’ordre supérieur, dans sa variante de la théorie des types, nommée λPREDω, à laquelle les domaines du polymorphisme peuvent être ajoutés de manière fiable. Autant λHOL que λPREDω sont des systèmes de types bien connus et dans ce document nous étudions la raison pour laquelle λHOL avec les domaines du polymorphisme est incohérente et pourquoi λPREDω avec les domaines du polymorphisme, reste cohérente. Nous le faisons en décrivant un modèle simple pour cette dernière et nous montrons pourquoi il ne peut pas être un modèle de cette première.


Mais alors, HOL et sa théorie des types simples, c’est en fait λHOL ?

Ce papier est ajouté au message bibliographique de la page 2.

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 : 17807
Mar 30 Sep 2014 00:17
Message Re: Les logiques : notes en vrac
En rapport avec le message sur la relation entre logique et typage, une autre citation, issue d’une présentation de la “Computational Type Theory”, « Théorie des Types Algorithmiques » (?) [1].

Computational type theory (scholarpedia.org), Robert L. Constable.

Robert L. Constable a écrit : 
Computational type theory, like all type theories, is related to a foundational theory for mathematics originating with Bertrand Russell (Russell, 1908 a,b) as an attempt to deal with certain contradictions such as Russell's Paradox about the set R of all sets that are not members of themselves, denoted {x | x ∉ x} , a circular definition. The paradox arises from asking whether R belongs to R . Russell's theory of logical types was designed to prevent so called vicious circles in definitions which led to contradictions in mathematical reasoning.

Traduction a écrit : 
La Théorie des Types Algorithmiques, comme toutes les théories des types, est liée à une théorie des fondements des mathématiques, prenant naissance avec Bertrand Russel (Russel, 1908 a,b) comme tentative de travailler certaines contradictions, telle que le Paradoxe de Russel, à propos de l’ensemble R de tous les ensembles qui ne sont pas membres d’eux‑mêmes, noté {x | x ∉ x}, une définition circulaire. Le paradoxe apparait quand on veut savoir si l’ensemble R appartient à R. La théorie des types logique, de Russel, fût conçu de manière à prévenir les dits cercles vicieux dans des définitions qui aboutissent à des contradictions dans les raisonnements mathématiques.


[1]: je ne connais aucune traduction de ce terme en français, et je ne trouve rien de mieux que d’inventer la traduction qui me semble convenir le mieux, « Théorie des Types Algorithmiques », en espérant qu’elle ne sera pas trop source de confusions.

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 : 17807
Mar 30 Sep 2014 03:33
Message Re: Les logiques : notes en vrac
De la même source, une remarque sur l’impossibilité d’avoir un type de base unique; avec une référence inattendue, à Aristote.

Robert L. Constable a écrit : 
In PM and STT, types are used to render the notions of class and propositional function free from vicious circles. A type is the domain of significance of a propositional function, i.e. those objects that the proposition is about, and that domain can not include the proposition itself. What Russell believed is that there can't be a single universal type of all meaningful objects on which propositions are defined because that type would include the propositions being defined, creating a vicious circle. Instead, the universe must be divided into categories, Aristotle's terminology, or types.

Traduction a écrit : 
Dans PM et la STT, les types sont utilisés pour exprimer les notions de classes de fonctions propositionnelles, exemptes de tout cercle vicieux. Un type est le domaine de pertinence de la signification d’une fonction propositionnelle, c‑à‑d. les éléments sur lesquels porte la proposition, et ce domaine ne peut inclure la proposition elle‑même. Ce que Russel a crut, c’est qu’il ne peut pas exister un unique type universel de tous les objets ayant un sens, à propos desquels des propositions sont définies, car ce type devrait inclure la proposition ainsi définie, aboutissant à un cercle vicieux. Au lieu de ça, l’univers doit être divisé en catégories, une terminologie d’Aristote, ou des types.



Notes : PM, signifie Principia Mathematica (ceux de A.‑N. Whitehead et B. Russell en 1910) et STT signifie “Simple Type Theory”, « Théorie des Types Simples » (celle de HOL, entre autres). Le mot « univers » ne se comprend pas comme au sens courant; ici, c’est le monde d’un modèle mathématique, l’ensemble des tous les éléments qui le constitue.

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 : 17807
Mar 30 Sep 2014 05:20
Message Re: Les logiques : notes en vrac
Encore de la même source, une citation triplement intéressante. Elle aborde une chose introduite précédemment comme à définir, les notions de logique prédicative et logique imprédicative; un axiome célèbre (mais ne faisant pas l’unanimité) qui n’avait encore pas été introduit ici, l’axiome de réductibilité; et un exemple qui pourra sembler en contradiction avec ce qui a été dit sur le paradoxe de Russel, en des quantificateurs s’appliquant à ce qu’ils définissent.

Robert L. Constable a écrit : 
Principia Mathematica was also designed to demonstrate that mathematics could be reduced to logic, say to truth values and higher-order functions over them – specifically to predicative logic which avoids the concept of all functions or all propositions. This is one reason that PM did not start with a primitive notion of natural numbers nor with a notion of individuals as in HOL, namely, Russell and Whitehead wanted to derive mathematical concepts such as natural numbers and real numbers from more basic logical concepts. Unfortunately, the core PM foundation is inadequate for classical mathematics, even for natural numbers, without an axiom of reducibility in the typing rules, which is a way to introduce so called impredicative notions, those whose definition quantifies over a collection including the concept being defined.

Traduction a écrit : 
Principia Mathematica a aussi été conçu pour démontrer que les mathématiques pouvaient se ramener à la logique, c’est‑à‑dire à des valeurs de vérité et des fonctions d’ordre supérieur sur ces premières — spécifiquement à la logique prédicative qui permet d’éviter le concept du tout‑fonction ou du tout‑proposition. C’est une raison pour laquelle PM ne démarrât pas avec une notion primitive des nombres naturels, ni avec une notion d’individuels comme en HOL; nommément, Russel et Whitehead voulurent dériver des concepts mathématiques comme les nombres naturels et les nombres réels, à partir de concepts logiques plus basiques. Malencontreusement, le cœur de fondation de PM, est inapproprié aux mathématiques classiques, même aux nombres naturels, sans un axiome de réductibilité dans les règles de typage, une manière d’introduire les notions dites imprédicatives, celles dont la définition quantifie dans une collection incluant le concept ainsi défini.


J’en profite aussi pour ajouter la notion d’individuels à la liste du premier message.

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 : 17807
Mar 30 Sep 2014 06:40
Message Re: Les logiques : notes en vrac
De deux autres sources, et racontant la même chose que la précédente citation. C’est comme dans le précédent message, sur le souhait premier d’une prédicativité, pourtant finalement l’introduction de l’imprédicativité par l’axiome de réductibilité.

Axiom of reducibility (oxfordreference.com)

Oxford Reference a écrit : 
Axiom introduced by Russell and Whitehead in Principia Mathematica. In that system propositional functions are sorted into levels, as part of the ramified theory of types. The axiom says that for any function at any level there exists a formally equivalent function at the first level. The axiom is needed to allow the construction of elementary mathematics, in particular to certify the principle of mathematical induction. Its effect, as Ramsey pointed out, was largely to nullify the point of introducing different orders of functions.

Traduction a écrit : 
Axiome introduit par Russel et Whitehead dans Principia Mathematica. Dans ce système, les fonctions propositionnelles sont rangées en niveaux, selon la théorie ramifiée des types. Cet axiome dit que pour toute fonction à n’importe quel niveau, il existe une fonction strictement équivalente au premier niveau. Cet axiome est nécessaire pour rendre possible la construction des mathématiques élémentaires, en particulier pour certifier le principe de l’induction mathématique. Elle eût, comme l’a fait remarquer Ramsey, pour effet de largement rendre caduque l’idée d’introduire différents degrés pour les fonctions.


C’est plus explicite dans la définition de l’Encyclopaedia Britannica, même si elle est moins complète (plus complète dans la version payante).

Axiom of reducibility (global.britannica.com)

Encyclopaedia Britannica a écrit : 
Russell and Whitehead tried unsuccessfully to base mathematics on a predicative type theory; but, though reluctant, they had to introduce an additional axiom, the axiom of reducibility, which rendered their enterprise impredicative after all.

Traduction a écrit : 
Russel et Whitehead tentèrent en vain de baser les mathématique sur une théorie prédicative des types; mais, bien que réticents, ils ont dut introduire un axiome additionnel, l’axiome de réductibilité, qui rendît leur ouvrage imprédicatif, finalement.

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 : 17807
Mar 30 Sep 2014 07:31
Message Re: Les logiques : notes en vrac
Un élément de catégorisation des systèmes logiques, semble être : ceux dans lesquels les entiers naturels sont une notion dérivée d’une construction d’objets plus élémentaires; et ceux dans lesquels les entiers naturels sont une notion primitive.

Il n’est pas sûr que la première catégorie soit meilleure que la seconde, malgré son apparence séduisante autant que malgré qu’elle soit la plus courante.

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 : 17807
Mar 30 Sep 2014 09:23
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
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) […]


Pas tout à fait quand‑même.

À l’origine de la logique intuitionniste, il y a Brouwer (qu’il n’y a pas besoin de présenter), et à l’origine de la logique constructiviste, il y a Bishop (je crois, ou au moins il a joué un rôle important). Ça fait déjà une petite différence, par l’origine, mais qui n’implique rien pour la nature de ces deux logiques.

La différence de nature semble être : l’intuitionnisme est à propos des fondements… relevant de l’intuition pour Brouwer, et le constructivisme est à propos de la logique appliquée, qui implique que la caractère calculable en pratique des propositions logiques est un fondement, selon Bishop.

La logique constructiviste est intuitionniste, Bishop ayant approuvé l’intuitionnisme qui pré‑existait. Comme l’intuitionnisme a rapidement approuvé le constructivisme, les deux ont fini par se confondre et à ne se distinguer que pour l’histoire et les cas où n’est abordé que l’un ou l’autre des deux fondamentaux — fondements relevant de l’intuition ou fondements nécessitant la calculabilité pratique — ou les quelques points de désaccords entre Brouwer et Bishop, comme la nature des nombres réels — notion de continuum pour Brouwer, notion de calcul dérivée des entiers naturels et des rationnels (une fonction tendant vers une valeur), pour Bishop.

Ça semble être ça, en résumé.

Image
Hibou57

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