λ-calcul binaire

• fr:Lambda-calcul

John Tromp a mis au point le λ-calcul binaire comme programmation suffisamment puissante pour écrire un programme avec le moins de bits possible pouvant s’approcher au plus près de la complexité de Kolmogorov.

« Compléxité de Kolmogorov : un nombre comme étant la longueur du plus petit programme nécessaire pour calculer ce nombre. Un nombre complètement aléatoire ne peut être décrit par aucun programme plus court que le nombre lui-même, et possède donc une complexité de Kolmogorov maximale (on rejoint ici le concept d’entropie, qui est maximale quand les données sont aléatoires). Exemple : “la la la la la la la la la la la la la la la la la la la la” contient assez peu d’information, résumée dans l’algorithme “écrire 20 fois le mot ‘la’” »

Le langage de John Tromp est issu du λ-calcul, pour lequel tout programme est une expression, qui ne peut être que l’une des 3 formes suivantes :

• Une variable, de la forme x, y, z ou n’importe quelle autre lettre
• Une abstraction, de la forme (λx.a), où x est une variable et a est une autre expression
• Une application, de la forme (a b), où a et b sont deux autres expressions

Plus précisément, λ-calcul binaire définit une machine universelle qui, à partir d'un flux de bits d'entrée, analyse l'encodage binaire d'un terme de calcul lambda, applique cela au reste de l'entrée (traduit en une liste « ennuyeuses de booléens, qui ont une représentation standard en calcul lambda), et traduit le résultat évalué en une serie de bits en sortie.

• Entropie, exergie et information, Blog de Cyril Deguet 2013
• Mesurer la complexité des programmes grâce au λ-calcul binaire, Blog de Cyril Deguet 2013
• John's Lambda Calculus and Combinatory Logic Playground
• The art of obfuscation
• IOCCC 2012, Tromp
• Functional Bits: Lambda Calculus based Algorithmic Information Theory, John TrompMay 10, 2018
• Introduction au lambda-calcullogique combinatoire, Pierre Lescanne, ENS Lyon, 2012
• Introduction au lambda-calcul pur Yves Bertot, INRIA 2006