Problems in Rewriting Applied to Categorical Concepts by the Example of a Computational Comonad.

Abstract

We present a canonical system for comonads which can be extended to the notion of a computational comonad (BG91) where the crucial point is to find an appropriate representation. These canonical systems are checked with the help of the Larch Prover (GG91) exploiting a method by G. Huet (Hue90a) to represent typing within an untyped rewriting system. The resulting decision procedures are implemented in the programming language Elf Pfe89j since typing is directly supported by this language. Finally we outline an incomplete attempt to solve the problem which could be used as a benchmark for rewriting tools.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1994
Accession Number
ADA288582

Entities

People

  • Wolfgang Gehrke

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Calculus
  • Civil Rights
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Equations
  • Identities
  • Language
  • Law
  • Mathematics
  • Polynomials
  • Programming Languages
  • Semantics
  • Specifications
  • Translations
  • Universities

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Operations Research