z-logo
open-access-imgOpen Access
A Model of Intuitionistic Affine Logic from Stable Domain Theory (Revised and Expanded Version)
Author(s) -
Torben Braüner
Publication year - 1994
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v1i27.21639
Subject(s) - mathematics , functor , adjunction , linear logic , affine transformation , pure mathematics , recursion (computer science) , enriched category , category of topological spaces , algebra over a field , discrete mathematics , algorithm , biochemistry , chemistry , topological tensor product , functional analysis , gene
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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.
Having issues? You can contact us here