Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d’application. L’idée de base du lambda-calcul est que tout est fonction. Une fonction est en particulier exprimée par une expression qui peut contenir des fonctions qui ne sont pas encore définies et qui sont alors remplacées par des variables. Le jeu des crocos propose de substituer les règles formelles du λ-calcul par des règles plus naïves mais tout aussi « efficaces ». Ainsi, en compagnie de « familles crocos », les parenthèses, les définitions lambda, les applications, les alpha-conversions et les beta-reductions deviennent des vieux crocos, des croco affamés, de pauvres familles dévorées (mais qui vont se réincarner, ouf !), des changements de couleurs et des éclosions d’œufs....respectivement bien sur !
Un grand merci à Bret Victor pour avoir inventé ce jeu qui ne demandait qu’à être codé ! Les règles originales
Une idée importante pour le λ-calcul est celle qui consiste à ramener les fonctions de plusieurs variables à des fonctionnelles d’une seule variable. Par exemple, le pgcd est une fonction de deux variables entières a et b, et on peut considérer a non pas comme une variable, mais comme un paramètre, et étudier la fonction pa qui, à b, associe pa(b)=pgcd(a,b) : Cette famille de fonctions porte en elle toute l’information nécessaire à l’étude du pgcd. Voici par exemple la représentation graphique de p60 :
suite = (pgcd(60,x) for x in [0..60])
dessineSuite suite, 60, 0, 40, 2, "blue"
On peut donc remplacer 60 par un autre nombre pour voir l’allure d’autres fonctions de ce genre.
L’idée de remplacer une fonction de plusieurs variables, par plusieurs fonctionnelles d’une variable, est suffisamment importante pour porter un nom : C’est la curryfication. Mais elle remonte au moins à Gottlob Frege vers la fin du XIXe siècle, elle est donc nettement antérieure au λ-calcul.
Le nom de curryfication est évidemment un hommage au logicien Haskell Curry (dont le prénom est celui d’un langage de programmation basé sur le λ-calcul). Dans les années 1920, Curry s’intéressait à la logique combinatoire qui étudiait le comportement syntaxique des quantificateurs.
Un problème de cardinalité se posait à propos des fonctions, qui sont beaucoup plus nombreuses (il y en a 22ℵ0) que les noms disponibles pour les nommer (en général f et g...). Alors vers la fin des années 1920, Alonzo Church a inventé une fonction qui a pour but de rendre anonyme une fonction, ainsi que sa variable. Cette anonymisation est notée λ. Par exemple la fonction « carré » devient λx.x² et perd son nom (« I am not a lambda, I am an human being », dirait le prisonnier). Or Church a constaté que λ se comporte en bien des égards comme un quantificateur : C’est ainsi que le λ-calcul est né.
Comme l’idée de Russel qui était de tout représenter par des ensembles, était vouée à l’échec à cause du paradoxe de Russel, Church a proposé durant les années 1930 de fonder les mathématiques sur la notion de fonction et le λ-calcul. Mais en 1933, Rosser et Kleene, thésards de Church, ont découvert dans le λ-calcul typé un paradoxe autoréférentiel. Church a alors abandonné le λ-calcul typé et c’est en 1936 qu’il a publié le λ-calcul tel que présenté ici.
Dans les années 1940, Curry a découvert le paradoxe de Curry dans le λ-calcul non typé. Des recherches assez actives sont donc en cours sur les λ-calculs typés. Voir par exemple les travaux de Thierry Coquand et Gilles Dowek.
Une famille « petite » :
Un croco qui garde un œuf [1] !
Une famille « moyenne » :
Un croco vert et un croco rouge qui garde un œuf vert et un œuf rouge. Pour être plus précis, nous dirons qu’un croco vert garde un croco rouge qui lui-même garde un œuf vert et un œuf rouge [2] !
Une famille « grande » :
Un croco jaune qui garde un croco vert qui garde un croco rouge qui garde un œuf vert, un vieux croco qui lui-même garde un œuf jaune et un œuf vert, et un œuf rouge [3] !
Une petite famille croco composée d’un croco jaune qui garde un œuf jaune se trouve juste devant une famille croco composée d’un croco vert qui garde un croco rouge qui garde un œuf vert et un œuf rouge...
Un croco affamé est...affamé !
Il dévore toujours ce qu’il y a devant lui !
Ensuite, il meurt !
L’ œuf de la même couleur va éclore
Et donner naissance à ce qui à été mangé (exactement) !
Une famille composée d’un croco jaune qui garde un œuf jaune, se trouve devant une famille composée d’un croco vert qui garde un croco rouge qui garde un œuf vert et un œuf rouge, qui se trouve elle-même devant une famille composée d’un croco violet qui garde un croco orange qui garde deux œufs violets et un œuf orange...ouf !
Le croco affamé « le plus en haut à gauche » dévore ce qu’il y a devant lui
Ensuite, il meurt et les œufs de la même couleur vont éclore
Et on recommence...Le croco affamé orange « le plus en haut à gauche » dévore ce qu’il y a devant lui (la famille jaune), ensuite, il meurt et l’œuf de la même couleur va éclore
Vous pouvez le trouver ici ! Ce jeu a été testé avec Chrome et Firefox. La vitesse d’exécution de Chrome restant incomparable avec tout autre navigateur, on ne saurait vous conseiller d’en utiliser un autre...pour ce jeu bien entendu !
La version en ligne du jeu des crocos se compose d’un « plateau de jeu » et d’un « panel glissant ». A l’aide du panel, on peut fabriquer des configurations de familles de crocos et observer, étape par étape, l’évolution de cette configuration jusqu’à ce qu’il n’y ait plus rien a manger !
Permet de jouer l’animation en boucle jusqu’à la fin
Permet d’interrompre l’animation en boucle
Remet à zéro la console et efface tous les graphiques
Affiche/Cache la console
Affiche/Cache les paramètres supplémentaires
Affiche/Cache le nom des variables
Affiche/cache le nom des étapes
Bascule entre le graphe et les crocos
Affiche une aide interactive pour faire du λ-calcul en CoffeeScript
Bouton de selection des exercices du tutoriel :
Glissière permettant de régler le temps d’animation de chaque étape du jeu :
Glissière permettant de d’agrandir ou de réduire la taille des crocos et des œufs :(zoom)
Boutons de construction graphique d’un jeu de crocos :
Ce bouton est le plus important, parce qu’il permet d’inventer son propre jeu. De ce point de vue, le jeu des alligators est plutôt un méta-jeu, ce qui a de l’importance puisque
le jeu est à zéro joueur, il n’y a pas de but à atteindre ni d’adversaire à battre ;
on évolue dans un micromonde qu’il est intéressant d’explorer.
Pour transformer ce jeu sans joueur en jeu à un joueur, on peut choisir une configuration d’arrivée et demander comment y parvenir. Mais là ce n’est plus un jeu, c’est un exercice d’algorithmique. Ah bon ? Parce qu’il y a une différence ?
Au cas où l’enfant a trouvé un jeu intéressant, il peut être tenté d’en communiquer la configuration initiale. Pour cela, il y a la console dont le contenu peut être copié-collé...
Le tutoriel se compose de 8 exercices qui permettent de prendre en main l’interface du jeu et en particulier la construction graphique d’une famille de crocos par glisser déposer :
C’est donc idéalement par là qu’il faut commencer ...
La console permet de taper des lambda-expressions et les convertir en « configurations crocos » en appuyant sur la touche en haut à gauche du clavier (de la console). L’opération inverse (obtenir une lambda expression depuis une configuration de crocos) est possible avec la touche adjacente.
Cette console est importante, elle permet en définitive, de comprendre que le lambda-calcul permet de réaliser des opérations qui peuvent s’apparenter à des calculs arithmétiques qui sont à la base de tout autre calcul. C’est ainsi que les lambda-expressions prouvent leurs capacités de calcul.
Voici quelques expressions toutes faites telles que données dans la console :
bouton
λ-expression
zero
(λf.λx.x)
one
(λf.λx.(f x))
two
(λf.λx.(f(f x)))
three
(λf.λx.(f(f(f x))))
four
(λf.λx.(f(f(f(f x)))))
five
(λf.λx.(f(f(f(f(f x))))))
succ
(λn.λf.λx.f (n f x))
plus
(λm.λn.λf.λx.m f (n f x))
mult
(λm.λn.λf.m (n f))
pow
(λb.λe.e b)
pred
(λa.λf.λx.a (λg.λh.h (g f)) (λu.x) (λu.u))
sub
(λm.λa. (a (λn.λf.λx. n (λg.λh.h (g f)) (λu.x) (λu.u))) m)
Le graphe n’a pas grande utilité, si ce n’est celle de représenter les lambda-expressions autrement encore, afin d’en saisir, ça ou là, leur moëlle substantifique !
Ce tracé évolutif est fait par l’excellent logiciel libre arbor.js
Le jeu des crocos et son set de règles : comme une notion d’infini !?
[1] l’expression représentée est λe.e ; le λe est l’alligator et e est l’œuf ; la lettre « e » désigne une couleur et le fait que l’alligator et l’œuf sont de la même couleur se voit dans l’identité du nom de la variable entre le λe et le e
Dans un site très personnel, Olivier Sicard nous offres quelques « délires » de mathématiques, algorithmique et programmation. Entre autres pépites, on découvrira le Rubix-Tore, la loi normale asymétrique, la théorie du choix social et le dessin à l’aide des séries de Fourier.
Après Elwyn Berlekamp l’année dernière, c’est au tour du centenaire Richard Guy et de l’immense John Conway. Ce document de Richard Guy (une mise en garde contre le raisonnement inductif) montre bien le style unique de son auteur, en plus d’être une mine de ressources pour des exercices. Conway, outre son jeu de la vie, a créé des dizaines de jeux, dont Sprouts, très populaire dès le CP.
On sait bien que Nicolas Bourbaki n’était pas le nom d’une personne mais le pseudonyme d’un groupe. L’équivalent en informatique théorique est Claude Livercy, auteur de la théorie des programmes. Roger Mohr était un des membres de Claude Livercy.
Quand les chercheurs mettent au point des modèles d’optimisation et de recherche de plus court chemin qui s’inspirent du comportement de masse de colonies de fourmis...
À écouter : Sur les Épaules de Darwin, émission diffusée sur France Inter samedi 31 août 2013.
Les RMLLd se dérouleront pour la 2e fois à Saint-Joseph du 22 au 25 août.
C’est une opportunité pour les élèves qui suivent la spécialité ISN et les passionnés d’informatique.
Commentaires