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
Dim 13 Avr 2014 20:27
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
J’ajoute à la liste du premier message, « calcul des séquents vs déduction naturelle ».

Une différence importante entre les deux, semble être l’élimination des coupures, une opération du calcul des séquents (pas nécessaire, le calcul des séquents pouvant être avec ou sans cette élimination). Les preuves avec le calcul des séquents sans coupures (après élimination), sont réputées plus longues que celles de la déduction naturelle (et je crois comprendre, que celle du calcul des séquent sans élimination des coupures, aussi), même s’il peut sembler contre‑intuitif qu’une chose à laquelle est appliquée une élimination de quelque chose, soit plus longue qu’une autre (peut‑être que l’élimination nécessite une substitution par une autre chose plus longue).

En Anglais, « élimination des coupures », se dit “cut‑elimination”.

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 14 Avr 2014 18:40
Message Re: Les logiques : notes en vrac

Le calcul des séquents et la déduction naturelle


Citation d’une thèse de maitrise de Aaron Bohannon, “Sequent Calculus and Abstract Machines(« Calcul des Séquents et Machines Abstraites »), Université de l’Oregon, 2004.

Une traduction est ajoutée plus bas.

Aaron Bohannon a écrit : 
The sequent calculus proof system, as an alternative to natural deduction and Hilbert-style systems, has been well-appreciated for its structural symmetry and its applicability to automated proof search. Over the past decade, it has additionally been shown to have a computational significance, perhaps most notably as a type system for the λ-calculus, designed by Hugo Herbelin. It is the purpose of this thesis to demonstrate that the structural properties of the λ-calculus (derived from the underlying type system) are ideally suited for describing the states and transitions of several abstract machines that have been developed for executing programs written in a functional style. […]


Traduction a écrit : 
Le calcul des séquents comme système de preuve, comme alternative à la déduction naturelle et aux systèmes à la Hilbert, a été apprécié pour sa symétrie structurelle et son applicabilité à la recherche automatique de preuve. Au cours de la précédente décennie, il a de plus été montré qu’il a une pertinence calculatoire, peut‑être le plus remarquablement comme système de typage pour le λ‑calcul, conçu par Hugo Herbelin. C’est le propos de cette thèse, que de démontrer que les caractéristiques structurelles du λ‑calcul (dérivé du système de typage sous‑jacent) sont conviennent idéalement pour décrire les états et transitions de plusieurs machines abstraites qui furent développées pour l’exécution de programme écrits avec un style fonctionnel. […]


Le calcul des séquents est venu après la déduction naturelle comme alternative à celle‑ci (la déduction naturelle étant elle‑même une alternative aux systèmes à la Hilbert), et le calcul des séquents a une proximité particulière avec le λ‑calcul.


Citation d’un papier de José Espírito Santo, “Revisiting the Correspondence between Cut Elimination and Normalisation(« Ré‑examen de la correspondance entre l’élimination des coupures et la normalisation »).

Une traduction est ajoutée plus bas.

José Espírito Santo a écrit : 
Cut-free proofs in Herbelin’s sequent calculus are in 1-1 correspondence with normal natural deduction proofs. For this reason Herbelin’s sequent calculus has been considered a privileged middle-point between L-systems and natural deduction. However, this bijection does not extend to proofs containing cuts and Herbelin observed that his cut-elimination procedure is not isomorphic to β-reduction. […]


Traduction a écrit : 
Les preuves du calcul des séquents d’Herbelin, sans coupures, établissent une correspondance 1‑1 avec les preuves de la déduction naturelle normale. Pour cette raison, le calcul des séquents d’Herbelin fut considéré un point intermédiaire privilégié entre les L‑systèmes et la déduction naturelle. Cependant, cette bijection ne s’étend pas aux preuves avec coupures et Herbelin observa que sa procédure d’élimination des coupures n’est pas isomorphique à la β‑réduction. […]


On apprend que l’élimination des coupures du calcul des séquents, est sujette à une correspondance, une peu comme il existe la correspondance de Curry‑Howard, et c’est très intéressant; que le calcul des séquents est entre les L‑systèmes et la déduction naturelle, ce qui suggère s’ajouter les L‑systèmes à la liste des systèmes de démonstration (mais j’ai un doute, et ne suit pas certain que ça en soit un).

