Lambda-calcul et point fixe

jingenbl

Bonjour à tous et bonne année 2021!

Je suis novice dans le lambda-calcul et je rame un peu (beaucoup...)
Il existe un théorème du point fixe du genre
" il existe un combinateur Y tel que Yx =(beta) x (Yx)"

Bon admettons...
Il en découle le résultat suivant
"pour tout Z et pour tout n, l'équation en x : xy_1y_2...y_n = Z est résoluble en x c-à-d il existe X tel que Xy_1y_2...y_n = [X/x]Z"

([X/x]Z veut dire X à la place de x dans Z, les autres conventions du lambda calcul étant respectées)

Il "suffit" de prendre X = Y(^xy_1y_2...y_n.Z) ou Y est le combinateur du point fixe Y = UU et U =^ux.x(uux)

Ah bon ? Les termes que j'écris tournent en boucle... Il y a quelque-chose qui m'échappe...
Merci par avance de vos lumières !

christophe c

Il est tout à fait normal que le calcul boucle, tu n'espères quand-même pas que tu vas associer des points fixes concrets à toutes les fonctions du monde. Si ça ne bouclait pas c'est ce qu'il se passerait et tu aurais un vrai entier $n$ tel que $n+1=n$. Tout le monde en rêve.

Si j'ai bien compris tes notations, tu demande $f$ telle que $fabc = Z(f)$. Bin tu prends un point fixe $p$ de $Z$ tel que $p=Z(p)$ et la fonction $f$ telle que $\forall x,y,z: fxyz = p$

Mais peut-être avais-tu mis les a,b,c,.. dans l'écriture de Z?

De toute façon, c'est toujours la même chose: tu prends $gxabc = Z(xx)abc$ et $f:=(gg)$

jingenbl

Merci pour cette réponse ultra-rapide!

Je suppose en effet que abc apparaissent dans Z. Je suppose que Z(f) veut dire cela...

Je ne comprends pas bien... admettons que j'ai p tel que p=Zp (Z appliqué à p) et que j'ai f tel que fabc=p pourquoi ai-je fabc = Z où j'ai remplace x par f dans Z ?

Autre réflexion: si c'est normal que ça boucle, alors qu'apporte le théorème de plus que si p=Fp, je remplace p par ça valeur p=FFp, je remplace p par sa valeur etc...

Merci par avance de cette aide rapide et précieuse

Remarque: comment inclure Latex dans ce mémo? Merci encore

christophe c

Non, mais déjà il vaut mieux pour qu'on se compenne, écrire avec soin. Dans tous les cas tu as des points fixes habituels, mais je ne te suis pas trop avec tes notations.

Si tu cherches $\forall a,b,c: xabc=Zxabc$, je t'ai répondu, tu prends :

$\forall a,b,c,x: gabcx :=Z(xx)abc $ et $fabc=gabc(gabc)$

de sorte que tu auras $\forall a,b,c: fabc=Z(fabc)abc$

Sur ta dernière question, si si c'est vachement utile. Quand tu as une fonction qui termine TOUJOURS par exemple, et bien l'appel terminera aussi et tu auras un vrai point fixe.

En gros tout dépend de ce que tu cherches, on ne peut pas avoir le beurre et ...

Si tu programme $\forall x: fx = g(xx)$ et exécute $ff$, tu as le point fixe $ff=g(ff)$, MAIS SURTOUT comme $g$ prend "tout en charge", tu as un VRAI résultat plaisant, c'est à dire un point fixe de $g$ in the bank

Par exemple, avec Matiasevic, tu peux te taper des délires sur les formes que tu veux voir prendre à ton polynôme universel avec ça.

Ca permet aussi de prouver le théorème de Godel, via:

$$\forall x: f(x) := Prouvable (Non(xx))$$

