On an open problem of Amadio and Curien: The finite antichain condition

Abstract: More than a dozen years ago, Amadio [Bifinite domains: stable case, in: Lecture Notes in Computer Science, vol. 530, 1991, pp. 16–33] (see Amadio and Curien, Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science, vol. 46, Cambridge University Press, 1998 as well) raised the question of whether the category of stable bifinite domains of Amadio–Droste [R.M. Amadio, Bifinite domains: stable case, in: Lecture Notes in Computer Science, vol. 530, 1991, pp. 16–33; M. Droste, On stable domains, Theor. Comput. Sci. 111 (1993) 89–101; M. Droste, Cartesian closed categories of stable domains for polymorphism, Preprint, Universität GHS Essen] is the largest cartesian closed full sub-category of the category of ω-algebraic meet-cpos with stable functions. An affirmative solution to this problem has two major steps: (1) Show that for any ω-algebraic meet-cpo D, if all higher-order stable function spaces built from D are ω-algebraic, then D is finitary (i.e., it satisfies the so-called axiom I); (2) Show that for any ω-algebraic meet-cpo D, if D violates MI ∞, then [D→D] violates either M or I. We solve the first part of the problem in this paper, i.e., for any ω-algebraic meet-cpo D, if the stable function space [D→D] satisfies M, then D is finitary. Our notion of (mub, meet)-closed set, which is introduced for step 1, will also be used for treating some example cases in step 2. [Copyright &y& Elsevier]