A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for short). We introduce a notion of effective model of λ-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 λβ or λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. For 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 the minimum among the theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards L¨owenheim–Skolem theorem.

Effective lambda models versus recursively enumerable lambda theories

SALIBRA, Antonino
2009-01-01

Abstract

A longstanding open problem is whether there exists a non-syntactical model of the untyped λ-calculus whose theory is exactly the least λ-theory λβ. In this paper we investigate the more general question of whether the equational/order theory of a model of the untyped λ-calculus can be recursively enumerable (r.e. for short). We introduce a notion of effective model of λ-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 λβ or λβη. We then show that no effective model living in the stable or strongly stable semantics has an r.e. equational theory. For 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 the minimum among the theories of graph models. Finally, we show that the class of graph models enjoys a kind of downwards L¨owenheim–Skolem theorem.
2009
19
File in questo prodotto:
File Dimensione Formato  
VQR-berline-manzo-salibra.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 377.15 kB
Formato Adobe PDF
377.15 kB Adobe PDF   Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/31345
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact