Bon les exemples, ils se comprennent mieux sur les dessins de Tarik, surtout si on sait que parfois il n'en a dessiné qu'un sur deux.
Comprendre les constantes
On comprend mieux les constantes si on pense à \oplus et \otimes comme à des opérations n-aires.
La constante 0 est le \oplus d'une famille vide: le joueur qui doit choisir n'a pas de choix, et donc ne peut pas jouer (sur cette formule).
La constante 1 est le \otimes d'une famille vide : le joueur qui veut s'en débarrasser doit se scinder en une famille vide de joueurs et doit répartir ses autres
formules entre les membres de cette famille vide. Il faut donc qu'il n'ait aucune formule à répartir.
La finitude de MALL
Ce jeu MALL est fortement fini (on dit peut-être noethérien), en ce sens que non seulement toutes les parties sont finies mais su'en plus, pour toute position p, l'ensemble des longueurs des parties commençant en p est fini (et donc majoré).
De MALL à LL
Quoi d'autre dans LL à part MLL? Il y a les quantificateurs, bien sûr, et aussi les exponentielles ! et ? .
En gros !A, c'est A \otimes A \otimes A ... une infinité de fois, tandis que ?A c'est A \par A \par A ... une infinité de fois. Et bien sûr cette infinité va être source d'ennuis. La dernière chose qu'il faut absolument savoir sur LL c'est que la logique classique, LK, se traduit en LL, on verra comment. Le point le plus spectaculaire de cette traduction concerne l'implication: la traduction de A =>B est !A* -o B* , où A* et B* sont les traductions de A et B. On dit à ce sujet que Girard a décomposé l'implication classique en termes de connecteurs ( -o et !) plus élémentaires.