Lambda theories of effective lambda models

Details Lambda theories of effective lambda models Lambda theories of effective lambda models

2007-01-24

arxiv.org/abs/math/0701684v2

Mathematics

Logic

15 pages, accepted CSL'07

Scientific paper

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).

Affiliated with

Also associated with

No associations

Rating

Lambda theories of effective lambda models does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Lambda theories of effective lambda models, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Lambda theories of effective lambda models will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-603765