Un L‑système est un système de Lindenmayer. C’est une grammaire formelle, précisément une grammaire générative, créé par Lindenmayer, alors biologiste, qui voulait créer un langage permettant d’exprimer formellement l’évolution de la croissance d’êtres vivants ou d’ensemble d’être vivants. Sa grammaire formelle a été récupérée par les théoriciens de l’informatique, le concept central des L‑systèmes étant le ré‑écriture.


D’après From Natural Deduction to the Sequent Calculus (imada.sdu.dk) [PDF]. Matthias Puech. Août 2013. Université AARHUS.

Matthias Puech a écrit : 
Natural deductions are “reversed” sequent calculus proofs.

Traduction a écrit : 
Les déductions naturelles sont des preuves par des calculs des séquents « en sens inverse ».



Un cours succinct et en français :
Déduction naturelle et calcul des séquents [PDF] (univ-mrs.fr). Marc Bagnol. 2012.


D’après Relevance of Curry-Howard (lambda-the-ultimate.org), une interprétation de l’élimination des coupures dans une preuve, est les évaluations dans un programme.

D’après Matthias Puech (référence donnée plus loin en arrière), la déduction naturelle est comme une fonction dans le style direct (celui qui se rapproche le plus d’une équation) et le calcul des séquent est comme une fonction avec accumulateur.

Historiquement dans le temps, la déduction naturelle précède le calcul des séquents, et il existe une relation entre les deux, qui fait autant venir la déduction naturelle avant, comme une précondition.
Auteur inconnu a écrit : 
Theorem. A ⊢ Γ A is derivable in the sequent calculus if and only if it is derivable in natural deduction.

Traduction a écrit : 
Théorème. A ⊢ Γ A est dérivable dans le calcul des séquents, si et seulement si, elle est dérivable dans la déduction naturelle.


Puis, autant important :
Auteur inconnu a écrit : 
Theorem. The sequent Γ ⊢ ∆ is provable in the sequent calculus if and only if Γ ⊧ ∆.

Traduction a écrit : 
Théorème. Le séquent Γ ⊢ ∆ est prouvable dans le calcul des séquents si et seulement si Γ ⊧ ∆.



Il existe deux systèmes de calcul des séquents : le système LK, pour la logique classique et le système LJ pour la logique intuitionniste.

Image
Hibou57

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

Dernière édition par Hibou le Ven 1 Jan 2016 04:18, édité 18 fois.

Mise à jour

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Lun 14 Avr 2014 19:41
Message Re: Les logiques : notes en vrac
À propos de la différence entre FOL et HOL, il semble que les définitions récursives, comme les types de données récursifs, ne peuvent être exprimées qu’en HOL et pas en FOL (du moins pas sans beaucoup de difficultés).

Si ce n’est pas une bêtise (ça me semble cohérent en tous cas), alors c’est une raison suffisante pour mettre HOL en exergue, surtout dans les sciences de l’informatique.

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 16 Avr 2014 05:51
Message Re: Les logiques : notes en vrac
Dans le message qui liste des liens, est ajouté Relevance of Curry-Howard (lambda-the-ultimate.org). Il permet aussi de compléter le message sur le calcul des séquents, car la correspondance de Curry‑Howard, dit que l’élimination des coupures dans une preuve, correspond aux évaluation dans un programme.

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 16 Avr 2014 19:20
Message Re: Les logiques : notes en vrac
Question de symboles. Ne pas confondre ⊧ (U+22A7) et ⊨ (U+22A8). C’est la purée de pois pour les distinguer. Unicode appel le premier “models” (« modélise ») et le second “true” (« vrai »).

Deux problèmes…

Le symbole ⊨ semble être la tautologie pour Unicode, alors que la tautologie se représente le plus couramment par le symbole ⊤ (U+22A4, “down tack”).

Le symbole ⊧ semble être la substitution / la conséquence sémantique, alors que la conséquence sémantique se représente le plus couramment par le symbole ⊨.