qui va te donner $ff:= Prouvable (Non(ff))$ qui va TERMINER (enfin être sain, ie sa non terminaison établira la non prouvabilité, et donc en plus vérité de $non(ff)$

Le LC est peut-être plus appréhendable mais plus "bizarre" avec la logique combinatoire ou tu n'as pas de variables liées. Ce sont juste des mots. Donc là, tu te rends mieux compte de ce qu'il se passe, car (je tape au hasard "EXSOPQ", flemme, c'est pour te faire comprendre le principe) tu auras ton point fixe EXSOPQ = Prouvable ( non (EXSOPQ) ) où tu t'aperçois que Prouvable est légitime car s'applique à la suite de signes et non son sens. C'est un peu comme si Prouvable prend un numéro en paramètre et calcule tranquillement, il n'y a pas d'autoréférence contrairement à ce que croient souvent les gens.

jingenbl

Merci pour cette réponse.
En effet, je ne retrouve pas dans le message la syntaxe habituelle...

Si j'ai bien compris l'énoncé (copie jointe) on donne $x,a,b,c$ des variables et $Z$ un terme du $\lambda$-calcul (donc variable ou abstraction ou application avec ou sans $a,b,c$ comme variables libres). On cherche un terme $X$ tel que $Xabc \underset{\beta}{=} [X/x]Z$

Donc écrire $\forall a,b,c,x: gabcx := Z(xx)abc$ m'est obscure (je suppose que := veut dire égale par définition) et je suis déjà perdu.... Cette expression est-elle sensée définir $g$ du genre $g\equiv \lambda abcx.Z(xx)abc$ et $f\equiv \lambda abc.gabc(gabc)$ ?

$fabc = (\lambda uvw.guvw(guvw))(abc) = gabc(gabc) = Z((gabc)(gabc))abc=Z(fabc)abc$... en effet. Mais ce n'est pas le problème posé....

Le reste du mémo m'est opaque... Manque de connaissances et de pratiques dans le domaine sans doute....

Si je dis que le théorème du point fixe permet de définir récursivement la SYNTAXE de nouveau $\lambda$-termes (ce qui n'est pas possible dans la définition de base qui ne permet pas d'avoir le nouveau terme à gauche et à droite de l' "égalité"), est ce que je dis une grosse sottise ?

Merci encore

christophe c

Quand j'écris $\forall x: f(x):=Truc$, ça veut juste dire que je prends $f:=\lambda xTruc$ ou des fois on note aussi $x\mapsto Truc$, rien de plus.

Le combinateur de point fixe qui semble noté Y dans tes docs c'est probablement juste $Y:=(f\mapsto pf(pf))$ avec

$$\forall x: pfx := f(xx)$$

que tu peux aussi écrire $f\mapsto [x\mapsto f(xx)]$, et dans ton cours, c'est noté $\lambda f\lambda x(f(xx))$

et dans le cas de ton exo, tu appliquais ça à la fonction $x\mapsto Zxabc$.

Ta dernière question: non, ce n'est pas une sottise, mais c'est peu significatif. Ce n'est jamais trop utile de traduire en français vague des choses mathématiques précises. Après je ne sais pas quel est ton but. Si c'est pour une pancarte publicitaire pour un cours privé de lambda-calcul ou autre :-D

jingenbl

Merci pour la réponse... Mais je ne parviens pas à raccrocher les wagons...

Je traduis ton $Y \equiv \lambda f.pf(pf)$ (mais p??? est-ce une variable? un $\lambda$-terme quelconque?) ($\equiv$ pour synonime)
Je traduis $pf \equiv \lambda x.f(xx)$ et donc $Y \equiv \lambda f.((\lambda x.f(xx))(\lambda x.f(xx)))$ qui ne ressemble pas à $\lambda fx.f(xx)$


Donc "appliquer ça à $Zxabc$" j'en suis loin.... Avant qu'un ULM prenne son envol, il roule au raz des pâquerettes... Merci par avance pour ta patience

Pour info dans ma doc: $Y\equiv UU$ et $U \equiv \lambda ux.x(uux)$

christophe c

Ecoute, il n'y a aucun mystère dans le LC si ce n'est que la tradition notationnelle s'est construite sur une sorte de volonté de montrer qu'on est conscient de faire du formel, d'où des notations comme $t[x/y]$ voulant dire $x$ remplace $y$ dans $t$ ou comme $\lambda x:expression$ à la place de $x\mapsto expression$.

Donc je te recommande de ne pas faire table rase du passé et de jouir de ce que tu as déjà aimé faire quand tu faisais des maths traditionnelles où tu te frustrais de préciser des usines à gaz comme des ensembles de départ, d'arrivée, etc, car avec le lambda calcul, tout ça c'est fini, tu es revenu (mais sans perte) aux fondements les plus en amont de l'activité de pensée.

Donc tu peux te permettre d'écrire

"je veux" $f$ telle que $\forall x: f(x)=x(x)+1$ et je vous emmerde tous, car regardez comme je suis riche: ma fortune est $f(f)$ euros, c'est à dire $f(f)+1$ euros".

Autrement dit, certes, ton cours va te raconter avec froideur la même chose que:

Msieurs-dames, look at my dream:
je pose $forall f,x: \phi (f)(x) = f(x(x))$ et $\forall f: \sigma(f):=\phi(f)(\phi(f))$ et j'obtiens :

$\forall f: \phi(f) = f(phi(f))$, c'est à dire non seulement un point fixe de $f$, mais en plus "uniformément".


Ca ne change rien, te permet d'ailleurs de faire plus attention aux parenthèses en traduisant, mais surtout te retire le côté "tue-l'amour".

Dans ton premier post, tu as juste appliqué ça à la $f$ telle que $\forall f(x):=Z(x)(a)(b)(c)$.

Le mot ronflant "réduction d'un redex $(\lambda x :expression)(machin)$ en Bidule, c'est juste le fait que tu as fait ce que tu as toujours fait pendant tes études à savoir qu'on te décrit $f:=[x\mapsto expression]$, ce qui te dit ce que fait $f$ et éliminer le redex c'est juste écrire directement $f(machin)$ comme tu as toujours fait.

La beta réduction c'est juste passer d'un terme à un autre en éliminant ou créant des redex et tu rajoutes eta quand tu te donnes le droit de rajouter des lettres à droite en argument pour vérifier une égalité, ie tu peux ne pas arriver à égaliser $f=g$, mais ça arrive que tu peux égaliser $f(x)=g(x)$, et la eta te donne le droit de dire que $f=g$.

Bref, ne te laisse pas entrainer vers l'idée que tu n'as jamais fait ça. 100% des matheux font ça toute la journée, rien que ça, et n'en ont pas conscience, le LC est juste le fait de l'avouer franchement.

jingenbl

Encore merci pour le conseil: pas de table rase.... (à propos, le but du typage est-il la gestion saine du domaine et du codomaine ?)

Pour le reste, je reste désespérément au raz des pâquerettes...

On pose $\forall f,x: \phi(f)(x) = f(x(x)) \quad \forall f: \sigma = \phi(f)(\phi(f))$
On en déduit que $\phi(f) = f(\phi(f))$ ben,non... j'ai beau remplacé truc par machin dans bazar , je n'y arrive pas... Ne faudrait-il pas quelque-part $\sigma$? d'ailleurs...

Y-a-t-il un sens caché dans $\sigma$ qu'il faut comprendre à sa simple définition?...

Je vais encore essayer et merci pour les conseils

christophe c

Pardon, c'est une faute de frappe, évidemment, j'ai écrit $\phi$ au lieu de $\sigma$ je pense.

$\sigma(f) = \phi(f)(\phi(f)) = f( \phi(f)(\phi(f))) = f(\sigma (f))$

à propos, le but du typage est-il la gestion saine du domaine et du codomaine ?

En fait, le typage est relié aux preuves le tout à travers la correspondance de Curry Howard qui dans ce contexte très particulier va dire des choses comme un terme provenant d'une preuve va terminer en tant que programme si on l'exécute et pour prouver ça, on se sert du typage. Donc, en un certain sens, oui, ça gère, mais dire "sainement" est exagéré, car les bons programmes ne terminent pas et ont le devoir de ne pas terminer (si Windows termine, tu risques d'être énervé :-D ) et les seuls programmes dont on attend qu'ils terminent sont assez réduits, en gros ce sont ceux qui doivent donner le résultat d'un calcul, donc on est embêtés si on doit l'attendre éternellement.

Cela dit, ne pas boucler et "s'arrêter vite" sont des choses tellement différentes en pratique que tout ceci est peu pertinent.

Ce qui surtout est important ce sont les histoires de principe. Les preuves propositionnelles te construisent des objets dans n'importe quelle catégorie cartésienne fermée, leur exécution étant "évidemment" garanti terminer.

Mais les systèmes de typages sont très variés. En dehors de ceux destinés à ne donner que du terminant, qui eux sont triviaux et en gros proviennent des théories faibles, de l'algèbre, etc, la spécialité concernée essaie surtout de faire des associations de plus en plus "sémantiques" avec in fine, le but de tout typer, quitte à ajouter des types auto-référents comme $A=(A\to $ qui vont te typer par exemple ici le point fixe (construit comme ci-dessus) du "non". Mais là encore, tout ceci ce sont des grands mots savants pour que la spécialité vive, mais derrière, "pas de table rase" comme tu disais, ce sont des choses très familières et "évidentes". Je t'écris le typage bouclant ci-dessus, tu vas voir qu'on sait EXACTEMENT où mettre les hypothèses dès qu'on a le terme. Et ce "on sait" c'est essentiellement ça la vraie CorCuHo.

Supposons que $B^A=A$. Je vais te fabriquer un élément de $B$. La fonction $d:x\mapsto x(x)$ va de $A$ dans $B$ et est donc un élément de $A$, donc aussi de $A\to B$ de sorte que $d(d)\in B$.

Bon bin, je n'ai fait que regarder le terme $dd$ où $\forall x: d(x):=x(x)$.

Je vais maintenant te prouver que toute application de $B\to B$ a un point fixe. Soit donc $g: B\to B$. La fonction $f: x\mapsto g(x(x))$ va de $A$ dans $B$, ce qui fait de $f$ aussi un élément de $A$, donc $f(f)\in B$ et $f(f)=g(f(f))$ est un point fixe de $g$.

Il y a une "compulsion" qui fait que les gens s'interdisent de raisonner avec cette simplicité à cause ... du traumatisme de la crise des fondements d'il y a 120ans, du coup, tu n'es pas gâté car tu vas devoir te taper des précautions notationnelles inutiles lors de ta formation, juste à cause de cette angoisse injustifiée.

jingenbl

Grand merci. Avec $\sigma$ ça va mieux...

Je vais relire tout cela à tête reposée et avec l'avancement de mes lectures....

Bonne année 2012

christophe c

N'oublie pas d'aller voir assez vite la logique dite combinatoire, qui n'a rien de logique mais qui est juste du LCalcul remis en "bon ordre" avec des combinateurs et pas de lettres liées, ni de lambda