Sciweavers

Share
TLCA
2005
Springer

Continuity and Discontinuity in Lambda Calculus

8 years 11 months ago
Continuity and Discontinuity in Lambda Calculus
This paper studies continuity of the normal form and the context operators as functions in the infinitary lambda calculus. We consider the Scott topology on the cpo of the finite and infinite terms with the prefix relation. We prove that the only continuous parametric trees are B¨ohm and L´evy–Longo trees. We also prove a general statement: if the normal form function is continuous then so is the model induced by the normal form; as well as the converse for parametric trees. This allows us to deduce that the only continuous models induced by the parametric trees are the ones of B¨ohm and L´evy–Longo trees. As a first application, we prove that there is an injective embedding from the infinitary lambda calculus of the ∞η-B¨ohm trees in D∞. As a second application, we study the relation between the Scott topology on the prefix relation and the tree topologies. This allows us to prove that the only parametric tree topologies in which all context operators are continuo...
Paula Severi, Fer-Jan de Vries
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Paula Severi, Fer-Jan de Vries
Comments (0)
books