J’irai demander de l’aide dans un endroit approprié pour éclaircir cette ambiguïté, et ce message sera édité en conséquence si j’obtiens une réponse satisfaisante.

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 16 Avr 2014 21:26
Message Re: Les logiques : notes en vrac

Les systèmes de preuves


Hibou a écrit : 
  • […];
  • Calcul des séquents vs déduction naturelle vs L‑systèmes vs système à la Hilbert (sequent calculus vs natural deduction vs L‑systems vs Hilbert‑style system);
  • […].

Ces choses toutes reliées entre elles, sont des exemples de systèmes de preuves. Il est plus commode (pas besoin de tous lister) et plus sûr (évite le risque d’en oublier ou d’omettre ceux à venir) de les désigner par cette catégorie générale.

Ce message les listera en donnant leurs caractéristiques générale. Il sera sujet à mise à jour.

Les systèmes à la Hilbert (Hilbert systems)


À l’inverse des systèmes à séquents, ils sont constitués d’un grand nombre d’axiomes et d’un petit nombre de règles d’inférence, souvent même une seule, le modus‑ponem (i.e. A ⇒ B, A ⊢ B). J’ai l’impression que ça correspond au seul qui soit appris à l’école (finalement, on n’apprend presque rien de la logique à l’école… ou tellement peu). Les systèmes à la Hilbert sont réputé laborieux et conviennent plutôt à l’étude de la réalisabilité d’une preuve plutôt qu’à l’étude et à la réalisation d’une preuve.

Les systèmes à séquents (sequent systems)


À l’inverse des systèmes à la Hilbert, ils sont constitués d’un petit nombre d’axiomes et d’un nombre plus important de règles d’inférence.

La déduction naturelle (natural deduction)


Elle est un système à séquents. Ses règles sont symétriques, avec des règles d’introduction (assemblage, du haut vers le bas, descendant) et des règles d’élimination (désassemblage, du bas vers le haut, montant), pour chaque connecteur logique (∧ ∨ →/⇒ ¬ ⊥/RAA ). Contrairement au calcul des séquents, les preuves se lisent dans les deux sens. Comme son nom l’indique, elle a été créée (par Gherard Gentzen), pour être aussi proche que possible du raisonnement humain (quand il raisonne sur les détails d’une preuve). Elle convient bien à la formalisation des langages fonctionnels (ex. SML), mais convient assez mal à la recherche de preuve et encore moins à la démonstration automatique de preuve, et même ne convient pas à la validation informatique des preuves (ça, ce serait utile de montrer pourquoi par des petits exemples), tout cela, à cause du sens bidirectionnel de la lecture.

Gherard Gentzen a écrit : 
I intendend first to set up a formal system which comes as close as possible to actual reasoning. The result was a calculus of natural deduction.

Traduction a écrit : 
Mon intention était de concevoir un système formelle qui soit aussi proche que possible du raisonnement courant. Il en a résulté le calcul de la déduction naturelle.


Voir aussi le message sur à la fois, la déduction naturelle et le calcul des séquents.

Les calculs de séquents (sequent calculus)


Il est un système à séquents. Il expose bien le détail des preuves. Il est parfois présenté comme « le langage assembleur des mathématiques ». Il convient bien au traitement automatisé des preuves, comme l’assistance à la recherche de preuves, la démonstration automatique et la validation de preuves. Il est moins intuitif — moins proche du raisonnement — que la déduction naturelle. Contrairement à la déduction naturelle, les preuves se lisent dans un seul sens, toutes les règles d’inférence se lisant du bas vers le haut (le sens des règles d’élimination de la déduction naturelle). Malgré une certaine proximité par des règles de passage de l’un à l’autre système, les preuves du calcul des séquents sont assez différentes des preuves de la déduction naturelle.

D’après An introduction to Sequent Calculus (minimalblue.com). Décembre 2011. Auteurs multiple.

An introduction to Sequent Calculus a écrit : 
Sequent Calculus handles logical operators in a different way from Natural Deduction:

  • Natural Deduction uses introduction and elimination rules for the logical operator;
  • Sequent Calculus only uses introduction, but both on the left and on the right side of the sequent.

