Effective lambda-models vs recursively enumerable lambda-theories

Details Effective lambda-models vs recursively enumerable lambda-theories Effective lambda-models vs recursively enumerable lambda-theories

2008-06-13

arxiv.org/abs/0806.2264v1

Mathematics

Logic

34 p

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Effective lambda-models vs recursively enumerable lambda-theories 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 Effective lambda-models vs recursively enumerable lambda-theories, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Effective lambda-models vs recursively enumerable lambda-theories will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-123492