# Effective lambda-models vs recursively enumerable lambda-theories

Effective lambda-models vs recursively enumerable lambda-theories - Download this document for free, or read online. Document in PDF available to download.

1 PPS - Preuves, Programmes et Systèmes 2 Dipartimento di Informatica

Abstract : A longstanding open problem is whether there exists a non syntactical model of the untyped lambda-calculus whose theory is exactly the least lambda-theory l-beta. In this paper we investigate the more general question of whether the equational-order theory of a model of the untyped lambda-calculus can be recursively enumerable r.e. for brevity. We introduce a notion of effective model of lambda-calculus calculus, which covers in particular all the models individually introduced in the literature. We prove that the order theory of an effective model is never r.e.; from this it follows that its equational theory cannot be l-beta or l-beta-eta. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. Concerning Scott-s semantics, we investigate the class of graph models and prove that no order theory of a graph model can be r.e., and that there exists an effective graph model whose equational-order theory is minimum among all theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards Lowenheim-Skolem theorem.

Keywords : lambda-calculus effective lambda-models effectively given domains recursively enumerable theories graph models Lowenheim-Skolem Theorem lambda-theories Visser topology Scott-s semantics

Author: ** Chantal Berline - Giulio Manzonetto - Antonio Salibra - **

Source: https://hal.archives-ouvertes.fr/