Category: CMUTR
Institution: Department of Computer Science, Carnegie
        Mellon University
Abstract: We explore some foundational issues in the development of a 
        theory of intensional semantics.
        A programming language may be given a variety of semantics, 
        differing in the level of abstraction; one generally chooses the
        semantics at an abstraction level appropriate for reasoning 
        about a particular kind of program property.
        Exrensional semantics are typically appropriate for proving 
        properties such as partial correctness, but an intensional 
        semantics at a lower abstraction level is required aspects of 
        behavior such as order of evaluation and efficiency.
        It is obviously desirable to be able to establish sensible 
        relationships between two semantics for the same language, and 
        we seek a general category-theoretic framework that permits 
        this.
        
        Beginning with an "extensional" category, whose morphisms we can
        think of as functions of some kind, we model a notion of 
        computation as a comonad with certain extra structure and we 
        regard the Kleisli category.
        An intensional morphism, or algorithm, can be thought of as a 
        function from computations to values.
        This view accords with a lazy operational interpretation of 
        programs.
        Under certain rather general assumptions the underlying category
        can be thought of as a function from computations to vallues.
        This view accords with lazy operational interpretation of 
        programs.
        Under certain rather general assumptions the underlying category
        is cartesian closed.
        Under further assumptions the Kleisli category satisfies a weak
        from of cartesian closure: application morphisms exist, currying
        and uncurrying of morphisms make sense, and the diagram for 
        exponentiation commutes up to extensional equivalence.
        When the underlying category is an ordered category we identifys
        condition under which the exponentiation diagram commutes up to
        an inequality.
        We illustrate these ideas and results by introducing some 
        notions of computation on domains and by discussing the 
        properties of he corresponding categories of algorithms on 
        domains.
Number: CMU-CS-91-190
Bibtype: TechReport
Month: oct
Author: Stephen Brookes
        Shai Geva
Title: Computational Comonads and Intensional Semantics
Year: 1991
Address: Pittsburgh, PA
Super: @CMUTR