Lambda abstraction expliquée (1).pdf

Dr Gildas Nzokou Maître de Conférences Invité Département de Philosophie Faculté des Humanités/ Université Lille 3 Charles De Gaulle

Lambda abstraction dans la Théorie Constructive des Types Lecture explicative

Abstraction Lambda dans la Théorie Constructiviste des Types (TCT) Lecture explicative

Introduction : Dans ce qui suit, nous allons introduire un dispositif technique qui joue un rôle crucial dans la TCT, notamment l’opérateur d’abstraction Lambda. La fonction d’abstraction Lambda accroît le pouvoir d’expressivité des différents langages dans lesquels cette dernière est utilisée, en ce qu’elle permet de rendre formellement signifiantes certaines expressions telles que les prédicats complexes, la représentation compréhensive des ensembles de n’importe quelle grandeur. Et c’est le point de l’intentionnalité que permet d’exprimer l’abstraction lambda qui la rend pertinente dans le développement du langage de la Théorie Constructive des Types. Mais avant d’en faire un exposé technique, nous allons premièrement faire un point très bref d’histoire de la philosophie des mathématiques de Frege, notamment un bref rappel de son analyse concernant l’identité des fonctions. De fait, dans son article intitulé « Fonction et concept » de 1891, Gottlob Frege interroge le sens de l’égalité de deux expressions fonctionnelles « x2 – 4x = x (x – 4) » qui, intentionnellement, n’opèrent pas de la même manière mais ont pourtant un graphe identique pour n’importe quelle valeur prise de la variable. Cette égalité d’expressions propositionnelles reçoit trois lectures possibles et chacune entraînant une prise de position théorique particulière de Frege : a) La première lecture consisterait à y voir comme une identité (qualitative) entre des fonctions, toute chose que rejette Frege d’office. Car, à l’évidence x2 – 4 n’est pas la même chose que x (x – 4) même si elles ont même valeur finale. b) La deuxième lecture revenait à considérer l’équation « x2 – 4x = x (x – 4) » comme une proposition universelle quantifiée, c’est-à-dire, si nous l’exprimons dans la notation contemporaine : x (x2 – 4 = x (x – 4)) c) La troisième lecture – à laquelle souscrit Frege – c’est que les deux fonctions considérées ont en commun un même parcours de valeurs ; c’est-à-dire que les courbes de leurs graphes respectifs coïncident. Frege parlera alors de « parcours de valeurs », comme d’un objet autosubsistant (selon les mots d’Anthony Kenny), pour nommer l’extension des fonctions. Frege affirme que l’égalité entre expressions fonctionnelles – qu’il assimile à l’égalité des parcours de valeurs – est indémontrable et que ceci devrait être considéré comme une notion primitive, qu’on retrouve dans la notation de Frege comme suit : « ̛ (2 −) = ̛   − )) »1

1

Gottlob Frege, 1891, « Fonction et Concept » ; Conférence prononcée devant la Société savante de Iéna pour la médecine et les sciences naturelles le 9 Janvier et publiée la même année sous forme d’un livret de 31 pages. Traduction de Claude Imbert dans ; Gottlob Frege. Écrits logiques et philosophiques, Paris, éditions du Seuil, 1971, Coll. de poche « Essais » 1

Dr Gildas Nzokou Maître de Conférences Invité Département de Philosophie Faculté des Humanités/ Université Lille 3 Charles De Gaulle

Lambda abstraction dans la Théorie Constructive des Types Lecture explicative

