loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
The Sensible Graph Theories of Lambda Calculus
Turku, Finland
July 13-July 17
ISBN: 0-7695-2192-4
Antonio Bucciarelli, Universit? Paris 7, France
Antonino Salibra, Universit? Ca'Foscari di Venezia, Italia
Sensible λ-theories are equational extensions of the untyped lambda calculus that equate all the unsolvable λ-terms and are closed under derivation. A longstanding open problem in lambda calculus is whether there exists a non-syntactic model whose equational theory is the least sensible λ-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of models, there exist a minimal and maximal sensible λ-theory represented by it. In this paper we give a positive answer to this question for the semantics of lambda calculus given in terms of graph models. We conjecture that the least sensible graph theory, where "graph theory" means "λ-theory of a graph model", is equal to H, while in the main result of the paper we characterize the greatest sensible graph theory as the λ-theory B generated by equating λ-terms with the same B?hm tree. This result is a consequence of the fact that all the equations between solvable λ-terms, which have different B?hm trees, fail in every sensible graph model. Further results of the paper are: (i) the existence of a continuum of different sensible graph theories strictly included in B (this result positively answers Question 2 in [7, Section 6.3]); (ii) the non-existence of a graph model whose equational theory is exactly the minimal lambda theory λβ (this result negatively answers Question 1 in [7, Section 6.2] for the restricted class of graph models).
Citation:
Antonio Bucciarelli, Antonino Salibra, "The Sensible Graph Theories of Lambda Calculus," lics, pp.276-285, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.