Lambda expression en B

ou comment définir une fonction

Première construction

lambda . (x : s | E)

où s est un ensemble, x une variable non libre dans s, E une expression

ce qui se définit comme l'ensemble suivant :
{x, y | (x, y) : s * t & y = E} avec
x et y des variables non libres dans s et t, y n'étant de plus pas libre dans E, s et t sont des ensembles, E une expression, avec la condition suivante : ! x . (x : s => E : t)

Exemple :

lambda x . (x : NAT | x * x)
se définit comme l'ensemble :
{x, y | (x, y) : NAT * NAT & y = x*x}

lambda x . (x : NAT | x * x) (3) dénote l'application de la fonction au nombre naturel 3, i.e. dénote 9.

Deuxième construction

lambda x . (x : s & P | E)
avec x variable non libre dans s, E une expression et P un prédicat.
se définit comme l'ensemble :
{x, y | (x, y) : s * t & P & y = E} avec
x et y des variables non libres dans s et t, y n'étant de plus pas libre dans E, s et t sont des ensembles, E une expression, avec la condition suivante : ! x . (x : s & P => E : t)

Exemple :

lambda x . (x : NAT & x : NAT - {0} | 2 x) se définit comme l'ensemble :
{x, y| (x, y) : NAT * NAT & (x : NAT - {0}) & (y = 2x)}