Logique intuitionniste et CCH
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 $
3.7.2/ $(A\vee \to (A\cup $
3.7.3/ $(A\cap \to (A\wedge $
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.
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 $
3.7.2/ $(A\vee \to (A\cup $
3.7.3/ $(A\cap \to (A\wedge $
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
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
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 \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.
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 \to (A\cup $ 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$.
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.
@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!!
(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)
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$)
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".
$$ \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.
Édit: je répondais au post sur la démo bancale
$\forall P: (\forall x: (R(x)\to P))\to P$
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 !
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
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...
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
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)
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
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.
En général, on donne une définition plus compliquée, mais ça revient au même.
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).
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 \to $. 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 \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 \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.
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
$(A\wedge \leq (A\wedge \otimes (A\wedge \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 \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.
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 := \{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 \to C ] = [A\to (B\to C)]$ est universelle, et est produite par
$$(A\otimes := \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 \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 := ((A+L)\vdash $$
Visuellement, c'est très simple à comprendre. Pour prouver $H_1\to (H_2\to (.....(H_7\to ((A\to \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).
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.
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]
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.
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)
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...
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.
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 ?
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).
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
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}$ ?
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.
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.
S