1,720,974 research outputs found
An irregular filter model.
No full textIn this paper we introduce a new filter model, which is of a kind that has escaped investigation up to now: it is induced by an intersection type theory generated in a non-standard way, by a preorder which puts into relation an atom with an arrow type, without equating them. We study the domain-theoretic implications of this choice, that are not trivial: in order to describe this filter model a new category is introduced and a special purpose functor defined. The filter model is then characterized as the initial algebra of the functor
Tiered Objects
Full text linkWe investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects
A complete characterization of complete intersection-type preorders
No full textWe characterize those type preorders which yield complete intersection-type assignment systems for λ-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics, and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of thepreorder relation, ≤≤, set-theoretic inclusion, as interpretation of the intersection constructor, ∩, set-theoretic intersection, and by taking the interpretation of the arrow constructor, ← à la Scott, with respect to either any possible functionality set, or the largest one, or the least one. These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Second, the characterizations are all given just in terms of simple closure conditions on the preorder relation, ≤, on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Last, we do not restrict attention just to λ-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted λ-calculi. Nevertheless the characterizations we give can be tailored just to the case of λ-models
Intersection types and lambda models
No full textInvariance of interpretation by beta-conversion is one of the minimal requirements for any standard model for the gimel-calculus. With the intersection-type systems being a general framework for the study of semantic domains for the gimel-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results for intersection-type assignment systems. Instead of considering conversion as a whole, reduction and expansion will be considered separately. Not only for usual computational rules like beta, eta, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed gimel-models. (c) 2006 Elsevier B.V. All rights reserved
Simple Easy Terms
No full textWe illustrate the use of intersection types as a semantic tool for proving easiness result on λ-terms. We single out the notion of simple easiness for λ-terms as a useful semantic property for building filter models with special purpose features. Relying on the notion of easy intersection type theory, given λ-terms M and E, with E simple easy, we successfully build a filter model which equates interpretation of M and E, hence proving that simple easiness implies easiness. We finally prove that a class of λ-terms generated by ω2 ω2 are simple easy, so providing alternative proof of easiness for them. © 2002 Published by Elsevier Science B.V
A Characterization of Distance between 1-Bounded Compact Ultrametric Spaces through a Universal Space
Full text linkThe category of 1-bounded compact ultrametric spaces (KUMs) and non-distance increasing functions has been extensively used in the semantics of concurrent programming languages. In this paper a universal space U for KUMs is introduced, such that each KUM can be isometrically embedded in it. The space U consists of a suitable subset of the space of functions from [0, 1) to N, endowed with a "prefix-based" ultrametric. U allows to characterize the distance between KUMs introduced in Alessi et al. (1995) in terms of the Hausdorff distance between its compact subsets. As applications, it is proved how to derive the existence of limits for Cauchy towers of spaces without using the classical categorical construction and how to find solutions of recursive domain equations inside P-nco(U)
Recursive Domain Equations of Filter Models.
No full textFilter models and (solutions of) recursive domain equations are two different ways of constructing lambda models. Many partial results have been shown about the equivalence between these two constructions (in some specific cases). This paper deepens the connection by showing that the equivalence can be shown in a general framework. We will introduce the class of disciplined intersection type theories and its four subclasses: natural split, lazy split, natural equated and lazy equated. We will prove that each class corresponds to a different recursive domain equation. For this result, we are extracting the essence of the specific proofs for the particular cases of intersection type theories and making one general construction that encompasses all of them. This general approach puts together all these results which may appear scattered and sometimes with incomplete proofs in the literature
Solutions of Functorial and Non-Functorial Metric Domain Equations
No full textA new method for solving domain equations in categories of metric spaces is studied. The categories CMS ≈ and KMS ≈ are introduced, having complete and compact metric spaces as objects and ε-adjoint pairs as arrows. The existence and uniqueness of fixed points for certain endofunctors on these categories is established. The classes of complete and compact metric spaces are considered as pseudo-metric spaces, and it is shown how to solve domain equations in a non-categorical framework
Intersection types and domain operators
No full textWe use intersection types as a tool for obtaining lambda-models. Relying on the notion of easy intersection type theory, we successfully build a lambda-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the lambda-theory where the lambda-term (lambdax.xx)(lambdax.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of lambda-theories. The second result is that for any simple easy term, there is a lambda-model, where the interpretation of the term is the minimal fixed point operator. (C) 2004 Elsevier B.V. All rights reserved
- …
