Lambda Theories of Effective Lambda Models

DOI10.1007/978-3-540-74915-8_22zbMATH Open1179.03020arXivmath/0701684OpenAlexW1495260436MaRDI QIDQ3608418FDOQ3608418

Authors: Giulio Manzonetto, Chantal Berline, Antonino Salibra 

Publication date: 5 March 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Abstract: A longstanding open problem is whether there exists a non-syntactical model of untyped lambda-calculus whose theory is exactly the least equational lambda-theory (=Lb). In this paper we make use of the Visser topology for investigating the more general question of whether the equational (resp. order) theory of a non syntactical model M, say Eq(M) (resp. Ord(M)) can be recursively enumerable (= r.e. below). We conjecture that no such model exists and prove the conjecture for several large classes of models. In particular we introduce a notion of effective lambda-model and show that for all effective models M, Eq(M) is different from Lb, and Ord(M) is not r.e. If moreover M belongs to the stable or strongly stable semantics, then Eq(M) is not r.e. Concerning Scott's continuous semantics we explore the class of (all) graph models, show that it satisfies Lowenheim Skolem theorem, that there exists a minimum order/equational graph theory, and that both are the order/equ theories of an effective graph model. We deduce that no graph model can have an r.e. order theory, and also show that for some large subclasses, the same is true for Eq(M).

Full work available at URL: https://arxiv.org/abs/math/0701684

Recommendations

• Effective λ-models versus recursively enumerable λ-theories
• Graph lambda theories
• Mathematical Foundations of Computer Science 2003
• Graph models of $\lambda$-calculus at work, and variations
• scientific article; zbMATH DE number 599151

zbMATH Keywords

lambda calculusgraph modelsLöwenheim-Skolem theoremeffective lambda modelsrecursively enumerable lambda theories

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (18)

• Decidability of all minimal models
• Models of \(\lambda\)-calculus and the weak MSO logic
• On the construction of stable models of untyped \(\lambda\)-calculus
• Effective λ-models versus recursively enumerable λ-theories
• On the equational consistency of order-theoretic models of the lambda-calculus
• Mathematical Foundations of Computer Science 2003
• Graph models of $\lambda$-calculus at work, and variations
• Title not available (Why is that?)
• On the characterization of models of \(\mathcal H^\ast\): the semantical aspect
• On the completeness of order-theoretic models of the \(\lambda \)-calculus
• Lambda theories allowing terms with a finite number of fixed points
• Varying \(\Lambda\) theory revisited
• Minimal \(\lambda\)-theories by ultraproducts
• Title not available (Why is that?)
• Order-incompleteness and finite lambda reduction models
• Constructive \(\lambda\)-models
• Graph lambda theories
• Effectively given domains and lambda-calculus models

This page was built for publication: Lambda Theories of Effective Lambda Models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3608418)