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 : 15514
Mer 1 Oct 2014 06:44
Message Re: Les logiques : notes en vrac
La théorie des types simples (STT), n’est pas intuitionniste / constructiviste, elle admet le tiers‑exclus, la preuve par contradiction.

Il faudrait savoir comment et si c’est toujours le cas (existent‑ils plusieurs théories des types simples ou une seule ?).

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 : 15514
Mer 1 Oct 2014 09:02
Message Re: Les logiques : notes en vrac
À la fois dans la ligne du précédent message et en complément du message concluant qu’il existe finalement des différences entre logique intuitionniste et logique constructiviste.

La théorie des types intuitionnistes (ITT) de Martin-Löf, admet tous les algorithmes, même ceux qui ne se terminent pas. Ça n’est certainement pas constructiviste.

Là aussi, il faudrait voir comment et si c’est toujours le cas.

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 : 15514
Mar 23 Déc 2014 22:39
Message Re: Les logiques : notes en vrac
Une citation texte quasi‑fondateur, “The seven virtues of simple type theory”, « Les sept vertus de la théorie des types simples ». C’est au début, sur la seconde page imprimé (j’ai fait imprimer les 15 pages pour l’étudier dans de bonnes conditions).

William M. Farmer a écrit : 
First order logic is certainly an effective logic for theory, but it is an awkward logic for practice. There is little built‑in support for reasoning about higher‑order objects such as sets and functions in first‑order logic. As a result, many basic mathematical concepts, such as transitive closure of a relation and the completeness principle for the real numbers, cannot be expressed n first‑order logic directly. The overhead of formalizing basic mathematics like abstract algebra and calculus in first‑order logic is quite high: one has to start with a sophisticated theory of set or functions. Moreover, mathematical statements that are succinct in informal practice, often become verbose and unwieldy when expressed in first‑order logic because first order‑logic lacks an abstraction mechanism for building predicates and functions and a definite description mechanism for specifying values. Mathematicians almost never use first‑order logic to actually do mathematics; the benefits fall well short of justifying the pain and tedium that is involved in developing mathematical ideas in first‑order logic.


La première phrase de la partie surlignée, me fait penser à cette histoire de système à la Hilbert. La seconde partie, suggère l’une des principales vertus de la théorie des types simples (et de la logique d’ordre supérieure, HOL) : l’expressivité et une expression plus naturelle.

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 : 15514
Ven 6 Fév 2015 13:31
Message Re: Les logiques : notes en vrac
Un autre formalisme à présenter et débroussailler plus tard : Homotopy Type Theory, ou HoTT. Je viens d’en apprendre l’existence sur un Usenet dédié au langage ATS.

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 : 15514
Jeu 12 Fév 2015 13:01
Message Re: Les logiques : notes en vrac
Le titre d’un article m’intrigue :

Whither compositionality: declarative vs. imperative? (lambda-the-ultimate.org), Décembre 2014.

Habituellement, c’est la question « prédicatif vs imprédicatif » qui est posée, et poser la question « déclaratif vs imprédicatif », me laisse l’impression de dire que déclaratif et prédicatif, sont la même chose. Est‑ce que ça l’est ?

Une question à creuser…

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 : 15514
Jeu 12 Fév 2015 13:17
Message Re: Les logiques : notes en vrac
Il n’existe pas un, mais deux lambda‑cube :


Le second, celui de Barendregt, est aussi celui du calcul des constructions, de Coquand. C’est ce qui explique que les logiques dérivées du calcul des constructions soit si bien placé sur ce cube, qui établie une sorte de hiérarchie entre les logiques. Le lambda‑cube n’est en effet pas totalement neutre.

Le premier, porte dans son nom les trois lettres SKI, qui me rappel quelque chose, mais impossible de me souvenir quoi, je me souviens seulement que c’est important.

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 : 15514
Ven 3 Avr 2015 21:29
Message Re: Les logiques : notes en vrac
Un oubli que je ne corrige que maintenant.

Qui dit preuve des propriétés de quelque chose, dit nécessité de la couverture exhaustive des cas possibles sous lesquelles cette chose peut se présenter.

Concernant cette couverture, si on ne veut pas faire d’erreur d’interprétation, il ne faudrait normalement jamais oublier qu’avec les logiques, on est dans ce qui s’appelle l’hypothèse du monde clos (un exemple imagé est donné peu après). C’est une expression utilisée littéralement, et elle avait été rapidement mentionnée dans le sujet des références sur Prolog : Prolog — Les références partielles.

