Lambda-calcul

Introduction

Le Lambda-calcul est une façon abstraite de définir une fonction et ses arguments. Il formalise les opérations sur les fonctions elles-mêmes : c'est-à-dire des fonctions de fonctions.

Notation : la fonction carré : <math>x \rightarrow x^2</math> se note <math>\lambda x \cdot x^2 </math>

{} Exemple de fonction de fonction, la fonction <math>\circ</math> de composition s'écrit <math> \lambda f \lambda g \cdot (f (g(x))) </math> ou <math> \lambda f \; g \cdot (f (g(x))) </math>

Il faut noter que le symbole <math>\lambda</math> lie les variables qu'il introduit, on ne peut changer le nom de la variable liée dans la portée de l'expression sans changer toutes ses occurrences.

Syntaxe d'une formule lambda

soit <math>V</math> un ensemble de variables soit <math>L</math> l'ensemble des formules lambda construites à partir de <math>V</math>

• si <math>v\in V</math> alors <math>v \in L</math>
• si <math>F \in L</math> et <math>G \in L</math> alors <math>(F \; G) \in L</math> (composition )
• si <math>F \in L</math> et <math>v \in V</math> alors <math>\lambda x \cdot F</math> est une formule lambda (lambda-abstraction )
• rien d'autre n'est une formule lambda

Conversion

• le nom d'une variable liée n'a pas d'importance.
• <math>\lambda x \cdot (f \; x)</math> a le même sens que <math>\lambda y \cdot (f \; y)</math>
• il y a équivalence des lambda-termes par conversion des variables liées.

Application et réduction

• l'application d'une fonction est juste la substitution du ou des arguments
• <math>(\lambda x \cdot F)(y)=F[x/y]</math>
• ex: <math>(\lambda x \cdot x^2)3 = 3^2</math>
• on peut aussi appliquer des variables libres (NB: ici le résultat n'est plus une formule lambda):

<math>(\lambda x \lambda u \cdot x^2+u)(y+z)(t)=(y+z)^2+t</math>

Exemple d'utilisation en sémantique : compositionalité

Rappel express de logique

On considère pour l'exemple un langage de représentation logique, avec des termes, des prédicats, des propositions et des quantificateurs :

• termes : variables <math>x_i</math>, constantes <math>c_j</math>, images de fonctions <math>f(x)</math>
• propositions atomiques: prédicats <math>P(x), Q(x_1,x_2,x_3)</math>
• propositions construites avec <math>\neg</math> (négation), <math>\land</math> (et), <math>\vee</math>(ou), <math>\rightarrow</math> (implication matérielle): <math>P(x)\land \neg Q(y)</math>
• quantificateurs : <math>\exists</math>, <math>\forall</math> <math> \forall x [(oiseau(x)\land \neg pingouin(x)) \rightarrow vole(x)] </math>

Si l'on admet que la représentation de la phrase

Un homme dort

est la formule <math> \exists x \; (homme(x) \land dort(x)) </math>

Les questions à résoudre pour la construction du sens sont :

quelle est la contribution de chaque élément lexical à l'ensemble de la formule  ?

quelles sont les règles de combinaison de ces éléments qui donnent la formule finale ?

Prenons une petite grammaire hors-contexte comme exemple

S	<math>\rightarrow </math>	NP	V
NP	<math>\rightarrow</math>	D	N
N	<math>\rightarrow</math>	"homme"
D	<math>\rightarrow</math>	"un"
V	<math>\rightarrow</math>	"dort"

Forme Logique de "un"	<math>\rightarrow</math>	<math> \exists x ... </math>
FL de "dort"	<math>\rightarrow</math>	prédicat
FL de "homme"	<math>\rightarrow</math>	prédicat

Le lambda-calcul est une façon abstraite de définir une fonction et ses arguments, on va ici n'utiliser que des fonctions dont le résultat final est une formule logique du premier ordre.

ex: <math>\lambda x (oiseau(x))</math> est la représentation lambda du prédicat oiseau vu comme une fonction booléenne.

Par composition et réduction de formules lambda

<math>\lambda x (oiseau(x))](y)</math> donne <math> oiseau(y) </math>.

Les arguments des fonctions peuvent être des prédicats ou même des formules :

<math> \lambda P (\exists x (oiseau(x) \land P(x))</math>.

Exemple (suite)

Il faut considérer la sémantique des expressions comme des lambda-abstractions en attente de leurs arguments. Ainsi la sémantique d'un verbe peut être :

<math> [\![dort]\!] = \lambda x\cdot dort(x) </math>

Celle d'un nom commun est similaire :

<math> [\![homme]\!] = \lambda x\cdot homme(x) </math>

Et celle du déterminant peut aussi s'écrire :

<math> [\![un]\!] = \lambda P\lambda R\cdot (\exists x \; P(x) \land R(x)) </math>

Le processus de traduction correspond à des schémas d'application liées aux règles de la grammaire :

category1(sem:f(semNP,semVP)) <math>\rightarrow</math> categorie2(sem:semNP) categorie3(sem:semVP)

avec ici, f = application lambda.

En faisant toujours l'application de categorie3 comme argument de categorie2 et en reportant les applications successives sur l'arbre d'analyse syntaxique, on voit :

Relecture en cours Les commentaires des relecteurs de cet article n'ont pas encore été intégrés. Il n'est peut-être donc pas dans sa forme définitive.