- 著者
- Stephen Brookes, Shai Geva
- タイトル
- Computational Comonads and Intensional Semantics
- 日時
- October 1991
- 概要
- 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.
- カテゴリ
- CMUTR

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