Traduction a écrit : 
Le calcul des séquents traite les opérateurs logiques d’une manière différente de celle de la déduction naturelle :

  • La déduction naturelle a des règles d’introduction et d’élimination pour les opérateurs logiques;
  • Le calcul des séquents n’a que des règles d’introduction, mais pour les deux côtés gauche et droit du séquent.


Voir aussi le message sur à la fois, la déduction naturelle et le calcul des séquents.

Image
Hibou57

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

Dernière édition par Hibou le Jeu 17 Avr 2014 07:04, édité 14 fois.

Mise à jour

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Dim 20 Avr 2014 06:19
Message Re: Les logiques : notes en vrac
À propos de la logique du premier‑ordre (FOL) :

Wikipedia EN a écrit : 
Gödel's completeness theorem (Gödel 1929) established the equivalence between semantic and syntactic definitions of logical consequence in first-order logic.

Traduction a écrit : 
Le théorème de complétude de Gödel's (Gödel 1929) établit l’équivalence entre les définitions sémantique et syntaxique de la conséquence dans la logique du premier‑ordre.

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 21 Avr 2014 09:22
Message Re: Les logiques : notes en vrac
À propos de la correspondance de Curry‑Howard.

Une citation de Pierre‑Louis Curien, CNRS et Université Paris 7, “What can sequent calculus do for functional programs?”, 2009.

Pierre‑Louis Curien a écrit : 
Curry‑Howard correspondence: simply typed λ‑terms = proofs of (minimal) intuitionistic logic in natural deduction.

Traduction a écrit : 
La correspondance de Curry-Howard : λ‑termes simplement typés = preuves de la logique intuitionniste (minimale) en déduction 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 : 22173
Dim 27 Avr 2014 06:43
Message Re: Les logiques : notes en vrac

Axiomes, règles d’inférence et définitions fondamentales des HOL


Ce message listera les éléments fondamentaux des différents système du type HOL. Il n’y a pas une unique axiomatisation, mais plusieurs, normalement équivalentes, les axiomes de base de l’un des systèmes, pouvant normalement être des théorèmes démontrables, dans les autres systèmes.

Ce message sera mis à jour de temps en temps (le temps de récupérer les axiomatisations de plusieurs systèmes).

Par convention raisonnable, le trait horizontal du calcul des séquents, sera représenté par le symbole « ∴ » (*) qui semble être le meilleur équivalent de la « ligne d’inférence » pour une écriture linéaire.

(*) Le caractère U+2234, “therefore”, choisi après une question que j’ai posé ailleurs. Voir Réponse à “Notation for the horizontal line found in sequent calculus for linear writing (math.stackexchange.com).

Règles d’inférences, définitions et axiomes fondamentaux de HOL‑Light


Source : hollight.pdf (cl.cam.ac.uk).

Règles d’inférence…

(REFL)   ∴ ⊢ t = t
(réflexivité de l’égalité)

(TRANS)   Γ ⊢ t = s, Δ ⊢ t = u ∴ Γ ∪ Δ ⊢ s = u
(transitivité de l’égalité)

(MK_COMB)   Γ ⊢ t = s, Δ ⊢ u = v ∴ Γ ∪ Δ ⊢ s(u) = t(v)
(congruence de l’égalité)

(ABS)   Γ ⊢ s = t ∴ Γ ⊢ (λx. s) = (λx. t)
(abstraction de l’égalité)

(BETA)   ∴ (λx. t)x = t
(relation entre l’abstraction et l’application de fonction)

(ASSUME)   ∴ {p} ⊢ p
(modus‑ponens où la prémisse est une supposition)

(EQ_MP)   Γ ⊢ p ⇔ q, Δ ⊢ p ∴ Γ ∪ Δ ⊢ q
(relation entre l’égalité et la déduction)

(DEDUCT_ANTISYM_RULE)   Γ ⊢ p, Γ ⊢ q ∴ (Γ - {q}) ∪ (Δ - {p}) ⊢ p ⇔ q
(déduction de l’égalité à partir d’une double‑déduction)

