A Convex Powerdomain over Lattices: its Logic and λ-Calculus

Article type: Research Article

Authors: Alessi, Fabio | Dezani-Ciancaglini, Mariangiola | Liguoro, Ugo de'

Affiliations: Dipartimento di Matematica e Informatica, Università di Udine, via delle Scienze 208, 33100 - Udine, ITALY. email: [email protected] | Dipartimento di Informatica, Università di Torino, corso Svizzera 185, 10149 - Torino, ITALY. email: dezani,[email protected]

Abstract: To model at the same time parallel and nondeterministic functional calculi we define a powerdomain functor Ρ such that it is an endofunctor over the category of algebraic lattices. Ρ is locally continuous and we study the initial solution D∞ of the domain equation D = Ρ([D → D]⊥). We derive from the algebras of Ρ the logic of D∞, that is the axiomatic description of its compact elements. We then define a λ-calculus and a type assignment system using the logic of D∞ as the related type theory. We prove that the filter model of this calculus, which is isomorphic to D∞, is fully abstract with respect to the observational Preorder of the λ-calculus.

Keywords: λ-calculus, Nondeterminism, Full Abstraction, Powerdomain Construction, Intersection Type Disciplines

DOI: 10.3233/FI-1997-323401

Journal: Fundamenta Informaticae, vol. 32, no. 3-4, pp. 193-250, 1997