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

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: Paula Severi, Fer-Jan de Vries
• Keywords: Infinitary Lambda Calculus, Normal Form, Parametric Tree, Theoretical Computer Science, TLCA 2005