Linear types and approximation

2000 ◽  
Vol 10 (6) ◽  
pp. 719-745 ◽  
Author(s):  
MICHAEL HUTH ◽  
ACHIM JUNG ◽  
KLAUS KEIMEL
Keyword(s):  
Full Subcategory ◽  
Linear Logic ◽  
Domain Theory ◽  
Classical Domain ◽  
Complete Distributivity ◽  
Linear Types ◽  
Continuous Lattices

We study continuous lattices with maps that preserve all suprema rather than only directed ones. We introduce the (full) subcategory of FS-lattices, which turns out to be *-autonomous, and in fact maximal with this property. FS-lattices are studied in the presence of distributivity and algebraicity. The theory is extremely rich with numerous connections to classical Domain Theory, complete distributivity, Topology and models of Linear Logic.

scholarly journals Bistructures, Bidomains and Linear Logic

1994 ◽  
Vol 1 (9) ◽  
Author(s):  
Gordon Plotkin ◽  
Glynn Winskel
Keyword(s):  
Partial Order ◽  
Full Subcategory ◽  
Linear Logic ◽  
The Other ◽  
Causal Dependency ◽  
Input And Output ◽  
Event Structures ◽  
Kleisli Category ◽  
Higher Types ◽  
Cartesian Closed

Bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry's bidomains.

scholarly journals Domain Theory for Concurrency

2003 ◽  
Vol 10 (43) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Higher Order ◽  
The Other ◽  
Domain Theory ◽  
Parallel Composition ◽  
Concurrent Computation ◽  
Contextual Equivalence

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency.

scholarly journals A Model of Intuitionistic Affine Logic from Stable Domain Theory (Revised and Expanded Version)

1994 ◽  
Vol 1 (27) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
Alternative Model ◽  
Linear Logic ◽  
Canonical Model ◽  
Domain Theory ◽  
Left Adjoint ◽  
Stable Maps ◽  
Stable Domain ◽  
Intuitionistic Linear Logic ◽  
Coherence Spaces

Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model of Linear Logic. Now, the same phenomenon is present if we consider the category of pre dI domains and continuous stable maps, and the category of dI domains and linear stable maps; the functor that forgets the linearity has a left adjoint. This gives an alternative model of Intuitionistic Linear Logic. It turns out that this adjunction can be factored in two adjunctions yielding a model of Intuitionistic Affine Logic; the category of pre dI domains and affine stable functions. It is the goal of this paper to show that this category is actually a model of Intuitionistic Affine Logic, and to show that this category moreover has properties which make it possible to use it to model convergence/divergence behaviour and recursion.

An operational domain-theoretic treatment of recursive types

2013 ◽  
Vol 24 (1) ◽  
Author(s):  
WENG KIN HO
Keyword(s):  
Operational Semantics ◽  
Domain Theory ◽  
Invariance Property ◽  
Inverse Limits ◽  
Classical Domain ◽  
Contextual Equivalence

We develop an operational domain theory for treating recursive types with respect to contextual equivalence. The principal approach we take deviates from classical domain theory in that we do not produce the recursive types using the usual inverse limits constructions – we get them for free by working directly with the operational semantics. By extending type expressions to functors between some ‘syntactic’ categories, we establish algebraic compactness. To do this, we rely on an operational version of the minimal invariance property, for which we give a purely operational proof.

scholarly journals On traced monoidal closed categories

2009 ◽  
Vol 19 (2) ◽  
pp. 217-244 ◽  
Author(s):  
MASAHITO HASEGAWA
Keyword(s):  
Fixed Point ◽  
Full Subcategory ◽  
Monoidal Category ◽  
Structure Theorem ◽  
Linear Logic ◽  
Monoidal Categories ◽  
Simple Observation ◽  
Fixed Point Computation ◽  
Canonical Inclusion ◽  
Monoidal Closed Category

The structure theorem of Joyal, Street and Verity says that every traced monoidal category arises as a monoidal full subcategory of the tortile monoidal category Int. In this paper we focus on a simple observation that a traced monoidal category is closed if and only if the canonical inclusion from into Int has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts for traced models of linear logic, and some for models of fixed-point computation. To make the paper more self-contained, we also include various background results for traced monoidal categories.

From parametric polymorphism to models of polymorphic FPC

2009 ◽  
Vol 19 (4) ◽  
pp. 639-686 ◽  
Author(s):  
RASMUS EJLERS MØGELBERG
Keyword(s):  
Fixed Point ◽  
Intuitionistic Logic ◽  
Classical Result ◽  
Linear Logic ◽  
Lambda Calculus ◽  
Parametric Models ◽  
Domain Theory ◽  
Adequate Model ◽  
Typed Lambda Calculus ◽  
Parametric Polymorphism

This paper shows how PILLY(Polymorphic Intuitionistic/Linear Lambda calculus with a fixed point combinatorY) with parametric polymorphism can be used as a metalanguage for domain theory, as originally suggested by Plotkin more than a decade ago. Using Plotkin's encodings of recursive types in PILLY, we show how parametric models of PILLYgive rise to models of FPC, which is a simply typed lambda calculus with recursive types and an operational call-by-value semantics, reflecting a classical result from domain theory. Essentially, this interpretation is an interpretation of intuitionistic logic into linear logic first discovered by Girard, which in this paper is extended to deal with recursive types. Of particular interest is a model based on ‘admissible’ pers over a reflexive domain, the theory of which can be seen as a domain theory for (impredicative) polymorphism. We show how this model gives rise to a parametric and computationally adequate model of PolyFPC, an extension of FPC with impredicative polymorphism. This is to the author's knowledge the first denotational model of a non-linear language with parametric polymorphism and recursive types.

scholarly journals A General Adequacy Result for a Linear Functional Language

1994 ◽  
Vol 1 (22) ◽  
Author(s):  
Torben Braüner
Keyword(s):  
General Result ◽  
Functional Programming ◽  
Linear Functional ◽  
Linear Logic ◽  
Domain Theory ◽  
Main Concern ◽  
Functional Language ◽  
Stable Domain ◽  
Categorical Semantics ◽  
Intuitionistic Linear Logic

A main concern of the paper will be a Curry-Howard interpretation of Intuitionistic Linear Logic. It will be extended with recursion, and the resulting functional programming language will be given operational as well as categorical semantics. The two semantics will be related by soundness and adequacy results. The main features of the categorical semantics are that convergence/divergence behaviour is modelled by a strong monad, and that recursion is modelled by ``linear fixpoints'' induced by CPO structure on the hom-sets. The ``linear fixpoints'' correspond to ordinary fixpoints in the category of free coalgebras w.r.t. the comonad used to interpret the ``of course'' modality. Concrete categories from (stable) domain theory satisfying the axioms of the categorical model are given, and thus adequacy follows in these instances from the general result.

Sign in / Sign up

Export Citation Format

Share Document