Fully abstract submodels of typed lambda calculi (Q1095880)

Let \(M=(D^{\tau},\cdot,A)\) be the classical model based on complete lattices, for the typed lambda calculus \({\mathcal L}\). That is, \(D^{\tau}\) is an \(\omega\)-algebraic complete lattice for every type \(\tau\), the application operator ``\(\cdot\)'' is continuous and \(A\) is a homomorphic type-preserving map from \({\mathcal L}\) to \(\cup_{\tau}D^{\tau}\). The paper provides the construction of an extensional, fully abstract and algebraic submodel of M, denoted \(M^ Q=(Q^{\tau},\cdot,A^ Q)\), where the \(Q^{\tau}\)'s are homomorphic retractions of the \(D^{\tau}\)'s and ``\(\cdot\)'' for \(M^ Q\) is simply the restriction of ``\(\cdot\)'' for M. \(M^ Q\) is in fact the ``limit'' of some sequence of approximate finite submodels \(M^ Q_ i\). The technique of inclusive predicates is used. Milner's unique fully abstract model can be recovered from \(M^ Q\), and the given construction can be extended to hold reflexive types (in this case, the existence of the defined inclusive predicates must be proved). The question of how this technique could be extended to deal with \(P\omega\)-models may have connections with \textit{I. Bethke}'s work [e.g., Indag. Math. 48, 243-257 (1986; Zbl 0619.03013)].