Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422351 | Electronic Notes in Theoretical Computer Science | 2014 | 10 Pages |
Abstract
Lawvere theories provide a categorical formulation of the algebraic theories from universal algebra. Freyd categories are categorical models of first-order effectful programming languages.The notion of sound limit doctrine has been used to classify accessible categories. We provide a definition of Lawvere theory that is enriched in a closed category that is locally presentable with respect to a sound limit doctrine.For the doctrine of finite limits, we recover Power's enriched Lawvere theories. For the empty limit doctrine, our Lawvere theories are Freyd categories, and for the doctrine of finite products, our Lawvere theories are distributive Freyd categories. In this sense, computational effects are algebraic.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics