Logique intuitionniste et CCH — Les-mathematiques.net The most powerful custom community solution in the world

Logique intuitionniste et CCH

christophe cchristophe c
dans Fondements et Logique
Comme je n'ai jamais dû faire un truc "propre" pour les lecteurs débutants, je donne une version "un peu simpliste et remixée" pour les amateurs (suis en train de surveiller un bac blanc et on ne vient pas me suppléer :-X ). Ce mode d'emploi permet aux lecteurs motivés de pouvoir ensuite aller plus loin. Le sujet est brûlant avec des centaines de chercheurs (sinon plus) payés 3000E/mois. Donc ce n'est qu'une petite intro, mais j'espère que ça fera comprendre.

1/ J'appelle "combi" un uplet $(E,*,C,K,W)$ tel que $\{C;K;W\}\subset E$ et $*$ est une application de $E^2$ dans $E$ qui vérifie:


1.1/ $\forall x,y,z$ dans $E: [((C*x)*y)*z = y*(x*z)$
1.2/ $\forall x,y$ dans $E: [(K*x)*y) = x]$
1.3/ $\forall x,y$ dans $E: [(W*x)*y) = (x*y)*y]$

Dans la suite on notera $ab$ à la place de $a*b$ et les priorités des parenthèses sont à gauche, ie $abc$ abrège $(ab)c$. Une "combi" est fixée une fois pour toute jusqu'à la fin.

2.1/ Pour des parties quelconques $X,Y$ de $E$, je note $X\to Y$ l'ensemble des $x\in E$ tels que pour tout $y\in X: xy\in Y$.

2.2/ Pour toute famille $f$ de parties de $E$, je note $\forall x: f(x)$ l'intersection des $f(x)$ quand $x$ parcourt le domaine de $f$.

2.3/ Pour toutes partie $X,Y$ de $E$, je note:
2.3.1/ $X\wedge Y$ l'ensemble $\forall Z : [(X\to (Y\to Z))\to Z]$
2.3.2/ $X\vee Y$ l'ensemble $\forall Z : [(X\to Z)\to ((Y\to Z)\to Z)]$

3/ Exercices:

3.1/ Prouver l'existence, dans $E$ d'éléments $D,B,G,M,J,T$ vérifiant, pour tous éléments $x,y,z: $

3.1.1/ $Dxyz = x(yz)$
3.1.2/ $Bxy=yx$
3.1.3/ $Mxyz = x(zy)$
3.1.4/ $Jx=x$
3.1.5/ $Txyz = zxy$


3.2/ Prouver que $T\in \forall X,Y: [X\to (Y\to (X\wedge Y))]$

