Re: Questions sur le livre de Dehornoy
GaBuzoMeu: voilà ce qui se passe en gros (je pense que ça revient à ce que tu dis):
J'ai un type $U$ donné (c'est parce que le formalisme utilisé dans coq l'impose mais ça ne change rien) et une formule $A$ à un paramètre dans $U$.
Je crée une nouvelle section (un bloc).
Je déclare un objet t de type $T$ (c'est ce que j'appelle dans mes posts plus haut une variable locale)
Je prouve $\big(\forall x:U, A(x)\big) \to \big (\exists x:U, A(x) \big )$ dans ladite section (i.e. j'établis $\vdash_{[t]} \big(\forall x:U,A(x) \big)\to \big ( \exists x:U, A(x)\big ) $).
Quand je ferme la section, je me retrouve avec une preuve ($\vdash_{[]}$) de $\forall t:U,\left [ \big(\forall x:U,A(x) \big)\to \big ( \exists x:U, A(x)\big )\right ]$.
[size=x-small]Oui il y a beaucoup de code pour une seule idée, c'est le drame de ce genre de logiciels.[/size]
J'ai un type $U$ donné (c'est parce que le formalisme utilisé dans coq l'impose mais ça ne change rien) et une formule $A$ à un paramètre dans $U$.
Je crée une nouvelle section (un bloc).
Je déclare un objet t de type $T$ (c'est ce que j'appelle dans mes posts plus haut une variable locale)
Je prouve $\big(\forall x:U, A(x)\big) \to \big (\exists x:U, A(x) \big )$ dans ladite section (i.e. j'établis $\vdash_{[t]} \big(\forall x:U,A(x) \big)\to \big ( \exists x:U, A(x)\big ) $).
Quand je ferme la section, je me retrouve avec une preuve ($\vdash_{[]}$) de $\forall t:U,\left [ \big(\forall x:U,A(x) \big)\to \big ( \exists x:U, A(x)\big )\right ]$.
[size=x-small]Oui il y a beaucoup de code pour une seule idée, c'est le drame de ce genre de logiciels.[/size]
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
@GBZM: ce n'est pas qu'un goût. J'ai des raisons que j'ai parfois développées sur le forum. Je respecte les spécialités. Je comprends les gens qui ont envie de typer (entre AUTRE comme foys l'a LUI MEME RAPPELE, pour garantir la consistance ou la terminaison des algo) mais ça doit venir EN AVAL de la recherche et être une spécialité parmi d'autres. Sinon, si elle s'impose trop le nombre chercheurs transgresso-typage diminuera et on n'aura plus de financement pour les recherches fonda sur les théories fortes (et certes risquées). Il y a deux bouts.
De plus pour revenir à ce dont on discute on ne peut pas être auto réfèrent c'est à dire signaler un théorème dans un système usuel ULTRA REPANDU (auquel je ne suis pas suspect d'adhérer puisque j'aime comme toi l'ensemble vide) et juste répondre (ce que tu fais): OK bon bin voici une restriction qui elle marche (la quantification uniquement bornée pour la nommer par son nom historique). Bien sur il est plus modeste de ne pas quantifier sur "le monde entier" mais on ne peut pas évacuer les questions que se posent ceux qui ont toujours quantifié sur le monde entier en leur disant "vous aviez tort voilà ce qui arrive aux imprudents". Surtout quand c'est un truc aussi enfantin que la convention de ne pas prendre de modèles vides.
De mon téléphone
** par contre je suis sur mon téléphone mes réponses ultérieures peuvent tarder pardon.
Ce que je déplore, c'est cette reformulation snobinarde (je ne parle pas de toi, j'ai lu des textes où des auteurs autoritaires commençaient par " nous méprisons les gens qui confondent $\forall x\in A: R(x)$ avec $\forall x: (x\in A\to R(x))$ " (au quasi-mot près), tu es loin d'être le moins modéré) de $\forall x\in A$ en $\forall x:A$, surtout quand on sait qu'au fondement de ça, il n'y a pas de $x$ et que c'est une commodité.
Derrière ça, il y a, je l'ai dit, de la politique, mais ça, c'est pas grave, c'est noble, mais surtout un risque de profonde dégradation de la recherche mathématique si on continue (je le vois tout autour de moi, et on m'envoie souvent des mails pour me demander si c'est pertinent, mais je dois être un des seuls à répondre "non, il y a un gros risque que ça ne le soit pas") d'avoir une chapelle autant prosélyte***.
Oui, c'est de la recherche,oui c'est intéressant, mais non, ça n'a rien de "général" ni de "logique", ni de fondateur. Pour l'algèbre il y a de grandes chances que ça conduisent à de très intéressantes unifications comme je l'ai souvent dit.
Dans un autre fil j'ai expliqué pourquoi à mon avis, il faut aller dans rtès exactement le sens opposé: c'est à dire que quand $x$ n'est pas de type $A$, l'énoncé (que cette chapelle voudrait voir n'être jamais écrit et juste syntaxiquement fautif), $x\in A$ doit recevoir en toute honnêteté une valeur de vérité et non recevoir un avis de "je ne lirai pas".
Certes les classiques lui donnent la valeur "faux", mais je ne vais pas forcément jusque là dans le sens que le faux n'existe pas vraiment. Mais en aucun cas, ce mouvement politique ne doit continuer à prendre trop d'ampleur. Je rappelle qu'il n'existe strictement aucun objet mathématique qui soit typable "honnêtement" à par des absolus très peu intéressants. Combien de fois ai-je dû signaler à GG que $\N$ n'a pas de sens absolu? Il n'est défini que dans un univers ensembliste et qu'il n'y a aucun moyen de savoir si on a raison de croire à l'existence de l'intersection même seulement de tous les ensembles DEFINISSABLES contenant 0 et stable par suc (c'est une définition aussi autoréfente que $A:=(A\to Tout)$)
On avait $\vdash$, tu nous invites à connaitre $\vdash_{indices}$. Je ne sais pas si tu vois l'inflation notationnelle. Bref, je pense que nous sommes très limités et que "charger" les barques mènent non pas comme cette chapelle le croit à des progrès, mais plutôt à de la confusion et surtout un tarissement des théorèmes de fond (je ne connais aucun théorème profond qui ne transgresse pas la recherche de sécurité cherchée derrière le typage)
Par contre, bien sûr, j'en conviens, je viens de faire un discours purement politique et je ne donne que mon avis. Le sujet du fil ou ton invitation adressée à foys ne sont pas en cause puisqu'il ne s'agissait que de signaler un système où $\forall \subset \exists$ n'est pas "forcé" par les règles.
*** car ses adversaires n'en ont cure et se contentent de ne pas s'exprimer
Lorsque Grothen a demandé à être introduit à du bas niveau informatique, j'ai estimé utile de lui donner directement ce qui se fait de mieux comme coeur de processeur et qui se fonde sur des découvertes qui au départ se nourrisaient au lambda-calcul.
Il faut toutefois retenir que ce système fait peut de cas de la longueur des mots en mémoire et donc est en trompe-l'oeil, mais ce problème de gestion de mémoire sera disons HS.
Je ne savais pas que j'étais lu par alesha. Quand il a posé ses questions, je lui ai bien sûr répondu comme j'aurais répondu à grothen, de manière simplifiée.
Alors qu'alesha avait en tête un truc apparemment très précis, qui n'est rien d'autre que toute la théorie du lambda calcul et des découvertes qui ont été faites à son propos (il y a une longue liste, un peu comme pour les fonctions holomorphes de théorèmes "poil à gratter" rigolos)
Je donne donc quelques précisions:
1) en LC pur déjà on n'utilise pas de combinateurs (contrairement à moi qui en utilise et qui en plus ai rejeté toute variable). Mais ça c'est peu important
2) On appelle "réduction gauche" (enfin je crois que c'est son nom) le fait de procéder comme suit pour "déplier" (on dit "normaliser si possible") un terme du LC.
Normalize(u.v) := try r:=Normalize (u) finally "est-ce que r est de la forme $x\mapsto w$, si oui remplacer $x$ par $v$ dans $w$ et Normalize le résultat sinon try s:=Normalize(v) et renvoyer r. s
C'est extrêmement précis et le processeur avec piles que j'ai décrit à grothen reprend "avec légèreté" cette stratégie sans définition récursive.
On peut aussi prouver que c'est "la meilleure de toutes" les stratégies de normalisation
3) Mais attention: dans l'échange avec grothen, je n'ai évidemment pas introduit "d'éthique" (c'est un truc qui voudrait en gros que l'argument lui même dans l'écriture u.v soit "caché à u en tant que suite de caractères et lui apparaisse directement comme un "objet"), car tout simplement, je ne la suis (suivre) pas du tout cette éthique. Entre autre, chez moi, il n'y a pas nécessité de confluence, pas nécessité de n'ontroduire que des instructions qui voient seulement le premier terme de la pile, etc.
D'où les réponses que j'ai faites qui lui ont en partie déplues.
C'est peut-être parce que dans de tels systèmes il y a un théorème de déduction qui dépend des axiomes utilisés, qui n'est pas toujours vrai et que (priorité à droite pour les parethnèses) la preuve de $[A,B,C,D,A\to B\to C\to D\vdash D]$ est très courte et celle de $[\vdash (A\to B \to C \to D)\to A\to C \to B \to D]$ gigantesque?
Sinon, je vois que tu connais COQ. On m'en a dit beaucoup de mal (en particulier JLK, il y a 10-12ans quand il m'a initié à sa théorie). Il parait qu'il peut falloir des mois pour y entrer des preuves ... qu'on a sous les yeux et pas si longues
De manière expérimentée, je peux t'inviter, si ce n'est déjà fait à adopter AUSSI caml. Au moins avec lui, tu n'as aucun des inconvénients évoqués.
1) Tu peux entrer toutes les preuves TELLES QUELLES, sans contorsion
2) Ca ne prend que quelques minutes
3) Il n'y a pas de bridage et les raise sont installés
4) Pour te montrer à quel point c'est confortablre d'utilisation, j'ai dû reprogrammer 200 fois mes prouveurs car je n'éprouvais pas le besoin de les "mémoriser" (je ne me rappelais pas la fois suivante ce que j'avais défini). Ca ne m'a pas empêché d'exécuter le théorème de Brouwer, de Tychonoff, et AC=>non(AD)
5) L'avantage aussi est que les axiomes de ZFC (sauf l'extensionnalité) sont tous réalisés par ... J (le combinateur qui ne fait rien, et habituellement voué à $X\to X$)
6) Et cerise sur le gâteau, grace à alesha (ici intervenant), tous les programmes terminent!!!! Sachant que l'on implémente dans la TDE originelle (celle où toute collection est un ensemble) c'est un tour de force. Cela est dû au fait que grace à lui tout repose sur l'extensionnalité (qui implique A=>(A et A), donc qui évite de dupliquer les ressources, do'ù la terminaison). Par contre, ça peut parfois êrte exponentielle, mais je cherche une amélioration .... linéaire (en utilisant $\otimes$ à la place de $\wedge$ et toujours l'argument alesha)
Bref: CAML c'est bien. :-D
@GBZM: j'ai précisé dans l'autre fil mon erreur pour $\pi$: j'ai prouvé irréfutablement que si une certaine fonction est injective alors $\pi$ est irrationnelle. Il se trouve qu'elle est constante 2 :-D . Comme quoi, pas besoin de prouver $\forall X:X$ pour apprendre des choses. Prouver un truc vrai suffit.
Christophe c: j’ai commencé à prouver les théorèmes que t’avais mis qui étaient les théorèmes de type « lettre bidule réalise phrase machin » juste pour être rassuré tu peux me dire si j’ai pas fait n’importe quoi ? (Toi ou n’importe qui qui connaît ces trucs-là)
Donc par exemple pour celui qui était le plus simple à montrer:
J réalise $\forall A, A\to A$ (J’appelle cette phrase E)
Soit $p\in E, \exists A, p\in $ « $A\to A$ »
C’est-à-dire qu’il existe un programme x qui réalise A et une pile $n\in A$ (pourquoi le terme agresser comme synonyme d’appartenir? J’ai essayé de réfléchir un peu dessus vraiment je vois pas du tout, rapport physique avec une vraie pile ?) tels que $p = x + n$. x réalise A signifie $\forall q\in A, (x,q)\in $ « Paradis » or $n\in A$ donc $(x,n)$ est élément de Paradis (pourquoi ce nom ? Elle sort d’où cette nomenclature zarbi « agresser » « paradis » :-D ça me fait penser au rayon spectral pour parler de norme de matrice ou un truc du genre ou dirait la traduction en VF malfoutue d’une attaque d’un perso de dragon ball Z j’ai pas pu m’empêcher de me taper un fou-rire quand on m’a sorti cette expression) or (J,p)=(J,x+n) qui donne en un pas (x,n) or Paradis est stable par « pas inverse » donc (J,p) est dans paradis.
C’est vrai pour tout p donc J réalise la phrase E.
Édit: ah et aussi, pour toi non(A) est-ce que c’est $A\to $ $Paradis$ ? (Si c’est ça donc paradis c’est « Faux » l’espece De symbole qui ressemble à un T à l’envers que je vois parfois) si oui toujours même question pourquoi paradis ?
Je comprends pas, c’est pour les piles que tu utilises le mot agresser or un ensemble de pile c’est une phrase pas une pile.
Tu étends le mot agresser aux phrases aussi ? Imaginons que ce soit le cas, donc faux est un certain ensemble de phrase du coup (lequel ?) alors que paradis est un ensemble de processus. Est-ce que faux est l’ensemble des phrases telles que pour tout programme x, x réalise ces phrases ?