complétude fonctionnelle de la LC
bur...@math.jussieu.fr
Si quelqu'un saurait me renseigner sur ce point technique :
En logique combinatoire, pour tout terme t(x) où x est une variable,
il existe une constante (un combinateur) a tel que :
t(x)=ax
C'est la *complétude fonctionnelle*.
C'est pour avoir, en plus de l'existence, l'unicité de cette constante
a qu'on ajoute au système les axiomes équationnels :
S(KI)x = x,
S(S(KK)x)y = x,
S(S(S(KS)x)y)z = S(Sxz)(Syz),
(si j'ai pas fait d'erreur en recopiant).
Ce qui m'intéresse c'est d'avoir une référence de preuve que c'est
nécessaire. Par exemple, une preuve que de SKIx = Ix on ne peut tirer
SKI = I. C'est ce que je vois affirmer dans Lambek quelque part, mais
sans références ou d'indications.
Amitiés,
Albert
----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.