We show that the standard normalization-by-evaluation construction for the simply-typed ${\lambda }_{\beta \eta }$-calculus has a natural counterpart for the untyped ${\lambda }_{\beta }$-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...

We show that the standard normalization-by-evaluation construction for the simply-typed λβη-calculus has a natural counterpart for the untyped λβ-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal...

Let $C_p\left(X\right)$ be the space of continuous real-valued functions on X, with the topology of pointwise convergence. We consider the following three properties of a space X: (a) $C_p\left(X\right)$ is Scott-domain representable; (b) $C_p\left(X\right)$ is domain representable; (c) X is discrete. We show that those three properties are mutually equivalent in any normal T₁-space, and that properties (a) and (c) are equivalent in any completely regular pseudo-normal space. For normal spaces, this generalizes the recent result of Tkachuk that $C_p\left(X\right)$ is...

We study domain-representable spaces, i.e., spaces that can be represented as the space of maximal elements of some continuous directed-complete partial order (= domain) with the Scott topology. We show that the Michael and Sorgenfrey lines are of this type, as is any subspace of any space of ordinals. We show that any completely regular space is a closed subset of some domain-representable space, and that if X is domain-representable, then so is any $G_{\delta }$-subspace of X. It follows that any Čech-complete...