On the characterization of models of H*: The semantical aspect

TL;DR

This paper characterizes fully abstract models of untyped lambda-calculus for head-normalization, showing that hyperimmunity of extensional K-models is equivalent to full abstraction for H*.

Contribution

It provides a purely semantical proof of the characterization of fully abstract models for H*, contrasting with a syntactical proof in its companion paper.

Findings

Hyperimmune K-models are fully abstract for H*

Full abstraction is characterized by hyperimmunity

Semantic proof differs from syntactical approaches

Abstract

We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H* (observations for head normalization). An extensional K-model $D$ is fully abstract if and only if it is hyperimmune, {\em i.e.}, not well founded chains of elements of D cannot be captured by any recursive function. This article, together with its companion paper, form the long version of [Bre14]. It is a standalone paper that presents a purely semantical proof of the result as opposed to its companion paper that presents an independent and purely syntactical proof of the same result.