(qu'est-ce que ça me fait mal d'écrire ça, mais on est en logique intuitionniste, donc c'est bon. Mais bien entendu le truc de fond, c'est que:

$$T\in \forall X,Y: [X\to (Y\to (X\otimes Y))]$$

voir troisième post du fil. Hélas la log intu écrase la différence entre $\wedge$ et $\otimes$, snif.

3.3/ Prouver que $J\in \forall X:(X\to X)$

3.4/ Prouver que $C\in \forall X,Y,Z: [(X\to Y)\to ((Y\to Z)\to (X\to Z))]$

3.5/ Prouver que $J\in [(\forall xR(x))\to R(a)]$

3.6/ Construire un élément de $E$ qui appartient à $\forall R,a: [R(a)\to (\exists R(x))]$

3.7/ Construire des éléments de $E$ qui appartiennent aux ensembles suivants pour tous sous-ensembles de $E$

3.7.1/ $A\to (A\vee B)$
3.7.2/ $(A\vee B)\to (A\cup B)$
3.7.3/ $(A\cap B)\to (A\wedge B)$

4/ Les lecteurs qui auront fait tous ces petits exos (pas très difficiles) auront bien avancé et il leur restera à me demander vers quoi ils veulent ensuite que je documente le fil.

5/ J'allais oublier le plus important :-D . La logique intuitionniste est l'en,semble des phrases qui sont telles que si on les interpréte comme des parties de $E$ alors, on peut prouver qu'elles sont non vides. Leurs éléments peuvent être raisonnablement nommés des "réalisateurs" ou encore des "garanties" de ces phrases.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
«1

Réponses

  • christophe cchristophe c
    Pour que ce soit plus agréable à aborder, je donne quelques précisions historiques.

    1/ Les lettres majuscules (C,K,W...) que j'ai utilisées tout au début s'appellent généralement des "combinateurs" et étudier "ces choses" s'appelle "faire de la logique combinatoire".

    2/ La "vraie" CCH est un peu plus compliquée que ma présentation, mais ma présentation est parfaitement fidèle sur le fond aux phéomènes mathématiques découverts. Elle est donc "en un certain sens" bien mieux que ce qui est présenté dans les livres (qui font 200 pages).

    3/ On notera que $A\wedge B$ n'a rien à voir avec $A\cap B$, alors que pour $A\vee B$ on ressent une plus forte proximité avec $A\cup B$.

    4/ Il y a en gros deux tendances à l'entrée du chateau qui cherche à étudier ces choses. Une approche qui essaie (c'est le grand slogan de Alain Prouté par exemple) de rendre toutes les preuves d'un même théorème "égale" en un certain sens (qui n'a jamais été trouvé, c'est une sorte d'idéal). Une approche à l'extrême opposé qui fait qu'une preuve démontre plusieurs choses et qu'il y a toujours une infinité de preuves différentes pour prouver un théorème

    5/ La découverte a été tardive car on avait tendance (ce qui est respectable) historiquement à écrire des preuves avec des phrases qui décorait les articulations. Du coup il a fallu attendre en gros les années 1980 pour s'apercevoir que le "robot abstrait non décoré" de la preuve est suuffisant en le sens suivant: le couple (conclusion, robot) suffit instantanément à reconstruire la preuve telle que conçu historiquement comme un texte composé de phrases. C'est même mieux à cause de deux raisons:

    5.1/ La reconstruction évacue les hypothèses inutiles et respecte la polarité
    5.2/ Le robot donne la stratégie pour le prouveur dans le jeu prouveur-sceptique, or comme je l'ai déjà dit, in the fundamental world of science, le modus ponens n'est pas légitime, puisque l'inférence $(A,A\to B) \vdash B$ nécessite de vérifier l'égalité entre les deux $A$ (ce qui est infaisable en pratique, puisque ce sont des pointeurs et qu'il n'existe aucun programme capable de vérifier "une égalité sémantique" de deux pointeurs. Or le MODUS PONENS lui-même ne pose AUCUN PROBLEME lorsqu'on joue: le prouveur propose A et le sceptique CHOSIT entre continuer avec A ou avec $A\to B$. Il n'y a strictement aucune égalité à vérifier (pointeurs ou pas).

    6/ Important: la grande vertu des $W,C,K$ c'est de permettre que, quand vous avez un mot $m$ écrit avec $*$ et des parenthèses, et contenant certaines occurrences de la LETTRE $x$ (un nombre quelconque d'occurrences, éventuellement nul), alors grace à W,C,K, il est possible d'écrire un mot $p$ ET DE PROUVER que $px = m$ à partir de leurs seules propriétés supposées en (1.1) ... (1.3). Autrement dit, elles implémentent le mécanisme linguistique $x\mapsto m$. Avantage: faire sauter les variables et l'alpha-problème (renommage des variables liées dans les sciences).

    Pour finir, je vais illustrer en témoignant à voix haute, comment je construis un élément $G$ de $E$ tel que $Gxyz = xzy$ (autrement dit qui a l'effet suivant $f\mapsto (x\mapsto (y\mapsto f(y)(x)))$)

    C'est parti.... je ne mets pas de dollars:

    acb = ac(Kbc) = C(Kb)(ac)c = Ca ( [C(Kb)] ) c c = W [ Ca ( [C(Kb)] ) ] c =

    W [ Ca ( [ (CKC) b ] ) ] c = W [ C (CKC) (Ca) b ] c = W [ CC [C (CKC)] a ] b ] c = C( CC [C (CKC)] )W abc     gagné!!!!

    SI on pose $G:= C( CC [C (CKC)] )W$, on a obtenu que $\forall x,y,z: Gxyz = C( CC [C (CKC)] )Wxyz = xzy$.

    "L'esprit CCH" vient en fait de juste établir qu'on peut obtenir :

    $$ (X\to (Y\to Z))\to (Y\to (X\to Z)) $$

    à partir des 3 axiomes suivants (réalisés respectivement par $W,C,K$)

    $$\forall U,V,W : [ U\to (V\to U) ; (U\to (U\to V))\to (U\to V); (U\to V)\to ((V\to W)\to (U\to W))]$$

    en utilisant seulement le modus ponens.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Encore quelques précisions: les robots $W,C,K$ suffisent à eux seuls à décrire la logique intuitionniste. Il y a une correspondance, comme vu ci-dessus, entre axiomes des maths et garanties atomiques.

    Mais si on oublie le "côté preuves", il est intéressant de noter que cette approche "renseigne" sur plein de petits aspects:

    1/ on croit souvent que le produit cartésien est pertinent. Or, le paradigme montre que ce n'est pas du tout le cas "naturellement". en effet, un couple $(u,v)$ de robots, c'est "réellement" le robot : $[x\mapsto x(u)(v)]$ (**), qui dans d'autres domaines des maths est connu sous le nom de produit tensoriel et non pas sous le nom de produit cartésien. Et de fait, on "voit bien" que le passage de $(x,y)$ à $x$ va "jeter la ressource $y$". Le robot (ah oui, j'oubliais, appelons "robots" les éléments de $E$) $(u,v)$ devrait en fait se noter $u\otimes v$ et c'est ce que je ferai dans la suite du fil. On remarque que $(u\otimes v)K = u$. C'est pourqyuoi j'ai noté $T$ dans l'exercice qui demande le robot qui réussit $\forall x,y,z: Txyz = zxy$.

    Mais $K$ ce n'est pas n'importe qui. C'est le garantisseur de $A\to (B\to A)$, axiome qui n'est pas accepté en logique linéaire par exemple, et pour cause, il a un grand pouvoir qui est celui de jeter une ressrouce (rappel: $Kxy=x$). L'opération "abscisse" ou encore nommée "première projection" est donc le robot $BK$ ($B$ est le robot qui fonctionne comme suit: $\forall xy: Bxy=yx$ et les algébristes lconnaissent très bien $B$ qui est l'isomorphisme canonique de $E$ dans $E^{**}$).

    N'importe quel pro en algèbre linéaire sait bien qu'il n'y a pas d'habitants canoniques dans $L(E, L(F,E))$ o ù $L(X,Y$ désigne l'ensemble des applications linéaires de $X$ dans $Y$.

    Bref, il faut le pouvoir de la logique intuitionniste tout entière pour "projeter" (jeter des ressources), mais aussi pour dupliquer, ie obtenir un robot $r$ qui a comme effet : $\forall x: rx=x\otimes x$. Je laisse le lecteur le construire.

    Certains lecteurs se demanderont à quoi de logique correspond l'intersection (le produit tensoriel est le "et"). Et bien .... personne ne sait au juste :-D (c'est fondamentalement un problème ouvert, avec probablement une médaille Field à la clé à qui le fermera complètement). La seule chose qu'on sait c'est que $A\cap B$ contient les "objets" qui sont à la fois des preuves de $A$ et des preuves de $B$. De même $A\subset B$ signifie que $B$ est un cas particulier de $A$ (ie toute preuve de $A$ prouve $B$).

    Mais ça mène pas loin, puisque le seul exemple de preuve dans une intersection qui soit familière est le processus par lequel on s'autorise à passer d'une preuve de $R(x)$ sans rien avoir supposé sur $x$ à l'affirmation qu'on a prouvé $\forall xR(x)$. Mais au jour le jour, aucun matheux ne connait d'exemples disons "originaux" où on prouve AVEC LA MEME PREUVE deux énoncés ostentatoirement différents.

    Même question (et même peut-être encore plus intéressante) avec la proximité amie-ennemi entre $A\cup B$ et $A\vee B$. A noter aussi une chose spectaculaire: on a quand-même l'implication $(A\vee B)\to (A\cup B)$ qui est un petit joyau de la spécialité CCH. Qui eût cru qu'un jour on trouverait un majorant de $\{A;B\}$ qui soit "encore plus petit que le majorant bien connu $A\cup B$? :-D


    (**) j'ai donné en exercice au premier post de l'écrire à l'aide juste de $C,W,K$.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • FoysFoys
    NB: $\Gamma:=CC(CC)$ appartient à $(P\to Q \to R) \to (T\to Q) \to P \to T \to R$ pour tous $P,Q,R$; on peut ensuite poser $D:= C (CK\Gamma)$ et $S:= D(DW)\Gamma$. Ainsi on retrouve les combinateurs usuels B-).
    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$.
  • grothenbietegrothenbiete
    J’ai pas beaucoup de temps, donc j’ai juste fait le premier exo sur les nouveaux combinateurs.
    Peux-tu juste me dire si je débloque pas, je fais la suite dès que je peux.
    J = WK
    B = CK(CCW)
    D = CB(CC)
    M = CB(C(DCB))
    T = CB(C(DMB))

    Ps: je me rends pas du tout compte si c’est beaucoup trop long ou pas, même s’il y a une version en deux lettres à chaque fois (je pense que c’est impossible avec C K W j’avais testé ça marche pas) peux-tu au moins vérifier si c’est quand même bon je me fais pas du tout confiance.
  • christophe cchristophe c
    De mon téléphone: les premiers marchent et FELICITATIONS c'est bon signe. Je te ferai un chti programme pour les exécuter parce que les exécuter de te de mon téléphone je suis pas doué.

    @foys :je présume que tes parenthèses (pour les phrases) sont priorité à droite. Alors pour info et pour avoir contempler et programmer de tonnes de tentatives de passage concis de lambda terme à "combinateur-sans-variable"-termes avec caml l'expérience m'a montre que ton gamma (et même le S auquel tu penses sont trop consommateurs de "K". J'essairai de retrouver et poster mes meilleurs traducteurs mais il y avait pas mal de petits mécanismes artisanaux que j'avais ajoutes pour éliminer les "CJ" les "CxJ" et tout plein de pollueurs.

    @Grothen: bravo pour la concision de tes termes!!
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Bah je pourrais essayer en python pour le fun mais si t’as « Plus adapté » je veux bien.
    (Franchement flemme de dl masm pour l’assembleur surtout que je n’ai pas d’ordi je fais tout sur l’iphone, y a une app pour faire du python mais le reste pas sûr que ce soit faisable)
  • christophe cchristophe c
    De mon téléphone je ne connais pas python mais l'instruction "match" de caml c'est ultra-rapide.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    J’ai une question naïve de maths qui me gêne bêtement sur la suite. Elle apparaît dans l’exo en-dessous, ton 3.2.

    3.2. f est la fonction qui aux couples de parties de E: X et Y associe $X\to (Y \to (X\land Y))$. Je veux montrer que T est dans l’intersection de toutes les phrases (donc la phrase avec les quantificateurs).
    Soit X et Y deux parties de E et Z une partie de E. Soit p dans $X\to (Y\to Z)$.
    Soit x dans X et y dans Y, on a pxy dans Z.
    Or pxy = Txyp dans Z, donc Txy est dans $(X\to (Y\to Z))\to Z$ donc dans l’intersection sur Z donc Txy dans $X\land Y$ donc Tx dans blabla donc T dans blabla pour X et Y quelconques donc dans l’intersection c’est-à-dire ce qu’il faut.
    Pour moi cette démo est bancale.
    Je comprends pas bien le statut de l’ensemble vide, et ça me gêne à trois endroits, quand je dis soit x dans X, soit y dans Y, soit p dans $X\to (Y\to Z)$. Si X est vide je ne peux pas prendre de x dedans et du coup je ne peux pas prendre de p dans $X\to (Y\to Z)$ parce que je peux « rien appliquer à p avec * » (je peux pas écrire px de mon point de vue de débutant c’est même pas que c’est faux ou pas c’est que « c’est pas défini ») du coup je devrais systématiquement préciser que je prends X et Y non-vides mais du coup je ne sais pas du tout si $X\to (Y\to Z)$ est non vide pour prendre un p dedans. Du coup faut que je rajoute que le truc est non-vide tout le temps.
    Au final ça me rappelle que je suis pas très au clair sur « exister » ou sur « c’est quoi l’ensemble vide comment je le gère »


    Édit: en fait c’est moi qui suis censé dire comment je gère le domaine de f c’est Ça ? Je dois justifier que je peux trouver un domaine non-vide de f tel que les images sont jamais vides ?

    Édit 2: pour J en tout cas c’est moins gênant, je dois préciser que je fais l’intersection pour tous les X non-vides c’est tout car dès que c’est non-vide $X\to X$ aussi (x dans X donc Jx dans X donc J dans $X\to X$ donc dans l’intersection c-à-d $\forall X: X\to X$)
  • christophe cchristophe c
    Ta démo n'est pas bancale ce que tu dis est tout à fait correct y compris (et même encore plus :-D ) si x est dans emptyset etc.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    J'ai oublié quelques petits exercices édifiants pour augmenter le goût du sujet. Je donne quelques définitions avant:

    D1/ La somme d'un ensemble $X$ est $\{(u,v) \mid v\in X$ et $u\in v\}$
    D2/ L'union d'un ensemble $X$ est $\{x\mid \exists y\in X: x\in y\}$

    L'union d'un ensemble est donc l'image directe par la première projection (ie $(x,y)\mapsto x$) de sa somme. La somme (d'ensembles de cardinal 2) est intéressante dans le contexte présent, à condition de l'adapter:

    D3/ je note $X \sqcup Y := \{i\otimes x \mid (i=K$ et $x\in X)$ ou $(i=KJ$ et $x\in Y)\}$

    E1/ Prouver que pour tous $X,Y: $ l'ensemble $(X\sqcup Y)\to (X\vee Y)$ est non vide. [small]Je rappelle que les non vacuité de $(X\vee Y)\to (X\cup Y)$ et de $(X\vee Y)\to (X\sqcup Y)$ sont triviales et qu'il n'y a aucune raison de penser que pour tous $X,Y$, l'ensemble $(X\cup Y)\to (X\vee Y)$ est non vide a priori (mais ne connaissant pas la réponse "là et maintenant, je le mets sous forme de question)[/small]

    Q1/ Peut-on construire des ensembles $X,Y$ tels que $(X\cup Y)\to (X\vee Y) = \emptyset$

    E2/ Soit $a\in \forall X: (X\to X)$. Prouver que $a=J$.

    E3/ Soit $a\in \forall X,Y: (X\to [Y\to X])$. Prouver que $a=K$

    Je laisse les lecteurs s'amuser avec les autres "combinateurs". Autrement dit, se demander et répondre à la question de savoir s'ils sont les seuls à appartenir à l'intersection des théorèmes qu'ils garantissent. Les E2,E3 l'affirment pour $J$ et $K$.

    Avertissement: n'hésitez pas à vérifier que je ne me trompe pas, je n'ai fait sérieusement aucun des exos que je donne :-D , des erreurs sont possibles (même mon intuition de ce domaine est assez fiable).. Ca n'enlève rien à l'intérêt des exercices donnés que vous pouvez lire sous forme de questions "ouvertes".
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Un dernier pour la route. Je rappelle que la logique classique s'obtient à partir de la logique intuitionniste en ajoutant l'axiome:

    $$ \forall X,Y: ([(X\to Y)\to X]\to X) $$

    qui est appelé "axiome de Peirce"

    E4/ Prouver que $ \left( \forall X,Y: ([(X\to Y)\to X]\to X) \right) = \emptyset $

    Cet exercice montre que le paradigme retenu pour ce fil ne permet pas d'implémenter "naivement" la logique classique.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Ah parce que $(x\in \emptyset) \to T$ (T=tout) ....

    Édit: je répondais au post sur la démo bancale
  • Georges AbitbolGeorges Abitbol
    Euh, j'ai loupé la définition de $\exists x R(x)$, non ?
  • grothenbietegrothenbiete
    Elle y est sur le topic informatique page 3.
    $\forall P: (\forall x: (R(x)\to P))\to P$
  • Georges AbitbolGeorges Abitbol
    Merci !
    J'essaie de faire les exercices, mais j'ai du mal à avancer... Est-ce que $K$, $C$ et $W$ ont des noms ? Est-ce que $*$ a un nom ? Ca m'aiderait à trouver de l'inspiration !
  • grothenbietegrothenbiete
    Si, K s’appelle le combinateur « dustbin », W s’appelle « duplicator », et C le « implyer »
    Quant à * c’est « starlord »
    En espérant que ça t’aide

    Édit: pour les noms français je peux pas t’aider je connais pas la traduction mais je sais qu’historiquement le premier a avoir traduit en français c’est Alain Prouté.

    [Merci de respecter le patronyme d'Alain Prouté. Poirot]

    [un peu de tenue SVP]

    Édit réponse à CC: pour la 3.6 est-ce que tu peux me confirmer si c’est bien B ? J’aimerais bien avoir le temps de rester plus longtemps pour réfléchir à tout ça :/
  • Georges AbitbolGeorges Abitbol
    @Grothenbiete (En référence à ton EDIT) : Les gens du monde du catch savent pertinemment que c'est du fake ; toute la beauté du truc est qu'ils n'en parlent jamais :-D
    Pour le reste, merci pour les noms ! Cela ne m'a pas trop aidé à trouver de l'inspiration... J'ai essayé de me dire que $x * y$, c'est que $x$ est une sorte de Kirby, qui mange un autre Kirby $y$, et se transforme en un nouveau Kirby $x*y$, mais cela n'a pas porté ses fruits.
    Est-ce que je peux te demander comment tu as fait pour trouver $B$, par exemple ? Est-ce que tu te raccroches à des idées d'informatique ? Je dois dire que sans tes réponses, je crois que j'aurais tenté d'écrire un programme qui testerait tout plein de mots parenthésés avec $C$, $W$ et $K$ mais ça m'aurait pris du temps...
  • grothenbietegrothenbiete
    On Cherche un combinateur qui serait dans $\forall R,a: R(a)\to (\forall Z ((\forall x: (R(x)\to Z))\to Z))$

    Donc on cherche en fait un élément p par exemple qui soit dans l’intersection sur R,a de la phrase après le premier quantificateur. (Dans la suite je répète pas ça, mais à chaque fois qu’il y a un quantificateur c’est l’idée quoi)
    Donc je veux que pour un x dans R(a)
    Px soit dans $(\forall Z ((\forall x: (R(x)\to Z))\to Z))$
    Par définition ça revient à dire que pour un y dans $\forall x: (R(x)\to Z)$ on veut que pxy soit dans Z mais si y est dans $\forall x: (R(x)\to Z)$ qui est l’intersection des $(R(x)\to Z)$ il est en particulier dans $(R(a)\to Z)$ donc au final on cherche un p tel que pxy dans Z avec y dans blabla or si tu regardes un peu x et y, x c’est dans R(a) et y dans R(a) implique Z et par définition être dans R(a) implique Z ça veut dire que si on prend quelque chose dans R(a) en multipliant (le symbole étoile) c’est dans Z donc yx serait dans Z ce qu’on veut donc il faudrait un p qui transforme pxy en yx et dans la liste des combinateurs dont il fallait montrer l’existence plus haut t’as B qui fait exactement ce qu’on cherche bon après ça c’est ce que je me suis dit pour trouver mais faudrait montrer que B vérifie bien le truc en faisant un peu gaffe aux intersections et tout.

    Edit: en fait j’ecrs Juste la définition en entier et je regarde à chaque ce que ça veut dire que tel truc est dans l’implication bidule à la fin j’arrive sur un truc du type pxyzt et en regardant xyzt je peux normalement trouver une combinaison dans le bon ordre qui fait que le truc est dans ce que je veux donc il faut juste trouver le combinateur qui fasse ça, là ça va B est directement dans la liste j’ai regardé un peu la suite et faut en construire d’autres mals du coup ce sera le même genre de logique que pour le premier exo

    Édit2: mais je précise que je me fais PAS DU TOUT confiance franchement le nombre de fois où j’hallucine un truc sans me rendre compte même en me relisant et rerelisant donc je dis tout ça mais possible que ce soit complètement faux et que je me rende pas compte c’est à devenir schizo
  • Georges AbitbolGeorges Abitbol
    @Grothenbiete : Je n'en étais pas encore là, mais merci quand même ! Je me demandais comment tu avais pu trouver B = CK(CCW).
  • grothenbietegrothenbiete
    Ah vu que je parlais de B dans le 3.6 je pensais que tu parlais de celui-là surtout que t’avais demandé la définition de $\exists$.
    En fait je sais pas exactement pour B, je cherche un peu « à reculons » je me dis y aura bien un moment faudra faire passer du y devant le x or tu sais que C quand t’as un truc au milieu il le met devant et colle les bouts à gauche et à droite.
    Donc au lieu d’arriver à yx t’essaies d’arriver à Cxyy par exemple mais tu vois que ça va faire y(xy) donc t’auras à dupliquer à un moment le y et t’auras à l’effacer après par exemple avec K. Donc en fait t’aimerais avoir ça: C(Kx)yy
    Tu sais que tu peux facilement l’avoir si t’as ça: W(C(Kx))y
    Donc faut passer de xy à ça mais en fait ça va parce que concrètement tu vois qu’il faut « isoler » le x de xy et pour le coup en tâtonnant un peu en te disant « combien de lettres je peux caser avant pour agir sur x » et en voyant que K servira à rien et W pas grand chose tu vois qu’il faut mettre un C deux trucs puis xy comme ça t’auras un truc de la forme _(_x)y on est plus très loin du (C(Kx)) faut juste refaire la manip’ un coup donc en te dépliant le truc ça donne CK(_)xy et dans le (_) refaire la manip mais en casant le C cette fois donc en fait: CK(CC())xy
    Du coup de ça t’arrives à _(C(Kx))y et là on est quasiment sûr d’y arriver puisque tu vois qu’il reste qu’à dupliquer le y pour laisser le truc entre parenthèse finir le travail donc avec un W cad W(C(Kx))y
    Donc au final t’auras trouvé CK(CCW)xy ( en remettant W(C(Kx))y dans le bon ordre en rajoutant les C)

    Édit: en fait pour tous les autres c’est un peu comme ça qu’on trouve je pense, essayer de voir à reculons en utilisant les combinateurs d’avant (au début t’as que C W K mais après t’en as d’autres qui se débloquent)
  • christophe cchristophe c
    @GA de mon téléphone : l'algo automatique est le suivant.

    Pour trouver t tel que m=tx faire:

    Pick u,v tel que m =uv
    Trouver r,s tels que u=rx et v=sx
    Retourner W(Cr(Cs))
    Simplifier artisanalement.

    Sinon noSuccessPick faire :
    m=x
    > renvoyer J
    m autre lettre
    > renvoyer Km
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    lol c’est mieux que ma bouillie philosophico-heuristique

    CC: je me permets de te poser une question pendant que j’y suis, sur un autre fil je vous vois utiliser le mot modèle, quelle est la définition formelle de ça ? Je le trouve pas sur Google.
  • christophe cchristophe c
    Un modèle (essentiellement, je prends l'exemple des logiques classiques et intuitionnistes) est une fonction $f$ qui de domaine l'ensemble des phrases, qui associe à chaque phrase un élément de l'ensemble vérité ordonné $V$ des logiques concernées ($\{vrai; faux\}$ pour la classique et une topologie pour l'intuitionniste), qui est morphique pour les connecteurs (ie par exemple la phrase $A\to B$ est envoyé par $f$ sur $f(A)\to_2 f(B)$ où le $\to_2$ désigne l'opération qu'on veut voir s'appeler "implique" entre des valeurs de vérité), et qui "nomme tout le monde" en ce sens que $\forall R(x)$ est envoyé par $f$ sur la borne inférieure pour l'ordre de $V$ des $f(R(a))$ quand $a$ parcourt l'ensemble des constantes et $\exists R(x)$ est envoyé par $f$ sur la borne supérieure pour l'ordre de $V$ des $f(R(a))$ quand $a$ parcourt l'ensemble des constantes.

    En général, on donne une définition plus compliquée, mais ça revient au même.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Merci ! J’ai des problèmes de concentration en ce moment j’arrive plus trop à lire les textes comme ça (surtout que c’est Moi qui l’ai demandé donc bon ...) mais en attendant d’avoir le cerveau qui remarche lol, une question en passant avec ta def de « l’espace » des programmes (combi ?), dans un autre fil toi ou GBZM je sais plus, parlez de logique minimale, est-ce que ça peut s’obtenir avec le genre d’espace que tu définis au début mais en mettant pas les mêmes combis de base ? Genre juste J ou C par exemple ? Ça fait fourre-tout de questions à droite à gauche qui se dispersent mais c’est pas pour te faire écrire inutilement quand je peux j’essaie vraiment de « comprendre un peu tout ça » :-D
  • christophe cchristophe c
    Oui, K,C,W réalisent la logique dite minimale (elle n'a rien de minimale, vu que ce que les gens appellent "logique minimale" est en général "la logique intuitionniste" (à epsilon près), mais c'est une autre histoire).

    La logique "minimum" parmi celles étudiées avec énergie par les chercheurs est la logique linéaire intuitionniste (ou pas intuitionniste, à ce niveau l'intuitionnisme ne change pas grand chose), qui est réalisée par les combinateurs C,B où :

    $$\forall x,y: Bxy=yx$$

    Mais on peut retirer $B$ et se contenter de : $C,B',Z, K'$ où

    $$\forall x: B'x= xZ$$

    à condition de supposer qu'il y a un objet qui ne sert à rien (en caml, il est noté "()"), noté $Z$, et un compilateur $K'$, qui n'est autorisé d'utilisation que pour réaliser $X\to (1\to X)$, ie qui est la "commodité caml" consistant à programmer $a()$ plutôt que $a$ tout court pour éviter une exécution immédiate.

    Bref, en résumé, vrai, à epsilon près: le combinateur C fait tout le travail dans un monde où $X=(1\to X)$ pour tout $X$. Il suit que l'un des grosses ou bien erreurs ou bien négligences est de ne pas avoir identifié ce problème béant qui consiste à se demander s'il faut ou ne faut pas confondre $X$ avec $1\to X$. Actuellement la question est traitée comme s'il s'agissait d'une question politique, mais on peut espérer que dans quelques décennies, il y ait un peu mieux que ce libre-choix. Par exemple, les catégoriciens (mais ce n'est pas vraiment un choix de leur part, c'est venu après la définition de ce qu'est une catégorie) vont très fortement distinguer $X$ et $1\to X$ (pour mieux le récupérer via des propriétés supplémentaires ajoutées).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Maintenant que tu as l'air alerte, je vais te poster quelques "calculs" peu compréhensibles quand on n'est pas dans "l'entre-soi" de cette discipline. Parfois je parlerai "du type de" telle expression, sans même avoir précisé qu'on les a typé (sinon, c'est très long à écrire).

    La logique intuitionniste (appelée minimale parce qu'on ne dispose pas d'un langage riche, mais je choisis de tout passer au second ordre, donc les connecteurs sont définissables et on peut tout faire avec $\to$) est réalisée par $K,W,C$ et réciproquement tout énoncé réalisé par eux est un théorème de LI

    Si tu enlèves $W$ tu te retrouves avec une logique qui ne porte pas de nom à ma connaissance parce qu'elle est "bancale" : en effet, il y a des difficultés à rendre concrète toutes les abstractions, ie tous les $[x\mapsto m]$ (qui sont appelés $[\lambda x(m)]$ en lambda calcul. De plus on a gardé $K$, ce qui ajoute à la bancalité.

    L'approche naive consiste à prendre juste $C$ et un combinateur $G$ tel que $\forall x,y,z: Gxyz = xzy$ (autrement dit, un permutateur). Ca donne la logique linéaire.

    On obtient cependant le même effet en prenant $C,B$, avec $\forall x,y: Bxy=yx$

    $B$ est le réalisateur de tous les énoncés de la forme $A\to ((A\to B)\to B)$. De plus $B$ est ce que j'appelle (je ne sais pas s'il y a un vrai nom) "elicut-blanc". Autrement dit, quand il est présent quelque part et pas exécutable, il induit un enchainement qui ne perd aucune sous-formule. Plus précisément : $Bu$ est de type $(A\to B)\to B$ quand $u$ est de type $A$ et $B$ tout court ne pose pas de problème, ce qui fait qu'on ne perd rien. Par ailleurs dès qu'il y a deux arguments ou plus, il s'exécute (ie $Buvw...:=vuw...$)

    Un autre exemple de combinateur elicut-blanc est celui que je nomme $M$ (attention, j'ai tout refait, je n'ai rien lu, donc, mes noms ne correspondent pas forcément à la littérature officielle) qui marche comme suit : $$\forall x,y,z : Mxyz := x(zy)
    $$ À partir de 3 arguments ou plus, il est exécutable, mais tant qu'il a 1 ou 2 arguments, il ne l'est pas. Et bien quand il en a deux, ie $Muv$, on est face à $u$ de type $B\to C$ et $v$ de type $A$ et le résultat $Muv$ est de type $(A\to B)\to C$, on n'a donc rien perdu.

    De même les combi $K;W$ sont elicut-blancs.

    Il n'en est pas du tout de même par contre pour $C,D,G$. Par exemple, $Cuv$ de type $A\to C$ quand $u$ de type $A\to B$ et $v$ de type $B\to C$ fait disparaitre $B$.

    Je ne connais pas d'exemple de jeux de combinateurs qui soient tous elicut-blanc et pour lesquels il est facile en LL de prouver qu'il la réalise. Il est probable qu'il n'en existe pas (sinon la vie serait belle, on prouverait l'élimination des coupures à vitesse constante).

    J'en reviens à $B,C$. Question: quelle est au juste la "puissance de $C$ là dedans. Et bien il fait presque tout dans le sens suivant, je t'énonce un théorème et je te laisse le prouver (ce n'est pas très dur).

    Théorème: soit $P$ un théorème linéaire (resp affine) écrit avec des lettres et des implique. Alors il existe $Q$ qui est réalisé par un terme uniquement construit avec des $C$ et des $B'$ et qui s'obtient comme suit. Pour chaque lettre $x$ présente dans $P$, on l'a juste remplacée par $x_1\to x_2$. De plus, on a utilisé $B'$ uniquement avec des types $[(a\to a)\to Y] \to Y$ où $a$ est UNE LETTRE (et $Y$ une formule).

    Exercice: prouver ce théorème. Remarque: ça donne, en l'appliquant une jolie définition des preuves des théorèmes de maths sous forme de "petits diagrammes" très harmonieux.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Wesh, ce qui s’est passé avec le site c’etait de la maintenance ou un bug ? (D’ailleurs il y a des projets pour mettre un peu à jour le site ? en-dehors du forum j’ai l’impression que tout est laissé à l’abandon)
    Pour revenir au sujet, j’ai eu un peu de temps donc avant d’attaquer tes derniers pavés je me suis mis à jour en continuant là où je m’étais arrêté.
    du coup j’ai continué les exos du début que j’avais sautés, dis-moi si ça débloque pas stp.

    3.7.1: CB(CC(BK))
    3.7.2: D(BJ)(BJ)
    3.7.3: CB(CW)
    Ensuite j’ai lu une partie des pavés après, je pense avoir compris le plus gros « dans les grandes lignes » par contre la partie sur $\otimes$ je ne suis pas sûr de voir, désolé d’être « pragmatique » mais la définition formelle de $\otimes$ c’est quoi ? De ce que j’ai compris la phrase $X\otimes Y$ c’est l’ensemble des t tels que $\exists x\in X, \exists y\in Y: t=Txy$ et $\otimes$ tout seul c’est une application de ExE dans E telle que pour tout x y dans X Y, $\otimes (x,y)=Txy$. Du coup pour X et Y deux phrases $X\otimes Y$ c’est l’image par $\otimes$ de (X,Y) c’est ça ? Bon si oui je vais essayer de relire le truc sur le produit cartésien.
    Ah et le robot r qui fait rx = $x\otimes x$ c’est WT du coup ?.
    Sinon avec ça je trouve que $(X\otimes Y)\subset X\land Y$ pour la réciproque ça a l’air plus difficile j’ai pas cherché.

    Encore merci pour tes réponses ! J’attaque la suite dès que je peux et que je suis assez « fonctionnel » :-D
  • christophe cchristophe c
    $<<A\otimes B>>$ est une abréviation de $<<\forall X[(A\to (B\to X))\to X]>>$, c'est tout. Mais dans notre contexte, c'est équivalent à $A\wedge B$, car:

    $(A\wedge B)\leq (A\wedge B)\otimes (A\wedge B) \leq A\otimes B$ et

    $A\otimes B\leq A$ et $A\otimes B\leq B$, donc $A\otimes B\leq A\wedge B$.

    Les réalisateurs qui permettent de réaliser ces choses là sont fabriqués avec $K$ et $W$. C'est pourquoi, j'ai décidé de séparer les combinateurs "inoffensifs" et ces deux-là, obtenant un système, au choix à 3 ou 4 générateurs et non à 2. Dans les livres tu liras souvent la paire de générateurs complète $\{S;K\}$ où $S$ fonctionne comme suit:

    $$Suvt := (ut)(vt)$$

    autrement dit, c'est $Suv := W(Cu(Cv))$. D'ailleurs, foys en parle souvent, il y est même revenu dans le présent fil je crois en faisant la promotion d'un combinateur que je noterai $Q$ qui agit comme suit:

    $$Qxyzt:=(xz)(yt)$$

    autrement dit, $Q:=CC(CC)$.

    Mais le fait que $S$ embouteille l'efficacité de $W$ m'a conduit à le retirer des générateurs que je promeus. Cela, dit, si on veut aller par là (vers un petit nombre de générateurs), je te mets un exercice. Tu verras que foys était près du but, mais l'a "raté de peu" (si on fait semblant de croire qu'il pousuivait un but, ce qui est évidemment fautif): l'un des plus joli que j'ai trouvé dans la famille "il suffit de l'avoir" est le suivant, que je note $R$:

    $$Ruvxy:=(uy)(vx)$$

    qui est "presque" celui de foys à un chouya près.

    Et bien il a l'avantage suivant, de permettre les deux théorèmes suivants:

    Théorème1: $\{R;J\}$ permet de construire tous les combinateurs linéaires, entre autres $D;C;B; M; etc$

    Théorème2: Tout mot peut se mettre sous une forme "sans parenthèses" dès lors qu'on dispose de $R;J$, ie le mot peut être écrit sans parenthèses dès lors qu'on dispose de la seule priorité à gauche.

    qui ont comme corollaires suivants, les conclusions logiques :

    Cor1: la logique linéaire est engendrée par modus ponens à l'aide du seul schéma d'axiomes, en plus des phrases de la forme $X\to X$:

    $$ (A\to (B\to D))\to ((C\to B)\to (C\to (A\to D))) \ (**) $$

    Et même mieux:

    Cor2: pour tout théorème de science $P$, il existe une suite finie $H_1,..,H_n$ telle que :

    a) $H_1 =[ (H_2\to (H_3\to (.....\to H_n\to P)...) ]$

    b) Chaque $H_i$ est un axiome ou une phrase de la forme (**) ou de la forme $X\to X$


    A noter que $\{R;J\}$ n'est pas la seule paire à avoir ces propriétés. Par exemple il y a aussi $\{D;H\}$ où :

    $$Dxyz:=x(yz); Hxyz:=yzx$$

    mais le côté amusant de $R$ c'est que son copain est $J$.

    J'ignore s'il existe un singleton $\{Y\}$ qui aurait cette propriété, mais si c'était le cas, on aurait alors une correspondance canonique entre théorèmes et nombres entiers, puisque les garanties s'écriraient toutes comme suit:

    $$ YYYYYYYYYYY.....Y$$

    Ainsi chaque théorème aurait une sorte de numéro magique (le nombre de $Y$ écrits). Je serais alors étonné que les nombres premiers ne jouent aucun rôle.

    Avec $\{R;J\}$ ou $\{D;H\}$, on a un peu le même phénomène, mais un peu "trop artificiel" ou pas assez puriste, puisqu'il faut écrire en binaire. Par exemple le théorème garanti par DDHDHDDDDHHHH est le théorème numéro: 1101011110000.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Il doit y avoir un problème dans ta définition ou de $A\otimes B$ ou de $A\land B$ car si tu définis $A\otimes B$ par $\forall X: (A\to (B\to X))\to X$ Vu que c’est la définition que t’as donnée à $A\land B$ dans ton premier post y a aucune équivalence à montrer c’est exactement la même chose.
  • christophe cchristophe c
    C'est parce que le thème du fil étant la logique intuitionniste, le tenseur et la borne inf se confondent. D'un PC je preciserai (je l'ai déjà souvent fait dans d'autres posts).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    @grothen: si on change le paradigme, particulièrement si on change les robots disponibles, il y a des changements (importants) au niveau des "et" et des "ou".

    Par exemple: soit $E$ un ensemble muni d'une opération qui est juste commutative et associative avec un élément neutre. Continuons de définir :

    $$(A\to B):= \{x\in E\mid \forall y\in A: xy\in B\} ; (\forall x\in Toto: R(x)) := [IntersectionDesR(x),x\in Toto]$$



    Non seulement en l'absence de robots, tu as beaucoup moins de théorèmes, mais en plus, il n'est pas possible d'ajouter l'hypothèse qu'on a des robots "riches comme avant" sans provoquer $card(E)=1$. C'est très facile à voir:

    $$x = kxy = kyx = y$$

    en ajoutant $k$ par exemple.

    La définition de $A\otimes B$ comme étant telle que $\forall A,B,C: [(A\otimes B)\to C ] = [A\to (B\to C)]$ est universelle, et est produite par

    $$(A\otimes B):= \forall X: [(A\to (B\to X))\to X]$$

    Mais ce qui change radicalement est que $A\otimes B$ n'a plus rien à voir avec $A\cap B$.

    En logique intuitionniste et classique, d'ailleurs, ce n'est pas non plus $A\cap B$ qui "représente bien" le "et", c'est le produit cartésien (qui se confond "un peu bêtement" avec le produit tensoriel dans ces logiques car on dispose des projecteurs $BK$ et $B(KJ)$ qui vérifient $BK(x\otimes y) = x$ et $B(KJ)(x\otimes y)=y$.

    Mais dans le présent fil, je traite du "bête et méchant" lambda-calcul et des premières idées "naives" qui permettent de comprendre la CCH. Dans un tel cadre, le produit tensoriel est le produit cartésien, $A^2=A$ et $\wedge = \otimes$. Par contre, l'opération n'est "rien du tout" (elle n'est ni associative, ni commutative).

    Dans d'autres cadres, $A\wedge B$ ne peut pas être défini, il faut l'ajouter. Dans "le bon cadre", on peut le prouver (qu'il est inaccessible). Alors que $\otimes$ ne pose aucun problème (mais s'obtient à partir de $\wedge$).

    Si la logique linéaire t'intéresse, ce n'est pas trop le bon fil. Je te donne malgré tout sa définition (dans sa version écrite juste avec implique) car elle est très courte. Les axiomes sont $[A]\vdash A$ et la seule règle de déduction est:

    $$ \frac{ L_1\vdash A\ ; \ L_2\vdash (B\to C) }{L_1+L_2\vdash (A\to B)\to C}$$

    avec la convention que les $L_i$ sont des listes non ordonnées, que A,B,C sont des formules et que la définition par récurrence de $\vdash$ est donnée par :

    $$ A\to (L\vdash B) := ((A+L)\vdash B)$$

    Visuellement, c'est très simple à comprendre. Pour prouver $H_1\to (H_2\to (.....(H_7\to ((A\to B)\to H_8\to (....\to P)..)$, que l'on regarde comme écrit en ligne, le prouveur a le droit:

    1/ de permuter les hypothèses (sceptique inactif en réponse)
    2/ "couper" le ruban: ie proposer au sceptique au choix de lui prouver ou bien $H_1\to (H_2\to (.....(H_7\to A)...)$, ou bien $B\to (H_8\to (....\to P)..)$

    Et c'est tout. Le prouveur gagne quand il arrive à $X\to X$.

    Sur le plan CCH, les théorèmes sont les phrases réalisables avec C,B (ou encore $R,J$, etc). Au passage, les théorèmes écrit juste avec UNE SEULE lettre et $\to$, qui sont des théorèmes forment un ensemble NP-complet (donc tu vois, ne pas se fier aux apparences :-D )


    Pour en revenir à $A\wedge B$, $A\times B$ et $A\otimes B$ les distinctions de fond sont entre $\wedge$ et les autres: $A\wedge B$ est en quelque sorte l'ensemble des preuves qui garantissent aussi bien $A$ que $B$. Rien à voir avec le fait d'avoir d'un part une preuve de $A$ et d'autre part une preuve de $B$. Le produit cartésien n'est tout simplement "pas pertinent", mais c'est une autre affaire (c'est une sorte de produit tensoriel "à la condition d'avoir K,W", et dans la vraie vie, c'est un produit tensoriel "vu d'un autre monde"). On parvient parfois (par exemple avec les espaces vectoriels) à bien différencier cartésien et tensoriel), mais sur le plan logique il y a une petite arnaque de "changement d'échelle". Cette "erreur" est loin de tes préoccupations du moment j'imagine, je la signale juste parce qu'elle a empêché la "quantisme" (ie d'avancer pour marier logique et mécanique quantique).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Comme je te l'ai dit (grothen), il y a un article qui prouve que l'ensemble des théorèmes de logique linéaires propositionnels et écrit seulement avec une lettre et le signe => est NP-complet.

    L'exercice suivant est par contre très facile: l'ensemble des théorèmes propositionnels de la logique affine écrits avec juste le signe => et des lettres est NP-complet.

    précision: cet ensemble est l'ensemble des phrases réalisées par C,B,K (par exemple) ou encore par R,J,K.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    Je passe juste pour dire que je n’abandonne pas le fil et les réponses que tu m’as faites (peut-être que tu t’en fous mais sait-on jamais par politesse voilà) j’ai juste pas le temps en ce moment (ces jours-ci quoi) voilou :-D
  • christophe cchristophe c
    Ne t'inquiète pas, je me connecte aussi assez difficilement ces temps-ci.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    LOOOOL mais les hasards dans la vie parfois, Abitbol fait un topic sur ta thèse ça me fait lire des trucs sur la mécanique quantique je trouve ça stylé, je rencontre au même moment Alain Connes par hasard, je regarde du coup après des vidéos d’Alain Connes je tombe sur la vidéo d’interview Laurence Honorat, je vois que le type qui l’interview c’est un certain Khelif (kabyle d’origine ?) Je remarque c’est le nom du type qui chapeautait ta thèse et je ne sais pas quelques jours plus tard c’est-à-dire à l’instant je le croise dans un café. Quelles étaient les chances alors que j’ai jamais rencontré de mathématicien dans ma vie que juste après avoir lu le topic d’Abitbol sur ta thèse je tombe sur Connes et quelques jours après avoir découvert le visage de Khelif je tombe sur lui ? :-D
    Bref anecdote en passant, c’est dommage parce que je partais au moment où je le croise.

    [Les noms propres prennent toujours une majuscule ! AD]
  • christophe cchristophe c
    :-D le monde est petit et je vais dire à Anatole de moins trainer dans les bars. Moi si tu me croisés ces jours ci ce sera vraiment un miracle car je suis en train de farfouiller dans les boutiques de légumes grillés à l'huile d'olive dans les vieilles ruelles de Nice :-D . Pour info, Alain Connes ne serait peut être pas content de se voir re-orthographier en promoteur de cigarettes.

    Après si tu traines dans les quartiers de la rive gauche fac-bobo-GE de Paris ce n'est en fait pas si grand. Donc la proba a priori est moins faible que tu crois. Mais elle reste faible.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    « Après si tu traines dans les quartiers de la rive gauche fac-bobo-GE de Paris » 
    J’habite vraiment pas loin du tout pour ne pas dire que je suis en plein dedans :-D et vraiiiment pas loin du tout du café où il était
    Mais ça va tu peux lui laisser un peu de liberté il était sagement assis à faire des maths sur une feuille blanche A4 il était pas en train de se saouler au comptoir (il était que 15h aussi c’est un peu tôt (ou trop tard ?) pour ça)
  • Georges AbitbolGeorges Abitbol
    @Christophe : Je n'arrive pas à me rendre compte de si, quand il y a plusieurs choix pour exécuter un truc, si l'ordre dans lequel on exécute les trucs a une importance.

    Sinon, tu as dit que tu allais écrire un truc pour exécuter ces petits programmes ; j'ai moi-même essayé, et je me mords les doigts. Tu as un moyen simple de faire ça ?

    Je représente mes robots par des arbres dont les noeuds qui ne sont pas des feuilles sont des $*$, etc. Je fais ça en C et comme les pointeurs me traumatisent depuis que j'ai appris à les utiliser en première année, j'ai très mal à la tête. Et puis j'ai galéré à trouver quelque chose qui marche pour ton $D$ ci-dessus et mon exécuteur dit que je me suis trompé, alors je ne sais plus où trouver mon erreur.
    En plus, comme les parenthèses rendues superflues par ta convention me rassurent, j'en mets partout. Et, même si je n'y ai pas réfléchi, j'ai l'impression que de coder un truc qui traduit des chaînes de caractères parenthésées selon ta convention en arbres, c'est plus coton que quand toutes les parenthèses y sont...
  • christophe cchristophe c
    Je voulais me reposer un peu (je n'arrête pas d'envoyer des mails guerrier pour des affaires de boulots), mais ok, je te le ferai (attention, je le fais en caml, c'est très fluide à programmer, mais ce ne sera pas du C).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Georges AbitbolGeorges Abitbol
    Non, non, t'inquiète, ça m'amuse de le faire en C, je voulais savoir si tu avais des astuces pour faire un truc court.
  • christophe cchristophe c
    En te mettant un code caml (le caml est très simple à lire), tu y verras les astuces facilement pour ne pas y passer 3H. Par contre, il y a des implémentations fonctionnelles du caml** qui seront peut-être difficile ensuite pour toi à transformer, mais je te mettrai un panel au sein duquel une bonne partie sera traductible presque mot pour mot.

    Par exemple, en caml, on programme le lambda-calcul en une ligne pure par:

    type terme = NomOuautreStructure of nimporteKoi | L of (terme->terme) | A of terme*(terme list)

    Et la fonction qui applique un terme à un autre par:

    let ap x y =
    match x with
    | Nom............... -> cequiteplait
    | L f -> f y
    | A(u,m) -> A(u,y::m)

    Et si tu veux éliminer les coupures d'un coup, tu peux modifier légèrement:

    type terme = L of (terme->terme) | R of (Simple * terme)
    and Simple = Hypo of int (ou autre, disons "atome") | A of (Simple * terme)

    Et la fonction qui applique un terme à un autre par:

    let ap x y =
    match x with
    | L f -> f y
    | R u -> R (A(u,y))
    |lerestesttrivial

    De sorte que quand tu enregistres une preuve, il ne se donne même pas la peine de la mémoriser, il l'enregistre DIRECTEMENT sous une forme sans coupure (une coupure est un couple A( L f, u) présent syntaxiquement au lieu d'avoir exécuté "f (u)" )

    En C, les combinateurs se programment avec la même facilité qu'en caml, par contre, ce que je viens de te raconter est plus délicat à traduire dans la "pauvreté impérative" du C.

    Autre astuce, pour éviter des usines à gaz de contructions de phrases, tu considère les entiers comme des phrases, le nombre (2n) étant d'office a phrase (4n+1)=>(4n) et le nombre (2n+1) étant d'office la phrase (4n)=>(4n+1) (je fais ça pour préserver les polarités, tu peux aussi faire négligemment que n est la phrase (2n+1)=>(2n), mais c'est plus tristounet)

    A noter, que tu t'apercevras (phénomène peu connu, hélas), toute preuve prouve tout énoncé en ce sens que la procédure très simple d'exécution enregistre naturellement les axiomes à utiliser pour obtenir l'implication. Par exemple, tu peux t'amuser à exécuter une réalisation de Ascoli sur l'énoncé "il existe au moins un entier parfait impair" et regarder ce que ça donne. Bien évidemment l'activité des matheux consiste à chercher, face à un énoncé E, à proposer un terme tel que tous les axiomes qui seront enregistrés seront "acceptables" (et même de la forme X=>X).

    Pour confronter un terme à un énoncé:

    type env = Fond of phrase | Pile of (terme * env)

    let rec execute t e =
    match (t,e) with
    | (t, Fond atome) -> let h=>c la phrase mise** sous forme d'implication qui est synonyme de atome in execute t (h implique c)
    | (Hypo s, Fond z) -> Enregistrer l'axiome qui dit que s implique z (plus précisément, mais bref, que s est inclus dans z (pour les puristes))
    | (L f, Fond (a implique b)) -> begin prendre a; execute (f (Hypo a)) (Fond b) end
    | (L f, Pile (u,suite)) -> execute (f u) suite
    | (A(u,v),e) -> execute u (Pile(v,e))
    | (Hypo (a implique b), Pile(u,suite)) -> begin execute u (Fond a); execute (Hypo b) suite end

    Cette fonction te donne (quand tu lances execute t (Fond p)) ce qu'il suffit de supposer à minima pour que la preuve t prouve l'énoncé p. De plus, la preuve livrée est sans coupure!! Par ailleurs

    Bon, j'ai tapé le post à toute vitesse sans avoir caml à disposition, je le copie-collerai dans caml un peu plus tard et te donnerai quelques détails. Je fais peu de faute en général, donc, si ça se trouve, à quelques espaces éventuellement oubliés, ça doit tourner.

    L'avantage avec les entiers c'est que toute phrase est une implication.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    @GA: je t'ai tapé un code cmal complet et pratique, je te le copie-colle ci-dessous, mais préviens-moi de où tu en es avec le caml AVANT que je ne réponde à tes demandes. Le caml n'est pas très long à apprendre (environ 30mn + 1H de pratique), mais je ne sais pas si tu l'as fait ou pas.


    type term =  L of (term->term) | R of simple

and simple = Hyp of int | A of (simple * term)

type magic = V of int | L2 of (magic -> magic) | Ap of (magic*magic)

type env = Fond of int | Pile of (magic * env)

type logicom = C | B | W | K | J | Op of (logicom * logicom) | Va of int

let pointeur = ref 1
let listeaxiomes = ref []

let nouveau() = begin incr pointeur; (!pointeur) end
let ajouteAuxAxiomes x = let m = (!listeaxiomes) in listeaxiomes := x::m

let pair n = ( n mod 2  = 0 )

let hc n = if pair n then (2*n+1, 2*n) else (2*n, 2*n+1)
let hy n = let (a,b) = hc n in a
let co n = let (a,b) = hc n in b


let ap u v = match u with 
 | L f -> f v
 | R w -> R (A(w,v))
 
let rec traduire t = match t with 
 | V n -> R (Hyp n)
 | Ap (u,v) -> ap (traduire u) (traduire v) 
 | L2 g -> let f x =  traduire (g (detraduire x)) in L f
 
and detraduire u = match u with 
 | L f -> let g x = detraduire (f (traduire x)) in L2 g
 | R(A(x,y)) -> Ap (detraduire (R x), detraduire  y)
 | R(Hyp n) -> V n
 

let rec execute t e = match (t,e) with 
 |(Ap (u,v),e) -> execute u (Pile(v,e))
 |(L2 f, Pile(u,e)) -> execute (f u) e
 
 |(V n, Fond s ) -> ajouteAuxAxiomes (n,s)
 
 |(V n, Pile(u,e)) -> 
  begin 
  execute u (Fond (hy n)) ; 
  execute (V (co n)) e
  end
 |(L2 f, Fond s) -> let (h,c) = (hy s,co s) in execute (f (V h)) (Fond c) 

 
let rec excu t m = match (t,m) with 
 | (J,x::suite) -> excu x suite
 | (B, x::y::suite) -> excu y (x::suite)
 | (W, x::y::suite) -> excu x (y::y::suite)
 | (K, x::y::suite) -> excu x suite
 | (C, x::y::z::suite) ->excu y ((Op(x,z))::suite)
 | (Op(u,v) , pil ) -> excu u (v::pil)
 | (q, li) -> (q, excus li)
 
and excus m = match m with 
 | [] -> []
 | x::suite -> let (r,belle) = excu x [] in (souder r belle) :: (excus suite)
 
and souder t m = match m with 
 | [] -> t
 | x::suite -> souder (Op(t,x)) suite
 

 
 
let sr u v = Op (W, (Op(  Op(C,u),  Op(C,v) )   ) ) 

 
let rec lambda n t = match t with 
 | Va p -> if p=n then J else Op(K,Va p)
 | Op(u,v) -> let (u1,v1) = (lambda n u, lambda n v) in sr u1 v1
 | _ -> Op (K, t)
 
 
 
let rec purversmat  t = match t with 
 | V n -> Va n
 | L2 f -> let p = nouveau() in lambda p (purversmat  ( f (V p)) )
 | Ap(u,v) -> Op(purversmat u, purversmat v)
 


let rec netoi1 t  = match t with 
 | Op(W,K) -> J
 | Op(W, Op(K,x)) -> x
 | Op(C,J) -> J
 | Op( Op(C,x), ((Op(K,y)) as z) ) -> z
 | Op (Op (C,x) , J ) -> x
 | Op (Op(C,(Op(K,v))), u ) -> Op(K, Op(u,v))
 | Op(x,y) -> Op(netoi1 x, netoi1 y)
 | _ -> t
 
let rec netoi t = let r = netoi1 t in if r=t then r else netoi r
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Georges AbitbolGeorges Abitbol
    Merci beaucoup pour ce code ! Ben en fait je ne connais pas du tout le caml. Je vais m'y mettre, du coup ! Mais attends, là, ton code, tu lui donnes une phrase bien parenthésée (i.e. un mot avec des lettres et des parenthèses où on suppose qu'entre deux choses, il y a le $*$ de la combi) et il essaie d'exécuter un $C$, un $W$ ou un $K$ ? Parce que moi, j'ai déjà un code assez long qui prend une phrase bien parenthésée, qui renvoie un arbre (et ce n'est déjà pas une mince affaire) et puis après, je me suis pris la tête.
    Du coup, pour ma question de s'il y a deux exécutions possibles dans une même phrase, est-ce que l'ordre importe ?
  • christophe cchristophe c
    Avec le caml, on n'a pas tous ces problèmes (apprends-le, c'est très simple). Mon code te donne 4 trucs (+ quelques fonctions de confort):

    1/ implémentations des termes uniquement normaux (sans coupure) (on dit sans redex chez les spé) (terme et simple)

    2/ implémentations des termes quelconques (magic)

    3/ implémentations des termes écrit avec C,W,K,B,J et sans variables ni lambda (logicom)

    4/ Traductions des uns dans les autres (traduire, detraduire, purversmat)

    5/ Exécution des termes quelconques (execute), avec production de "la phrase maximale prouvé par lui" (quand il normalise)

    6/ Exécution des termes logicom (excu)

    7/ une chtite fonction de nettoyage (netoi), non optimisée

    J'ajouterai la transformation de tout ça en chaines de caractères

    Ce sont les fonctions execute et excu qui font le paradigme de Krivine par exemple.

    (C'est sûr que si tu grilles des heures avec des traductins d'expressions, tu vas vite en avoir marre).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Georges a écrit:
    Du coup, pour ma question de s'il y a deux exécutions possibles dans une même phrase, est-ce que l'ordre importe ?

    Le LC est "confluent" (en gros, ça te répond que non l'ordre "ne devrait" pas avoir d'importance à la fin). Mais attention, ça, c'est juste un petit théorème un peu anecdotique car ne concerne que les modèles où on n'a rien ajouté "d'extérieur". Sinon, la notion de confluence est même sans intérêt en plus d'être "vraie" ou "fausse".

    Mais de toute façon, moi, je parle "d'exécution" (qui est en elle-même aussi intéressante que le résultat), et j'applique récursivement la chose suivante:

    let rec normalise (u.v) =

    if le terme t:= u.v est un redex*** alors traite-le, sinon renvoie récursivement (normalise u).normalise v)

    Ca s'appelle "la réduction gauche". Il y a un théorème qui dit qui si un ordre d'exécution quel qu'il soit termine alors l'ordre gauche termine. Mais comme je n'ai pas implémenté "normalise", mais plutôt l'exécution avec piles, ça ne voit pas directement dans le code (enfin presque), puisque l'appel récursif est remplacé par l'utilisation de la pile.

    **un redex est un terme d'une des formes clé K.u.v; C.u.v.x; etc dont on veut qu'ils deviennent immédiatement par exemple u; v.(u.x); etc
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • grothenbietegrothenbiete
    J'ai passé ma période de crise de l'autre topic, j'ai le temps cet après-midi de continuer un peu les maths "fondements et tout". Dans un bar la dernière fois j'avais entendu deux personnes parler de Ocaml et ils en avaient dit pas mal de bien en plus du coup avec ce topic ça me fait envie d'apprendre un peu les langages de la famille de haskell. Mais de ce qu'ils disaient ils comparaient haskell et caml et ils disaient que haskell était moins "contraignant" mais bon j'imagine que les deux se ressemblent assez pour que ça change rien d'apprendre l'un ou l'autre surtout "à mon niveau" (je veux pas faire un jeu avec).
    Pour apprendre au moins la syntaxe openclassrooms ça va ? https://openclassrooms.com/courses/apprenez-a-programmer-en-caml
    Là y a à peu près ce qu'il faut, je veux dire il manque pas de "gros chapitre" ?

    Édit: bon comme je suis parti faire d’autres trucs je suis toujours au point mort en caml, j’ai trouvé ça sur Google: https://caml.inria.fr/distrib/books/llc.pdf

    Ça fait quasiment 400 pages, tu dis qu’on peut apprendre caml en 30mns pour la partie théorique, du coup qu’est-ce qui vite fait faudrait prendre dedans ?

    Edit 2: bon j’ai commencé à feuilleter vite fait mais le truc est super long quand même.
    Juste, j’ai une question en parcourant et je trouve qu’ils sont pas clairs dessus (et je peux pas vérifier j’ai pas caml sur mon portable), pour caml c’est pareil:
    Let f a =
    let g b = a + b in
    g;;
    Et:
    let f a b = a + b;; ?
    Du coup pour caml on « identifie » $(E^{F})^{G}$ et $E^{G\times F}$ ?
  • christophe cchristophe c
    @Georges, si tu veux apprende le caml, je te copie-colle une liste de fonctions facilement reconnaissables que je viens de taper pour toi (ne t'inquiète pas, ça a dû prendre moins de 20-30mn, c'est l'avantage du caml, sans compter que "taper en caml est très réposant" ).

    Les majuscules sont très importantes en caml, elle te permettent de créer des types en tout genre. Il ne faut les utiliser que pour ça. Lesmots utilisés (par exemple "Vide" ci-dessous, sont à ton libre choix).

    Par exemple, si tu veux créer un type liste d'entiers, tu tapes:

    type liste = Vide | TeteDeListe of ( int * liste )

    et quand tu taperas la fonction

    let f m = match
    | Vide -> fais tout exploser
    | TeteDeListe (u,v) -> u

    la fonction f te renverra le premier terme de la liste.
    type entier = Sd of entier | D of entier | Nul

let rec suc a = match a with 
 | Sd x -> D (suc x)
 | D x -> Sd x
 | Nul -> Sd Nul
 
let rec moitie a = match a with 
 | Sd x -> x
 | D x-> x
 | Nul -> Nul
 
let rec somme a b = match (a,b) with 
 | (Sd x, Sd y) -> D (suc (somme x y ))
 | (Sd x, D y) -> Sd (somme x y)
 | (D x, D y) -> D (somme x y)
 | (Nul, x) -> x
 | _ -> somme b a

let rec produit a b = match (a,b) with 
 |  (D x, y) -> D (produit x y)
 | (Sd x, y) -> let r = produit (D x) y in somme r y
 | (Nul, x) -> Nul
 | _ -> produit b a
 
exception Sol
 
let rec prev a = match a with 
 | Nul -> raise Sol
 | Sd x -> D x
 | D x -> suc (D (prev x))

let rec factorielle a = match a with 
 | Nul ->Sd Nul 
 | _ -> let b = prev a in produit a (factorielle b)
 
let rec puissance a b = match b with 
 | Nul -> Sd Nul
 | _ -> let c = prev b in produit a (puissance a c)
 
 
let pair x = ((x mod 2)=0)

let rec traduire n = match n with 
 | 0 -> Nul
 | _ -> if pair n then D (traduire (n/2)) else Sd (traduire (n/2)) 

 
let rec panel a b f g i= if b<a then i else 
 let c = b-1 in g(panel a c f g i)(f b)
 
let somme a b f = let g u v = u+v in panel a b f g 0
let produit a b f = let g u v = u * v in panel a b f g 1


let rec hacher m = match m with 
 | [] -> ([], [])
 |x :: suite -> let (a,b) = hacher suite in (x::b, a)
 
let rec catalogue a b = match (a,b) with 
 | [], x -> x
 | x,[] -> x
 | x::li1, y::li2  -> 
  if x<y 
  then x :: (catalogue li1 b) 
  else y :: (catalogue a li2)
 
 
 
let rec tri m = match m with 
 | [] -> m
 | [x] -> m
 | _ -> let (a,b) = hacher m in catalogue (tri a) (tri b) 
 
 
let rec prochain n f = if f n then n else prochain (n+1) f
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Précision: une grosse partie des fonctions (les deux premiers tiers) forment un kit d'arithmétique rapide.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe cchristophe c
    Pardon, je ne relis qu'à l'instant ton post initiateur des derniers échanges.
    GA a écrit:
    Et, même si je n'y ai pas réfléchi, j'ai l'impression que de coder un truc qui traduit des chaînes de caractères parenthésées selon ta convention en arbres, c'est plus coton que quand toutes les parenthèses y sont...

    En fait, non, j'avais le même souci de flemmardise il y a 30ans avec mes premiers PC. Voici une astuce paresseuse, mais rapide:

    pour traduire une expression bien parenthèsée (ou pas d'ailleurs :-D ) :

    rechercher dans la chaine s un sous-mot $x*y$ de longueur 3 (ie une suite de 3 atomes sans parenthèses), la remplacer par un "fresh" atome t, ce qui donne la chaine s', traduire la chaine s' et remplacer t par ce que tu as envie que veuille dire $x*y$ dans $s'

    Même principe pour les chaines où des parenthèses sous-entendues apparaissent.

    C'est 3 lignes de programmation.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • samoksamok
    Pourquoi 3 ?

    S
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!