Bonjour,
 
J'ai actuellement un projet reliant sml et lambda calcul, et je suis bloqué.
Même si vous ne connaissez pas le sml je suis sur que vous pourrez m'aider ! ^^
 
On me demande de montrer que :
Yt = (λx.λy.y (x x y)) (λx.λy.y (x x y))
 
Est un point fixe, c'est à dire que Yt g = g Yt g.
 
Déjà question tout bête : Dans cette écriture de Yt, est-ce que y(x x y) signifie y(x*x*y) ou y(x(x(y))) ou ...
 
Pour la démonstration je pense avoir trouvé en tâtonnant pas mal.
 
Ensuite je dois coder une fonction factorielle adaptée au lambda calcul et utilisant le point fixe.
J'ai souvent vu sur internet des exemples utilisant un point fixe mais je n'ai toujours pas compris à quoi cela servait.
 
Ma fonction doit avoir cette allure :
 
Y est le point fixe
F est la fonction factorielle "classique" : Si n=0 alors 1 sinon n*f(n-1)
 
Et ensuite pour appeler la fonction on me demande d'utiliser le point fixe :
 
val fact = A(Y, F), où A est une application (en gros le point fixe Y prend en paramètre la factorielle F).
 
Voilà j'espère que vous pourrez m'aider à éclaircir ces points:
-Quel est le rôle d'un point fixe
-Quel est son utilité dans la factoriel
-Que signifie exactement l'expression : Yt = (λx.λy.y (x x y)) (λx.λy.y (x x y))
 
Merci de votre aide.

J'ai édité mon message pour le rendre plus simple et l'adapter à l'évolution de mes réflexions. :-)

C'est de la prog, ça

C'est à cheval entre la prog et les maths...mais c'est bien en cours de prog que je fais ça.

Si je me souviens bien, il faut écrire la fonction de sorte que l'application successive sur le résultat ne varie pas plus qu'un epsilon donné. Le résultat Y est alors le point fixe de la fonction.

Y est le combinateur de curry:
 
Y g  = (λf . (λx . f (x x)) (λx . f (x x))) g  (par definition de Y)
 = (λx . g (x x)) (λx . g (x x))  (beta-reduction de λf)
 = (λy . g (y y)) (λx . g (x x))  (alpha-conversion)
 = g ((λx . g (x x)) (λx . g (x x)))  (beta-reduction de λy)
 = g (Y g)
 
Pour la factorielle, wikipedia doit avoir des bribes