Le lambda‑calcul, purement et en général

Ce sujet parlera du λ‑calcul en général, et c’est pourquoi il ne réutilise pas le sujet des références sur SML.

L’écriture et les règles de réécritures sont autant importantes dans le λ‑calcul qu’elles le sont dans la logique en général, et il existe justement une très étroite relation entre logique et λ‑calcul. La première chose présentée, sera alors la syntaxe.

λ Calculus (allisons.org)

Il donne cette syntaxe pour le pure lambda calcul, celui des mathématicien(ne)s :



On peut définir une chose dont les éléments font référence à d’autres choses préalablement définies (la syntaxe pour associer un symbole à une expression, n’est pas donnée), mais on a pas de point d’entrée, puisque pour définir un nouveau symbole, il faut bien qu’il y ait des symboles préexistants.

Il complète en ajoutant une production pour les constantes, dont on pourra supposer qu’il en est des prédéfinies.



Il ajoute deux commentaires, qui introduisent aussitôt deux notions : l’application et l’abstraction. Les opérations sur les expressions du λ‑calcul, seront présentées plus tard.

Deux très bons liens et un troisième lien plus inattendu, moins généraliste que les deux premiers, mais important, car concernant les opérations que j’ai promis d’aborder plus tard. Le premier lien est vers un PDF, les deux suivants sont vers des pages web classiques.

• λ‑calculus: then & now (turing100.acm.org). Dana S. Scott, Mai‑Août 2012;
• The lambda calculus (plato.stanford.edu). Jesse Alama, Décembre 2012;
• A graphical notation for the lambda calculus with animated reduction (dkeenan.com). David C Keenan, 1996‑2014.

Je recopie ici un message posté dans Les logiques : notes en vrac (page 6), et ajoute une référence plus bas.

‑‑‑‑‑‑‑‑‑‑ %< ‑‑‑‑‑‑‑‑‑‑‑‑‑‑‑ >% ‑‑‑‑‑‑‑‑‑‑

Les axiomes du lambda‑calcul dans un diaporama présentant les grandes lignes de l’inférence de types. C’est de troisième main, ces axiomes sont repris et repris… une source parmi d’autres.

An Introduction to Type Inference (cs.columbia.edu) [PDF], Alfred V. Aho, Novembre 2011.

À la diapositive № 5.




C’est simplifié, au moins pour le premier axiome, qui nécessite de s’assurer qu’une variable liée n’est pas renommée avec le nom d’un variable pré‑existante dans l’expression. […]

‑‑‑‑‑‑‑‑‑‑ %< ‑‑‑‑‑‑‑‑‑‑‑‑‑‑‑ >% ‑‑‑‑‑‑‑‑‑‑

À la fin du message d’origine, je parlais de la nécessité d’approfondir. Voici justement un article d’une encyclopédie de philosophie en ligne, qui le fait : Lambda Calculi (iep.utm.edu). Ou la version imprimable [1], plus agréable à lire à mes yeux : Lambda Calculi (version imprimable).


[1]: Pas sur papier hein, plutôt en PDF . Rien ne vaut jamais un gaspillage inutile.

L’application d’une fonction, est parfois nommée « combinaison » en français ou “combination” en Anglais. C’est au moins le cas pour HOL4, qui a une primitive nommée mk_comb, pour créer un terme qui est l’application d’une fonction à un paramètre.

Notez qu’une instanciation (terme pas encore introduit ici jusque maintenant), n’est rien d’autre qu’une substitution. Dans son sens le plus courant dans les langages informatiques en général, c’est une substitution d’une valeur à une variable (substitutions multiple, si nécessaire). En particulier, on parle d’instanciation dans le lambda‑calcul typé, quand on substitue un type à une variable de type. L’instanciation a un sens plus général par ailleurs.

Une valeur monadique, est une valeur accompagnée d’un état ou d’annotations (prenez l’expression qui vous parle le plus), et d’une fonction ou d’un opérateur (prenez le mot que vous préférez) interprétant cette valeur dans cet état ou cette valeur annotée.

Deux fonctions primitives s’appliquent aux monades : bind — souvent notée >>= — et return — parfois notée unit. Plus à ce sujet, peu après.

Les fonctions bind et return, doivent vérifier trois règles :

• Identité à droite : return x >>= f ≡ fx
• Identité à gauche : x >>= return ≡ x
• Associativité : (x >>= f) >>= g ≡ x >>= (f >>= g)

Bind, prend une valeur annotée pour en tirer une valeur non‑annotée, quand c’est possible, car ça ne l’est pas toujours. Si on note la valeur annotée, [x], et la valeur non‑annotée, x, alors bind permet de relier une fonction f: x -> [y] et une fonction g: y -> [z] pour obtenir [z]. Elle permet de prendre [y] venant de f et de passer le y qu’elle en tire, pour le passer à g pour finir avec [z], le résultat de l’expression.

Imaginons un cas en particulier, ou [y] est renvoyé par une fonction de division, et que l’annotation que peut porter [y], et de savoir si oui ou non, [y] est le résultat d’une division par zéro. Si c’est le résultat d’une division par zéro, alors il n’existe pas de y qui puisse être passé en argument, de par exemple une fonction d’addition. C’est pour cette raison que bind est nécessaire et qu’il n’en existe pas de définition unique. Pour rester concis, je ne dis pas ce que bind peut renvoyer quand il n’est pas possible d’extraire un y de [y].

Bind ne doit pas être confondue avec la composition de deux fonctions. Il n’existe en effet qu’une seule définition mathématique de la composition de deux fonctions, tandis qu’il n’existe pas de définition unique de bind, il y en a une pour chaque type monadique défini (les deux sont définis ensemble). Et bind ne renvoi pas une fonction, mais une valeur monadique, ce qui la ferait plutôt qualifier de fonction d’application.

Attention à ne pas confondre le type unit de SML avec unit, l’alias du return monadique. Le return monadique, est également différent du return des langages les plus courants. Attention à ne pas confondre le bind monadique avec le bind de JavaScript, même si on peut leur trouver des similitudes sémantiques.

Les monades, un terme mathématique, sont parfois appelées “computation expression” ou “computation builder”.

Une définition de l’interface abstraite des monades, en SML :



La fonction return, permet de définir une fonction monadique. Une fonction monadique, est une fonction retournant une valeur monadique, mais dont le paramètre est une valeur « normale ». La fonction bind, permet de lier deux fonctions monadiques, d’où son nom. Mais comme dit précédemment, attention à ne pas prendre bind pour une fonction de composition générale.

Pour un définition de alpha‑équivalence, voir : Re: Les logiques : notes en vrac.

Voir aussi le message « Re: Les logiques : notes en vrac », pour la mention d’un livre important.

Il me semble que les constantes pourraient être définies comme les paramètres d’une expression englobante, ou plutôt de plusieurs expressions englobantes, comme les paramètres multiples sont exprimés par curryfication.