20 000$ offerts à qui résout ce problème
Bonsoir à tous,
20000$ sont offerts à qui résoudra ce problème. J’ai juste lu en diagonale mais je pense que cela intéressera des contributeurs ici : https://writings.stephenwolfram.com/2021/06/1920-2020-and-a-20000-prize-announcing-the-s-combinator-challenge/
20000$ sont offerts à qui résoudra ce problème. J’ai juste lu en diagonale mais je pense que cela intéressera des contributeurs ici : https://writings.stephenwolfram.com/2021/06/1920-2020-and-a-20000-prize-announcing-the-s-combinator-challenge/
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
La même chose en français ?
Cordialement;
Rescassol
C'est intéressant, il s'agit de voir si un combinateur particulier (appelé S) à la propriété d'universalité (toute expression reprenant la plupart des combinateurs classiques et bien formée est réductible en combinaisons du combinateur S, qui semble être un combinateur qui distribue un paramètre sur une expression)
Il se fait qu'il est prouvé (c'est Wolfram qui le dit) que toute combinaison de deux combinateurs précis (S et K, K étant un combinateur qui renvoie une constante dans une expression) à cette propriété.
Donc, pour prouver l'assertion, il faut montrer que K se réduit en combinaisons de S.
Je n'ai fait qu'effleurer le sujet, donc je ne sais pas si c'est facile.
Wolfram prétend qu'il a fait pleins de tests et à toujours su réduire les combinaisons en combinateurs S, mais ce n'est pas une preuve.
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Erdos posait aussi souvent des récompenses en fonction de la difficulté de certains problèmes qu'il n'arrivait pas à résoudre, cela allait de 20 dollars à 500 dollars maximum, si mes souvenirs sont exacts.
Il va sans dire que la renommée de celui qui résolvait le problème à 500 dollars était faite et que la récompense était juste de l'argent de poche.
Knuth, pour la découverte d'une coquille dans son AOCP donne royalement 1 dollar hexadécimal, sous forme de chèque.
Il ne me viendrait même pas à l'esprit de l'encaisser, tant le fait d'avoir ce chèque est plus intéressant que l'aspect financier.
À bientôt.
[Juste pour info, l'accent pour Erdos ne passe pas.]
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Toujours est-il que pour le problème en question, 20000 dollars, c'est cheap mais tout le monde n'a pas forcément les fonds nécessaires pour donner 1 million à tout va (même si ce problème est effectivement dur).
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
En fait il faut aussi définir un encodage des fonctions récursives pour montrer la conjecture (donc l'énoncé est un peu vague).
Oui, j'ai vu par la suite que ce n'était pas aussi clair.
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
( A => (B=>C ) ) => ( (A=>B ) => (A=>C) )
oulala, non, cela SUFFIRAIT et comme dit foys, on peut prouver que ce n'est pas le cas.
En fait, le gars présente les choses avec une rhétorique "séduisante", mais produit un problème ouvert extrêmement "habituel", et e, plus de cela avec un degré de flou.
De la sorte même s'il est honnête, des matheux ne peuvent s'investir, pour juste 15000 euros, fournir un travail, lui envoyer la proposition et le laisser "seul arbitre".
Si tu veux une version formelle, on pourrait par exemple traduire en "une" version formelle sa demande comme suit:
"existe-t-il une réduction polynomiale de $EQS$ à $A$?" où :
1/ $EGQ$ est l'ensemble des équations diophantiennes ayant des solutions
2/ $A$ est l'ensemble des couples de mots $(x,y)$ écrits avec juste $S$ tel qu'il existe une beta-eta réduction allant de $x$ à $y$.
Tout intéressantes qu'elles soient, ces questions ne sont hélas pas traitables par autre chose que des informaticiens lambda-calculistes professionnels (ou jeunes "génies" passionnés, MAIS CULTIVES) ou par une des 5 à 10 personnes au monde (dont Foys sur le forum) un peu plus âgée dans le monde qui sur le tard se sont informés, de par leur puissance mathématique inédite, de ce que travaille cette ultra-spécialité.
Pour donner une idée, même parmi les logiciens, très peu connaissent de façon opérable cette spécialité. Par ailleurs, elle est "anonyme" partiellement du fait qu'elle est extrêmement inter connectée avec le monde des geek et des "codeurs bien payés" qui ne déclarent pas sur leur CV connaitre ça, alors qu'il le connaissent (parce qu'ils connaissent d'autres choses plus rémunératrices).
Je dois être un des seuls au monde qui s'intéresse à l'infini ET qui y ait villégiaturé de manière approfondie, et faut voir la raison "baroque" qui m'y a conduit: je recherchais... ce qu'on peut appeler "de la philo", dans des contextes... non habituellement matheux (ie cmt convaincre un non matheux de quelque chose qui est mathématiquement prouvable alors qu'il est de mauvaise foi dans son rôle sceptique; comment convaincre LA NATURE, etc)
En bref, "il achète" à des pros qui gagnent déjà bien leur vie, en vendant des choses comme ça plus standards, une solution à un problème "un peu plus théorique".
=> quelles seraient les applications « pratiques » et/ou philosophique/sur le monde/... de ce résultat s’il était démontré ?
=> alors question vague et vaste, mais plus généralement, toute la théorie des combinateurs, realisabilité, etc, quelles sont les implications pratiques et aussi philo/etc sur le monde que ça a eu ou risque d’avoir ? Ça a l’air quand même très prometteur et à la mode comme thème.
Édit : il existe une version « catégorique » de l’étude des logiques assez « consistantes », quel lien y a-t-il entre ce domaine et par exemple les gens qui bossent sur des topos de réalisabilité, etc. J’ai l’impression mais c’est par manque de connaissances sur la CCH qu’il y a un double étudié par lés catégoricitens ou redécouvert de ce qui est fait dans ce domaine.
Sur le monde, je ne sais pas (le monde va plutôt mal), la CCH est à moyen terme utile pour re-positionner la science dans sa relation avec les maths puisque la CCH (et ce qui l'entoure) éclaire le "rien". Actuellement, dans "A=>A", le "A" apparait 2 fois alors qu'on devrait représenter cette affirmation par une boucle, avec un seul A et une arrête en cercle (qui part de A tourne et revient à A). Quand on veut faire ça "à la main", ça devient brouillon et artisanal. Cette spécialité a tendance à archiver et collecter de réels progrès dans le sens que "rien" et bien représenté par "rien", et est donc incassable.
Les catégories, comme d'autres structures, permettent de faire une sorte de sémantique de ces choses. Mais, les catégories sont "ancien temps" dans le sens qu'elles manifestent cette habitude qu'ont les gens de faire des AR syntaxe-sémantique. Sinon oui il arrive souvent ( mais pas toujours) que les CAT redécouvrent l'eau chaude (en en étant conscients a priori, l'objectif étant compatible avec ça)
Pour ce qui concerne le truc à 20000 dollars, par contre je n'en vois pas l'utilité spécifique, si ce n'est pas progresser dans la connaissance de ces combinateurs. Ca ressemble plus à un hobby de l'auteur qui a l'air de "se démener". De toute façon, S est combinateur "tout pourri" :-D qui inclut 2 pouvoirs distincts (la composition et le clonage).
Tout pourri ?
Il a l'air d'être omniprésent et incontournable dans toutes les présentations que je lis depuis deux jours.
J'ai déjà vu bien plus pourri comme notion informatique (mais pour le cas d'espèce, je n'ai sans doute pas assez de recul, peut-être qu'il y a quelque chose de pourri quand on approfondit la notion).
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Il est rare de tomber (enfin j'imagine) sur de bonnes présentations.
Par ailleurs, voici ma position: séparer les combinateurs par pouvoir, c'st mieux.
La composition : C x y z := y (x z)
Le clonage : W x y := x y y
Le jetage : K x y := x
Le fait de déplacer, commuter: G x y z := x z y
Le "fameux" plongeur : B x y := y x
Le "réalisateur" du RPA : (la syntaxe est spéciale et double, je te la donne si tu le demandes).
Or S fait deux choses à la fois, dont une très importante qui est de cloner.
A la rigueur, ou pourrait lui préférer un R qui agirait comme suit:
R x y z t := x t (y z)
avec lequel on fait aussi tout sauf cloner et jeter.
Sur le plan logique ça correspond à des niveaux de garanties EXTREMENT DIFFERENTS! Par exemple, les déplacements, composition sont réellement inoffensifs (et même inexistant "in some sense" si on n'avait pas nos contraintes physiques d'écriture).
Jeter est DEJA un petit pouvoir "toxique"
Cloner est littéralement explosif, ce qui fait que les maths ne peuvent pas s'occuper du réel et doivent se prononcer seulement sur des énoncés "classiques + immuables + égaux à leur illusion"
(Pour te donner un ordre d'idée, quand tu peux cloner $\forall xR(x)$, tu supposes une seule fois ça mais ça va te donner R(a), R(b), R(c), .... Autre façon de le voir, pour battre Karpov, tu auras le droit de jouer, avec plein de copies de lui-même, etc. Pour battre Nadal, tu pourras arrêter le temps, le faire redémarrer, contrôler sa vitesse de déroulé, etc)
c'était abordé ici avant la fermeture et est peut-être passé inaperçu: http://www.les-mathematiques.net/phorum/read.php?16,2091694,2257736#msg-2257736
Il n'y a pas besoin de "droits de copie/poubelle" quand on a le droit de voyager dans le temps pour corriger ses fautes.
C'est ce genre de résultat qui me fait considérer que la réalisabilité classique n'est pas la CCH mais quelque chose d'autre.
P.S.: Les "vraies" lettres sont plutôt: B=T; C=Q.
Le Pearce réalisé Kriviniennement est "une erreur" (JLK s'en fout de dupliquer) un peu comme "aimer S".
Je détaille:
j'appelle processus la donnée d'un couple $(u,e)$. A gauche (u) on a un terme ou n'importe quoi qui en fasse officie et à gauche un "environnement" (ou n'importe quoi qui en fasse office, du moment que $x+e'$ soit un environnement dès lors que $x$ est un terme et $e'$ un environnement), avec "one-step" évolution suivantes:
1/ comme tu l'imagines pour les termes:
par exemple $(S,a+b+c+e)$ évolue vers $(a, c + (bc) + e )$ ou, autre exemple,
$(K,a+b+e)$ évolue vers $(a,e)$
2/ step d'empilage: $((uv,e)$ évolue vers $(u,v+e)$
3/ Mais là ATTENTION, faut pas faire comme JLK, pour le RPA, autrement dit, faut pas réaliser Pearce
$(CallCC,u+e)$ évolue vers $(u, [RetourVersLeFutur (e)] + RienDuTout)$
Et non pas $(CallCC,u+e)$ évolue vers $(u, [RetourVersLeFutur (e)] + e)$
qui DUPLIQUERAIT l'environnement $e$ (ce qui est soit dit en passant stupide, vu que l'environnement de principe c'est "tout le reste du monde" quand on ne se limite pas aux piles des geeks refugiés H24 dans leur cave à sentir le dessous de bras à pirater NASA et autre)
Par contre, tu peux garder le "step" de "RetourVersLeFutur":
$(RetourVersLeFutur(e),u+e_2)$ évolue vers $(u,e)$ (ce qui jette $e_2$).
Ce que tu réalises est $([A\to Tout]\to Tout)\to A$ et NON PAS $([A\to B]\to
Bon bin, du coup, en répondant à Foys, dreamer tu as les détails du RPA.
$u$ réalise $A$ quand tout $e$ qui agresse $A$ est tel que $(u,e)$ marche
$e$ agresse $A\to B$ quand il est de la forme $a+e$ avec $a$ qui réalise $A$ et $e$ qui agresse $B$
$e'$ agresse $\forall xR(x)$ quand il agresse $R(z)$ pour au moins un $z$
Par ailleurs, le mot "réalise" est mal choisi, il vaudrait mieux parler de "garantir". Dire "robot machin garantit à la phrase bidule"
Enfin, le seule chose que "marche" doit avoir comme propriété c'est que si un process X évolue en ONESTEP evers Y et que Y marche alors X marche.
Les théorèmes de maths sont les phrases qui peuvent être "réalisées" (je préfère garanties) quoique veuille dire (marcher, realiser, agresser) ayant les propriétés ci-dessus.
La CCH est juste la remarque que ce que je viens de faire et affirmer existe et est vrai (tout théorème est garantissable), et en plus de manière morphique (ie à chaque preuve, sans effort et de manière automatique vous associez un terme qui réalise sa conclusion)
Du coup, une "des idées" était d'étendre le mot "phrases garanties" à celles qui sont "réalisables". Ca a donné la découverte qu'avec une petite horloge on peut réaliser l'axiome du choix (non extensionnel, donc dépendant) par exemple. On ne peut pas le prouver, mais on peut "le réaliser" (autrement dit le "garantir"). Ca a donc donné un nouveau statut: il y a les
- théorèmes,
- les axiomes
Et maintenant grace à la CCH, il y a
- les bons axiomes
- les axiomes "bidons" (arbitraires), qu'on ne sait pas "réaliser" ou "garantir".
Désolé, après mon dernier message sur le fil de ola, je n'ai pas poursuivi sa lecture (c'est un défaut que je soignerais sous peu).
Merci pour ces échanges, j'ai du mal à tout suivre (sauf l'aspect explosivité, ça j'avais compris la fois dernière).
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
Mon "goût" pour $S$ (partagé par au moins 90% des gens qui s'occupent de ces sujets j'ai l'impression) vient de ce que $(S,K)$ produit la définition d'un algorithme d'abstraction (resp. la preuve du théorème de déduction) la plus courte possible. Ca ne va pas plus loin que ça.
Donnons-là pour les lecteurs: on pose $\lambda x .x:= SKK$, $\lambda x P:=KP$ lorsque $x$ ne figure pas dans $P$ et (étape d'induction) $\lambda x (FG):=S(\lambda x.F)(\lambda x.G)$. Avec ça on voit tout de suite par induction sur sa taille que pour tout terme $A$, $\lambda x.A$ ne contient plus d'occurrence de la lettre $x$, que $(\lambda x.A)x$ se réduit en $A$, puis (en notant $R[a:=T]$ le terme obtenu en remplaçant toutes les occurrences de $a$ par $T$ dans $A$; on remarque que la substitution de lettres par des termes ainsi définie commute avec la réduction, par induction immédiate sur la longueur du calcul effectué) que pour tout terme $B$, $(\lambda x.A)B$ se réduit en $A[x:=B]$, et en fait plus généralement, si $x_1,...,x_n$ sont des lettres distinctes, $(\lambda x_1. \lambda x_2... \lambda x_n.A)B_1B_2...B_n$ se réduit en $A[x_1:=B_1;x_2:=B_2;x_n:=B_n]$ (remplacement simultané des lettres $x_1,...,x_n$ par les termes $B_1,...,B_n$). $(\lambda x_1. \lambda x_2... \lambda x_n.A)$ ne contient aucune des lettres $x_1,...,x_n$; on voit donc comment définir une fonction avec une expression contenant des "variables" (les logiciens disent plutôt: des lettres "liées") en logique combinatoire.
L'algorithme ainsi défini produit des termes de grande taille et on peut l'optimiser un peu en rajoutant la clause $\lambda x.(Qx):=Q$ lorsque $Q$ ne contient aucune occurrence de la lettre $x$.
A partir de là, la preuve de la Turing-complétude de la logique combinatoire se fait comme celle du lambda-calcul (il existe des différences entre les comportements de la beta-eta réduction dans les deux systèmes mais elles ne jouent aucun rôle dans cette preuve-ci).
Blabla implique (A ou A)
et non pas
Blabla implique A
Mais comme il y a deux ou différents, j'ai détaillé côté combinateurs.
Alors pour tous $a,b,c$, $QQ(QT)abc$ se réduit en $acb$ et $QQ(QT) Q a b c$ se réduit en $a(bc)$.
Par suite, $(X \to Y \to Z) \to (Y \to X \to Z)$ est conséquence prouvable des schémas d'axiomes $A\to (A \to
Comment comprendre cette phrase, sauf à interpréter "$A\vee B$" par $(A\to
via ce qui précède, les schémas d'axiomes $A\to A$, $A\to (A \to
$((A\to
$$ blabla\multimap (A^\perp \multimap A) $$
Sinon, oui, en dehors du fait que je note
$C$ ton $Q$ et
$D$ l'autre composeur, ie $Dfg:=f\circ g$, et
$Bxy:=yx$ et $Gxyz:=xzy$
(pardon pour ces changements de lettres)
tu as [small]$puissance(C+B) = puissance(D+B)=puissance(C+G)=puissance(D+G)=$ la puissance linéaire.[/small]
En ajoutant $K$, tu obtiens la puissance affine
En ajoutant $W$ la puissance intuitionniste (ie tout le lambda calcul)
Par contre, les introductions de "RetourVersLeFutur" ne fonctionnent comme des combinateurs seuls. C'est pourquoi je t'ai suggéré d'introduire un "retourverslefutur" qui ne duplique pas de ressources.
Comme je ne sais pas où tu en es en dessous de la logique intuitionniste, je ne t'en mets pas plus pour éviter les tartines.
J'avais déjà fait des fils qui simplifiaient les différentes logiques. Je refais cid-dessous.
Tu as :
des phrases,
une phrase nommée $1$
une phrase nommée $0$,
une involution (je vais l'appeler nop) qui ressemble un peu mais pas trop à la négation nommée $x\mapsto x^\perp$ (c'est pourri mais je le garde)
une implication (je la note $\to$, mais dans la littérature elle estplutôt nommée $\multimap$ mais c'est pénible en latex.
mais surtout UN ORDRE $\leq$ que tu peux supposer complet et les axiomes suivants:
$a\to (b\to c) = b\to (a\to c)$
$a\leq b$ ssi $1\leq (a\to b)$
$\to$ décroissante à gauche et croissante à droite
$nop$ décroissante et $0=nop(1)$.
Si tu n'ajoutes rien de plus les théorèmes linéaires sont les phrases $p$ telles que tu peux prouver que $1\leq p$
Mais tu peux ajouter l'axiome $\forall x: x\leq 1$. Auquel cas tu as la logique affine. Selon tes gouts.
Il est "hérétique" d'aller plus loin, mais pour info, en ajoutant $\forall x: x^2=x$ va tout collapser à la logique classique. (Sans le nop, ce serait l'intuitionniste). Mais en fait, c'est plus "sain" de ne rien ajouter à ce que j'ai dit. Pour des riasons trop longue à expliquer.
La complétude te donne deux "et".
Le "et" numéro1 appelé (de manière pourrie :-D ) tenseur est la borne inférieure des $[a\to (b\to x)]\to x$ quand $x$ parcourt toutes les phrases. Il est noté $a\otimes b$ et est tel que $\forall a,b,c: a\to (b\to c)=(a\otimes b)\to c$
Le "et" "gentil" mais pernicieux est appelé "aec" et c'est juste a avec $b:= inf(a,b)$
Idem pour les "ou". Le "ou" dual du tenseur (je vais l'appeler le "ou lourd" (les linéaristes l'appellent "le par") est défini par $a-b:=((a^\perp)\to b)$ ce qui en passantte montre que grace à nop, on aurait pu définir de manière plus légère que je ne l'ai fait les $\otimes$.
Et tu as bien sûr le "ou" léger dual de avec qui est $sup(a,b)$.
Voilà, compte-tenu de ton niveau, tu es maintenant aussi espert que les professionnels de ces logiques dès lors que tu te sera appropiré ces définitions.
Bien évidemment, tu as $sup(a,a)\leq a$, ce qu'on peut exprime ren disant (a ou a) => a est un théorème, mais seulement avec le "ou" léger qui est "sans intérêt" dans sa relation avec l'implication.
Et ce que je te disais c'est que l'axiome de Pearce habituel renferme DEUX POUVOIRS.
L'un dit que ((A=>B) => A)=> (A $ou_{lourd}$ A)
L'autre dit que (A $ou_{lourd}$ A) =>A, qui n'est rien d'autre que le pouvoir de W.
Voilà voilà. C'est pourquoi, et sans vouloir casser la magie, devant tes remarques "émerveillées" que Pearce renferme la puissance du clonage, je t'ai posté toutes ces choses qui ne sont en fait que des duales de ce qui est connu pour le "et lourd".
Quand on a beaucoup utilisé la logique bancale (l'intuitionniste) qui a littéralement "jeté aux oubliettes culturelles" un des côtés mais pas l'autre (autrement dit en logique intuitionniste, il est bien vrai que A et nonA est contradictoire, mais il n'est pas un axiome que A ou nonA, etc, etc), c'est sûr qu'on n'est pas habitué par réflexe à voir les symétriques des choses auxquelles on est habituées.
Attention, je parle de bancalité objective. Je n'en critique pas l'aspect politique.
La dualité (terme, environnement) annonce d'ailleurs très bien la chose: (toi, le reste du monde).
L'approche symétrique te limite tellement que tu n'as plus besoin de voir le reste du monde comme un truc puissant (initialement destiné à compenser la puissance qu'on t'avait donnée en tant que terme possible) et la phénoménologie retrouve sa symétrie. Je pense que c'est ça qui a provoqué le privilège historique de la logique intuitionniste.
Mais en fait, en termes informatiques, il n'y a par contre "pas de souci", et avec un peu de pratique on voit très bien la symétrie (qu'on retrouve d'ailleurs avec les espaces vectoriels de dimension finie).
$A$ $et_{lourd}$ $B$ = $A\otimes B$
$A$ $et_{gentil}$ $B$ = $ A\oplus B$
$A^\perp$, bin, se note aussi $A^\perp$
Problème : $A$ $ou_{gentil}$ $B$ EST AUSSI EGAL A $A\oplus B$, donc, là, on voit que c'est "imparfait" comme représentation (mais pas grave)
$A\multimap B = L(A,B)$
Bon, c'est pas très dur de comprendre, vu que $inf(A,B)=A\cap B$ en alg linéaire,
et que tu as le FOR-MI-DABLE $(X\cap Y)^\perp = X^\perp + Y^\perp$
Mais pour comprendre l'aspect logique, il faut "passer au log", c'est à dire, en tout cas selon moi,
A avec B
> inf(A,B)
$A\otimes B $
> $A+B$
puisque le "et lourd" représente bien LA SOMME des ressources.
Combinateur-ment parlant:
$x\otimes y := [t\mapsto (tx)y]$
Par contre, il n'y a pas de représentation "purement combinatoriale" de inf et sup, ni de ce que j'ai appelé "nop".
$A\multimap B$ veut juste dire $\{x\mid \forall y\in A: xy\in B\}$
un ensemble étant un théorème quand il contient $e$.
Evidemment, tu peux restreindre les ensembles (comme par exemple, pour les anneaux, ne t'occuper que des idéaux, etc).
Un théorème linéaire est une phrase dont chaque fois que tu l'interprètes dans ce contexte, ça donne un ensemble contenant $e$.
Là tu sais vraiment de chez tout, absolument tout de ce qu'il faut savoir!!! :-D :-D
Je connaissais la logique linéaire version "calcul des séquents" (ça a été la première fois que j'ai pu écrire une preuve complète d'élimination des coupures pour moi-même avec la partie sans les $!,?$ car à vrai dire ce sont les droits de copie/effacement qui créent les complications) mais ne l'ai jamais vraiment utilisée (l'assimilation d'énoncés mathématiques à des ressources consommables limitées/malus non gratuitement destructibles, je trouve que c'est pousser un peu).
Une fois l'élimination des coupures obtenue il est facile de montrer qu'étant donné un énoncé écrit uniquement avec $\multimap$ comme connecteur, cet énoncé est prouvable en calcul des séquents linéaire si et seulement si il l'est dans le système de Hilbert dont les schémas d'axiomes sont $X \multimap X$, $(X \multimap Y \multimap Z) \multimap Y \multimap X \multimap Z$ et $(Y \multimap Z) \multimap (X \multimap Y) \multimap X \multimap Z$.
Sans plus connaître de détails, si on interprète chaque variable propositionnelle par un nombre entier et $\multimap$ par une soustraction, tous les théorèmes obtenus comme ça donnent $0$ ce qui permet de montrer que $(A \multimap A \multimap
astuces latex:
$ A \multimap B$ pour $A \to B$
$A \wp B$ pour $\left (A^{\perp} \otimes B^{\perp} \right)^{\perp} $ (ou $A^{\perp} \multimap B$)
C'est long mais c'est bon.
À bientôt.
Cherche livres et objets du domaine mathématique :
Intégraphes, règles log et calculateurs électromécaniques.
"A (ou lourd) B" qui se dit "A par B" à l'oral s'écrit donc en latex : $A \wp B$ (je le précise pour les lecteurs qui veulent connecter les posts).
A ma connaissance et aux articles ou commentaires que j'ai croisés ces dernières décennies, je crois surtout qu'au niveau "financement" ces labos essaient de résoudre P=NP et autre problèmes de cette famille en apportant le paradigme de ces logiques faibles. C'est une impression que j'ai eue.
Ca, c'est pour les articles publiés.
Ensuite pour le principe, c'est comme on dit souvent "pour l'honneur de l'esprit humain". Mais je pense "pas que". En effet, c'est en m'adaptant à ces logiques plus faibles que j'ai pu évoluer psychologiquement et devenir plus souple dans mes approches philosophiques par exemple des fondements quantiques.
En fait, il y a beaucoup à gagner à maitriser ces choses qui en plus ont le grand avantage d'être faciles. Leur seul inconvénient est que contrairement au rest de la science elles bénéficient de pas mal de financements et il y a "moins de sélection" des petits jeunes qui en font et du coup, les thèses se multiplient et les sigles avec. Donc quand on fait une recherche biblio, c'est une vraie jungle. Parfois on a l'impression (fausse) qu'il y a un système par chercheur du domaine.
PARDON pour garder mes lettres, pour la suite, c'est juste que je n'ai pas la dispo pour me contraindre à un exo de mémoire, j'ai pris des habitudes en réinventant tout seul et en passant des heures derrière caml
Mais je précise de toute façon, les comportements.
1/ Je note (les lettres minuscules sont supposées introduites par $\forall$) :
$abc$ abrège $(ab)c$
$Dxyz:= x(yz)$
$Cxyz:=y(xz)$
$Bxy:=yx$
$Wxy:=xyy$
$Jx:=x$
$Kxy:=x$
$Fxy:=y$
$Mxyz:=x(zy)$
$B'x:=xJ$
$Sxyz:=xz(yz)$
$Gxyz:=xzy$
$K'xy:=x$ (=K, mais vocation voir suite)
2/ Ces combinateurs réalisent (garantissent) phrases majuscules introduites par $\forall$ :
$C: (A\to
$D: (A\to
$G: (A\to (B\to C))\to (B\to (A\to C))$
$B: A\to ((A\to
$M: (B\to C)\to (A\to ((A\to
$K: A\to (B\to A)$
$F: A\to (B\to
$J: A\to A$
$W: (A\to (A\to
$B': (1\to A)\to A$
$K' : A\to (1\to A)$
$S: (A\to (B\to C))\to ((A\to
Il y a de fortes redondances que je signale maintenant, en admettant que $J$ est toujours tacitement présent :
3/ Avec $P:=puissance(C,B)$, on a :
$P=puissance(D,B)$
$P=puissance(D,G)$
$P=puissance(M,G)$
$P=puissance(C,G)$
$P=puissance(C,B)$
$P=puissance(C,B',K')$
tout n'y est pas. La puissance $P$ est celle des garanties de la logique linéaire. Par (comment dire) "grassitude" peut-être?), l'ajout de combinateurs maintient les égalités.
Ainsi en ajoutant $K$, on obtient la puissance des garanties de la logique affine.
Ainsi en ajoutant $W$, on obtient la puissance des garanties de la logique intuitionniste.
A noter qu'en plus, mais ce sont des curiosités :
$puissance(S,K)=puissance(W,C,K)$ (on peut retirer $B$ quand on a d'autres trucs)
4/ Les phrases garanties par un terme construit uniquement avec $M$ et $B$ ont AUTOMATIQUEMENT (pas de coupures à éliminer) des propriétés de sous-formules. Par contre, j'ignore si $puissance(M,B)=P$
5/ Je termine en donnant un exemple de preuve de comment on prouve que ceci garantit cela. Se reporter à mon post où j'ai donné les axiomes.
Exemple 5.1:
Supposons que $e$ agresse $(A\to
Il est donc de la forme $x+y+z+e$ avec:
$x$ garantissant $(A\to
$y$ garantissant $(C\to A)$
$z$ garantissant $C$
Le process $(D,e)$ va donc évoluer en un pas vers le process $(x, (yz) + e)$
Il suffit donc de prouver que $yz$ garantit $A$ pour obtenir que ce process marche.
En effet, $x$ garantit $A\to B$ et $e$ agresse $B$. Donc si on prouve ce qui est annoncé, $(yz+e$ agresse $A\to B$.
Soit $e'$ qui agresse $A$. Le process $(yz,e')$ évolue vers $(y,z+e')$.
L'environnement $z+e'$ agresse $C\to A$ car $z$ garantit $C$. Donc $(y,z+e')$ marche, CQFD.
[small]Exemple 5.2:
On prouve que $t:=WJ(WJ)$ garantit $0=1$.
Je note $a:=\{x\mid (x\in x)\to (0=1)\}$, de sorte que la phrase $H:=(a\in a)$ vérifie:
$$ H=(H\to (0=1))$$
Soit $e$ un environnement qui agresse $0=1$. Nous voulons prouver que $(t,e)$ marche. Or il évolue en un pas vers
$(WJ, (WJ) + e)$. Il nous suffit donc de prouver que $WJ$ garantit $H$ (il garantit alors aussi $H\to (0=1)$)
Soit $x+e'$ un agresseur de $H\to (0=1)$. On veut prouver que $(WJ, x+e')$ marche, il suffit donc de prouver que
$(W, J+x+e')$ marche. Ce process évalue vers $(J, x+x+e')$ qui évolue vers $(x, x+e')$.
Il suffit donc de prouver que $x$ garantit $H\to (0=1)$, ce qui est vrai par hypothèse puisque:
$x$ garantit $H$ et
$H=(H\to (0=1))$
[/small]
6/
Exos:
construire $D$ à partir de $C,G$
construire $C$ à partir de $D,G$
construire $D$ à partir de $M,G$
construire $G$ à partir de $D,B$
construire $G$ à partir de $C,B$
construire $B$ à partir de $C,B',K'$
construire $S$ à partir de $W,C,B$
On peut en ajouter une vingtaine, j'arrête là
7/ A noter que le plus "marquant" je trouve, puisque ça met une sorte de doigt d'honneur gentil à l'approche catégoricienne est l'universalité de $(C,B',K')$ qui singifie QU'SEUL axiome suffit à produitre TOUTE la logique linéaire via le seul modus ponens, à la condition d'avoir "en dur" que : $(1\to x)=x$.
Pour ne pas imposer ce "en dur", j'ai ajouté les combinateurs $B',K'$.
Pour les gens qui aiment bien caml ce sont les passages de :
toto()
à
toto
et inversement
qui apparaissent de l'enculage de mouches à 99% de la population mondiale informatique et qui pourtant .... est en fait de première importance.
$A \multimap A$
$(A\multimap C \multimap D) \multimap (B \multimap C) \multimap B \multimap A \multimap D$).
Idem dès lors que ça contient $R$ (c'est le nom que j'ai donné à ton combinateur) et $J$.
Autrement dit, pas besoin de modus ponens, mais juste de la règle de déduction suivante:
C'est une des 168571415687 :-D versions de ce que j'appelle souvent sur le forum le slogan:
[small]Preuve brouillone pour C,D.
ux(vy) == [D(ux)v ]y == ... == [mv] y == [triomphe] y (récurrence, $v$ étant plus court que $vx$)
ayant noté avant que :
a(ux) == [C(u)]ax == [pretiomphe]ax
Preuve brouillone pour R,J:
ux(vy) == [R(u)(v)]yx == ...[m (v)] yx == [triomphe] yx
ayant noté avant que :
a(uxy) == [RJ(ux)]ya == RR(u)xJya == .. triomphe
Pour R,J, il est aussi nécessaire de justifier qu'il est universel (je laisse en exo)[/small]
$R_1$ défini par $\forall x,y,z,t: R_1xyzt := (xt)(yz)$
mais aussi
$R_2$ défini par $\forall x,y,z,t: R_1xyzt := (xz)(yt)$
sont tous deux universellement linéaires (au sens qu'on peut obtenir tous les combinateurs linéaires).
Mais pour l'un des deux, je ne sais plus lequel, je ne suis pas parvenu à le rendre "super-universel" au sens de la deuxième partie de mon post. Bon, après ce sont des choses un peu anecdotiques tellement il y en a, que la recherche moyenne consacrée à chacune est peu de chose pour ce qui me concerne.
Après avoir lu minutieusement l'énoncé de notre cher Stephen Wolfram (qui m'a permis avec son Moteur Alpha de décoincer pas mal de problèmes de TD),
j'ai également tout de suite pensé aux fonctions récursives, et plus largement, à la programmation fonctionnelle.
En termes d'implantations, C++ serait plus rapide mais LISP/Scheme/Racket produirait une version plus exacte, analytiquement parlant, et plus élégante.
NB. À loisir, je proposerai(s) une implémentation du problème des combinateurs S-K, qui ne requiert même pas une représentation de groupes, mais, si je m'en fie à ma bonne étoile, aux monoïdes.
Complètement d'accord avec toi.
En Théorie des Modèles, deux Modèles sont équivalents modulo une catégorie près.
Et donc, le Lamba-Calcul convient parfaitement pour toute implémentation.
Mais c'est insuffisant...
Les combinateurs S et K peuvent être poussés jusqu'à être des représentations de géométrie des groupes d'action/d'algèbres d'opérateurs.
Alors, on peut représenter les combinateurs S et K, en plus de la propriété de compositions, d'engendrer des diagrammes de Cayley à 1,2,ou 4 générateurs.