Le jeu des alligators

mardi 26 mai 2015
par  Alain BUSSER , Florian TOBÉ

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

Remarques épistémologiques

  • 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 :

0102030405060010203040

Elle a été obtenue avec ce script sous alcoffeethmique :

  1. suite = (pgcd(60,x) for x in [0..60])
  2. dessineSuite suite, 60, 0, 40, 2, "blue"

Télécharger

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 220) 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.

Le materiel pour jouer « en vrai » !

A imprimer sur des feuilles de couleurs :

A imprimer sur des feuilles blanches :

Règles du jœufsjeu

Les pièces

  • Les crocos affamés mangent tout ce qui est devant eux, même si ce sont des familles entières :
  • Les vieux crocos n’ont plus faim, ils ne mangent rien, et ne servent qu’à garder leur famille. Mais ils meurent quand on n’a plus besoin d’eux
  • Les œufs sont de futures familles, sauf s’ils sont mangés avant d’éclore !

Les familles

  • 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] !

« Manger & Éclore »

Un exemple simple !

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) !

Et ça continue car on recommence...

  • Un croco affamé 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 a été mangé !

Un exemple plus complexe : « priorité en haut à gauche » !

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

...Avant de continuer, il faut apprendre la règle de la couleur (dans l’onglet suivant)

« Changer de couleur »

  • Un croco affamé ne peut rien manger qui soit de sa couleur ou de celle d’un membre de sa famille
  • Il faut changer les couleurs communes dans une des deux familles
  • Puis « manger »
  • « Manger encore... »
  • « Manger toujours... »
  • Et « manger » jusqu’à ce qu’il n’y ait plus rien à manger !

« Le vieux croco »

Il ne reste plus qu’une petite règle : celle du vieux croco !

  • Le vieux croco ne mange rien, il est trop vieux !
  • Il faut régler les affaires de famille d’abord !
  • Lorsque le vieux croco ne garde plus qu’un seul croco, il meurt !
  • Puis la loi de la jungle reprend ses droits...
  • Jusqu’à ce qu’il n’y ait plus rien à « manger » !

Le jeu « on-line »


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 !

Le panel glissant

Menu du jeu
Signification des icones
îconeusage
Permet de jouer un tour d’animation
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

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

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)
true (λa.λb.a)
false (λa.λb.b)
and (λp.λq.p q p)
or (λp.λq.p p q)
not (λp.λa.λb.p b a)
if (λp.λa.λb.p a b)
Y (λf.(λx.(f(x x)) λx.(f(x x))))

Le Graphe


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 !?

[1l’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

[2L’expression représentée est λe.λi.e i

[3expression λh.λe.λi.e (h e) i


Commentaires