Name
Abstract | ||
|---|---|---|
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öhm and Lévy–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öhm and Lévy–Longo trees. As a first application, we prove that there is an injective embedding from the infinitary lambda calculus of the ∞η-Böhm 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 continuous and the approximation property holds are the ones of Böhm and Lévy–Longo. As a third application, we give an explicit characterisation of the open sets of the Böhm and Lévy–Longo tree topologies. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11417170_27 | TLCA |
Keywords | Field | DocType |
continuous model,longo tree topology,prefix relation,scott topology,parametric tree,longo tree,normal form,hm tree,infinitary lambda calculus,context operator,approximation property,lambda calculus | Discrete mathematics,Continuous function,Lambda calculus,Embedding,Type theory,Parametric statistics,Operator (computer programming),Approximation property,Mathematics,Open set | Conference |
Volume | ISSN | ISBN |
3461 | 0302-9743 | 3-540-25593-1 |
Citations | PageRank | References |
6 | 0.60 | 11 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paula Severi | 1 | 122 | 16.19 |
| Fer-Jan de Vries | 2 | 244 | 21.67 |