L’hypothèse du monde clos, ça signifie que quand on interprète les conclusions d’un système logique, il faut s’assurer que de toutes les choses essentielles à l’interprétation, aucune n’est ignorée par le système logique.

Un exemple imagé pour comprendre : si vous disposer d’un ensemble de connaissance portant sur la couleur de différentes fleurs, et que vous utilisez un système logique pour poser des questions du style « cette fleur est‑elle de telle couleur ? » et que vous poser la question à propos d’un fleur qui ne fait pas parti des connaissances, certains systèmes logiques vont sembler répondre « Non », alors qu’en fait ils ne peuvent répondre ni « Oui » ni « Non », car la fleur pour laquelle la question est posée, ne fait pas partie des connaissances. C’est cela l’hypothèse du monde clos : pour un système logique, s’il n’a pas de connaissance sur une chose, alors cette chose n’existe pas, même si elle existe en dehors de son monde.

La logique est souvent abordée comme une chose qui répond par « Oui » ou « Non » ou encore par « Vrai » ou « Faux ». C’est une erreur d’interprétation, et dans la plupart des cas (avis personnel), seules les réponses « Oui » ou « Vrai » sont valables, et le « Non » ou « Faux », devraient parfois — mais pas toujours — s’interpréter comme « Je ne sais pas » ou « Je ne peux pas répondre ».

Une conséquence suggérée est qu’il est nécessaire de définir ce que sont logiquement le « Vrai » et le « Faux » ou le « Oui » et le « Non », c’est à dire, qu’est‑ce que l’on interprète de cette manière et comment on aboutit à cette interprétation. L’interprétation comme « Vrai » et « Faux » peut être parfois triviale et même directe, mais pas toujours. Comme remarque personnelle, j’ajoute que c’est surtout avec l’interprétation comme « Non » ou « Faux » que des écueils peuvent se présenter, et un exemple a été donné plus haut ; les interprétations comme « Oui » ou « Vrai » me semblent poser moins de problèmes, mais c’est peut‑être seulement que j’ignore des cas qui me laisseraient avec une autre idée.

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 : 15514
Sam 16 Mai 2015 17:30
Message Re: Les logiques : notes en vrac
Un PDF en Anglais sur la logique dans le langage naturel :
Logic_and_Natural_Language.pdf (umass.edu), Novembre 2005.

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 : 15514
Mer 16 Déc 2015 20:47
Message Re: Les logiques : notes en vrac
J’ajoute cette entrée à la bibliographie de la page 2.

A survey into the Curry‑Howard isomorphism & type systems (ccs.neu.edu) [PDF], Phillip Mates, 2011.

Abstract a écrit : 
The Curry-Howard Isomorphism is the correspondence between the intuitionistic fragment of classical logic and simply typed lambda calculus (λ→). It states that the type signatures of functions in λ→ correspond to logical propositions, and function bodies are equivalent to proofs of those propositions. In this survey we will explore the implications of this isomorphism and how it scales to higher order logic and type systems, such as System F and Dependent Types. Furthermore, we will look at how the Curry-Howard Isomorphism is being put to use in modern programming languages and academic research.


Traduction a écrit : 
L’isomorphisme de Curry‑Howard, est la correspondance entre le fragment intuitionniste de la logique classique et la lambda‑calcul simplement‑typé (λ→). Il pose que les signatures des fonctions dans λ→, correspondent à des propositions logique, et que les corps des fonctions sont équivalentes à des preuves de ces propositions. Dans cette enquête, nous explorerons les implications de cet isomorphisme et comment il peut s’ajuster à la logique d’ordre supérieur et systèmes de types, tel que System F et les Types Dépendants. De plus, nous verrons comment l’isomorphisme de Curry‑Howard est mis en œuvre dans les langages de programmations modernes et la recherche académique.

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 : 15514
Lun 21 Déc 2015 11:24
Message Re: Les logiques : notes en vrac
L’isomorphisme de Curry‑Howard, pour les débutant(e)s : The Curry-Howard isomorphism for dummies (rocq.inria.fr) [PDF], Pierre‑Marie Pedrot, Février 2015.

Et à la bibliographie, j’ajoute : Proofs and types (paultaylor.eu) [PDF], Jean‑Yves Girard, Paul Taylor et Yves Lafont (ces deux derniers, pour les annexes), 1989‑2003.

Ce dernier, il est chouette, il couvre tout : déduction naturelle, Cyrry‑Howard, System F, et types linéaires, pour ne dire que les grandes lignes.

Image
Hibou57

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