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

TL;DR

This paper characterizes models of untyped lambda calculus that are fully abstract for head-normalization, showing that hyperimmunity of extensional K-models is the key property, with a purely syntactical proof provided.

Contribution

It provides a syntactical proof characterizing fully abstract models for head-normalization in lambda calculus, focusing on hyperimmune K-models.

Findings

Fully abstract models are exactly the hyperimmune extensional K-models.

A purely syntactical proof of the characterization is presented.

The result applies to a large class of models of untyped lambda calculus.

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 $\mathcal{H}^*$. An extensional K-model $D$ is fully abstract if and only if it is hyperimmune, i.e., non-well founded chains of elements of $D$ cannot be captured by any recursive function. This article share its first title with its companion paper and a short version. It is a standalone paper that present a purely syntactical proof of the result as opposed to its companion paper that present an independent and purely semantical proof of the exact same result.