(INST)   Γ[x₁ … xₙ] ⊢ p[x₁ … xₙ] ∴ Γ[t₁ … tₙ] ⊢ p[t₁ … tₙ]
(instanciations de variables dans la prémisse et la conclusion d’un théorème)

(INST_TYPE)   Γ[α₁ … αₙ] ⊢ p[α₁ … αₙ] ∴ Γ[γ₁ … γₙ] ⊢ p[γ₁ … γₙ]
(instanciations de variables de type dans la prémisse et la conclusion d’un théorème)

Note a écrit : 
In MK COMB it is necessary for the types to agree so that the composite terms are well-typed, and in ABS it is required that the variable x not be free in any of the assumptions Γ, while our notation for term and type instantiation assumes capture-avoiding substitution.

Traduction a écrit : 
Dans MK_COMB, les types doivent être en accord, de sorte que le terme composé soit bien typé, et dans ABS, la variable x ne doit être libre dans aucune des suppositions de Γ, cependant que notre notation pour les terme et instanciation de [variables ndt] type présuppose une substitution sans capture.


Définitions…

⊤ ≝ (λp. p) = (λp. p)
(définition de Vrai)

∧ ≝ λp. λq. (λf. f p q) = (λf. f ⊤ ⊤)
(définition de la conjonction)

⟹ ≝ λp. λq. p ∧ q ⇔ p
(définition de l’implication matérielle)

∀ ≝ λP. P = λx. ⊤
(définition du quantificateur universel)

∃ ≝ λP. ∀q. (∀x. P(x) ⟹ q) ⟹ q
(définition du quantificateur existentielle)

∨ ≝ λp. λq. ∀r. (p ⟹ r) ⟹ (q ⟹ r) ⟹ r
(définition de la disjonction)

⊥ ≝ ∀p. p
(définition de Faux)

¬ ≝ λp. p ⟹ ⊥
(définition de la négation)

∃! ≝ λP. ∃P ∧ ∀x. ∀y. P x ∧ P y ⟹ x = y
(définition du quantificateur existentiel unique)

Note a écrit : 
These definitions allow us to derive all the usual (intuitionistic) natural deduction rules for the connectives in terms of the primitive rules above. All of the core “logic” is derived in this way.

Traduction a écrit : 
Ces définitions nous permettent toutes les règles usuelles (et intuitionnistes) de la déduction naturelle pour les connecteurs en termes des règles primitives ci‑dessus. Tout le cœur de la « logique » est dérivé de la même manière.


Axiomes…

(ETA_AX)   ∴ ⊢ (λx. t x) = t
(axiome d’extensionnalité)

(SELECT_AX)   ∴ ⊢ P x ⟹ P ((ε)P)
(axiome du choix de Hilbert)

(INFINITY_AX)   l’ensemble des termes de type ind, est infini
(axiome de l’infinité des individuels)

Il est à noter que les règles d’inférence REFL, BETA et ASSUME, sont en fait aussi des axiomes, et aurait put être noté avec les autres axiomes. Je les ai laissé dans les règles d’inférence, parce que le document original les place ainsi.

Image
Hibou57

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

Dernière édition par Hibou le Dim 27 Avr 2014 13:54, édité 17 fois.

Mise à jour

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22173
Dim 27 Avr 2014 09:13
Message Re: Les logiques : notes en vrac
Un axiome n’est rien d’autre qu’une règle d’inférence dont la prémisse est vide.

Réponse à “Understanding properties and criticisms of a specific sequent calculus” (math.stackexchange.com). Octobre 2013.
Citation : 
[…] formally an axiom is neither more or less than a rule of inference that requires no premises.


D’ailleurs, les règles d’inférence initiale et avec prémisse(s), sont autant posées « à‑priori » que le sont les axiomes. La distinction n’est pas tellement pertinente et plutôt arbitraire. Ce qui est indiscutable, c’est plutôt la distinction entre les fondations et ce qui peut être dérivé des fondations.

— Édit du 1 Janvier 2016 —

C’est faux, car un théorème démontré peut ne pas avoir de prémisses.

Image
Hibou57

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

Dernière édition par Hibou le Ven 1 Jan 2016 04:22, édité 1 fois.

Correction

Profil Site Internet