Le développement du dispositif d’abstraction-Lambda et sa généralisation trouve son origine dans le calcul lambda, système formel inventé aux environs des années 1928 par Alonzo Church dans le but d’atteindre un fondement solide à la science de la logique. L’abstraction Lambda devait en fait prendre le relais de la fonction qu’utilisait Russell en 1913 dans les Principia Mathematica pour l’abstraction de classes. Le calcul Lambda devait généraliser la notion de « fonction » et celle d’ « application », de sorte qu’elle développe une théorie intensionnelle des fonctions. Ce qui lui a donné un vaste champ d’applications notamment dans les sciences de la computation (pour le développement des langages de programmation), la linguistique computationnelle (les grammaires catégorielles de Montague), la Logique formelle et les fondements des mathématiques. L’abstraction Lambda en propre. Techniquement parlant, l’opération d’abstraction Lambda  permet de traiter avec pertinence la sémantique des expressions telles que les prédicats complexes (« marcher lentement » = prédicat joint à un adverbe modal), l’indication précise d’une classe complète de solutions à un problème traité par inférence, l’écriture d’un programme informatique, etc. Pour les nécessités de notre cours sur la TCT, nous allons d’abord, et ce brièvement, montrer comment travaille l’abstraction lambda dans le champ de la linguistique (sémantique formelle). Les règles d’écriture habituelles des expressions lambda-abstraites sont les suivantes :  Soit v une variable individuelle d’un langage de premier ordre, et  une formule quelconque dans laquelle v a des occurrences libres, l’expression v se lit : « la propriété d’être telle que  est vraie ». Autrement dit, nous avons affaire ici à un prédicat qui nous est donné de manière intensionnelle, c’est-à-dire que nous avons obtenu un prédicat par abstraction d’une classe d’objets.  Et lorsque cette expression prend un argument dans sa portée telle que : v, on lit : «  a la propriété d’être telle que  est vraie »  Et la règle de conversion Lambda fixe que : v  v/ ; c’est-à-dire que  a la propriété d’être telle que  est vraie si et seulement si, le résultat obtenu après substitution uniforme de toutes les occurrences libres de v dans  nous donne une phrase vraie. Cet usage de l’abstraction lambda a l’avantage de traiter de manière généralisée et uniforme, tous types de prédicats : les prédicats complexes, les prédicats relationnels, les prédicats de deuxième ordre et d’ordres supérieurs, les fonctions également. L’usage de l’abstracteur  dans la Théorie Constructive des Types (TCT par abréviation), intervient au niveau des règles d’introduction de l’implication matérielle et du quantificateur universel. De manière élémentaire, le point de vue constructiviste interprète une implication comme le lien qu’il y a entre une condition et sa conséquence. De sorte que pour prouver un conditionnel matériel, on fait l’hypothèse de l’antécédent et on voit s’il est effectif qu’on infère le conséquent. Si tel est le cas, alors la preuve de la proposition conséquente est fonction de la preuve de la proposition antécédente. Mais étant donné qu’en TCT on considère les propositions comme des types, qui eux-mêmes sont les ensembles de leurs propres preuves (d’où a : A se lit « a est un élément canonique, c’est-à-dire une preuve, de A »), alors l’ensemble des preuves d’une proposition implicative est une fonction des preuves de l’antécédent vers les preuves du conséquent. Et c’est ici qu’intervient la fonction d’abstraction Lambda. Celle-ci nous donne par abstraction, pour une proposition   , la classe des preuves « a » de  qui prouvent . D’où l’écriture suivante de la règle d’introduction du conditionnel matériel : 2

Dr Gildas Nzokou Maître de Conférences Invité Département de Philosophie Faculté des Humanités/ Université Lille 3 Charles De Gaulle

Lambda abstraction dans la Théorie Constructive des Types Lecture explicative

a :  . . b: (a), b :    De même, la règle constructiviste d’introduction du quantificateur universel se donne comme suit : x : A . . b(x) : B (x), b(x) : (x :A) Bx Ici, nous comprenons que la dépendance de l’élément canonique b(x) du type B à l’égard de l’élément canonique x du type A est en fait l’expression d’une fonction. Et l’abstraction Lambda permet de donner intensionnellement la classe complète des éléments canoniques de B qui dépendent du type A. Cette lecture trouve son fondement dans le travail de Church qui consistât à montrer que tout est fonction ; en ce sens nous disons que si, étant donné une variable x de type A nous avons construit un terme b(x) de type B, alors nous pouvons former le lambda terme (x)b(x) du type fonction A  B. Dans b(x) la variable x a une occurrence libre et n’est liée que par l’opérateur Lambda x. Une chose qui nous donne une acuité visuelle ici c’est de remarquer que les hypothèses non-déchargées sont représentées par les variables libres tandis que les hypothèses déchargées sont indiquées par la variable liée. NB : L’abstraction Lambda est une fonction qui nous donne comme résultat un objet indépendant. Ici, la classe des éléments canoniques de A qui prouvent B est un objet auto-subsistant, comme le nommait Frege. Lambda ne nous donne pas comme résultat une fonction ; plutôt, c’est une fonction qui nous permet d’abstraire un objet autonome. Et donc (x)b(x) est un objet théorique à part entière qui est indépendant dans ce contexte d’utilisation.

3