On étudie la question de l’existence d’un modèle non-syntaxique du lambda calcul appartenant aux sémantiques principales et ayant une théorie équationnelle ou inéquationnelle r.e. (récursivement énumérable).
Cette question est une généralisation naturelle du problème de Honsell et Ronchi Della Rocca (ouvert depuis plus que vingt ans) concernant l’existence d’un modèle continu de lambda-beta ou lambda-beta-eta. On introduit une notion adéquate de modèles effectifs du lambda-calcul, qui couvre en particulier tous les modèles qui ont été introduits individuellement en littérature, et on prouve que la théorie inéquationnelle d’un modèle effectif n’est jamais r.e.; en conséquence sa théorie équationnelle ne peut pas être lambda-beta ou lambda-beta-eta.
On montre aussi que la théorie équationnelle d’un modèle effectif vivant dans la sémantique stable ou fortement stable n’est jamais r.e. En ce qui concerne la sémantique continue de Scott, on démontre que la théorie inéquationnelle d’un modèle de graphe n’est jamais r.e. et qu’il existe beaucoup de modèles de graphes effectifs qui ont une théorie équationnelle qui n’est pas r.e.