Evaluation of source code, category theoretically?
What's the right way to think about evaluation in category theory? I'm guessing it will look kind of like this: the category will be symmetric monoidal closed and equipped with an object S whose points are "source code", together with a collection of interpreter epimorphisms run_{X, Y}: S -> [X, Y] and some notion of composition in S that works well with composition of morphisms. What are the right keywords for doing a literature search on this? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Mike, You might consider the literature on normalization by evaluation<https://www.google.com/search?q=normalization+by+evaluation&oq=normalization+by+evaluation&aqs=chrome..69i57j0l5.6625j0j7&sourceid=chrome&espv=210&es_sm=119&ie=UTF-8> . Best wishes, --greg On Thu, Jan 2, 2014 at 10:05 AM, Mike Stay <metaweta@gmail.com> wrote:
What's the right way to think about evaluation in category theory? I'm guessing it will look kind of like this: the category will be symmetric monoidal closed and equipped with an object S whose points are "source code", together with a collection of interpreter epimorphisms run_{X, Y}: S -> [X, Y] and some notion of composition in S that works well with composition of morphisms.
What are the right keywords for doing a literature search on this? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
I am sure there are many "right ways" to think about evaluation in categories .... One significant line of development, which one might call "abstract computability" was initiated by Di Paola and Heller's paper "Dominical Categories: recursion theory without elements". The key notion was of a Turing object which lived in a category of partial maps. The Turing object was universal in the sense that every object in the category was a retract of it and had a (weak) notion of "evaluation" on itself (and thus on every object). These ideas were followed up in various ways. One direction involved simply getting a better understanding of partial map categories (e.g. "P-categories" Rossolini and Robinson,"Partiality, Cartesian Closedness, and toposes" Curien and Obtulowitz, "Restriction Categories" Steve Lack and myself, ...). Another direction concerned better understanding the evaluation. In "Introduction to Turing Categories" Pieter Hofstra and I updated Di Paola and Heller's ideas, introduced the unifying idea of a Turing category, and also described the link to partial combinatory algebras (PCAs). The literature on PCAs (especially if you include the total variants: combinatory algebras) is extensive. Turing categories are the cleanest formulation so far for abstract computability. Interestingly they also are a setting in which one can study complexity: thus, there are Turing categories in which the only total maps are the P-time maps (e.g. see "Timed sets, Functional Complexity, and Computability" Gallagher, Boils, Hrubes, and I). -robin On Thu, Jan 2, 2014 at 11:05 AM, Mike Stay <metaweta@gmail.com> wrote:
What's the right way to think about evaluation in category theory? I'm guessing it will look kind of like this: the category will be symmetric monoidal closed and equipped with an object S whose points are "source code", together with a collection of interpreter epimorphisms run_{X, Y}: S -> [X, Y] and some notion of composition in S that works well with composition of morphisms.
What are the right keywords for doing a literature search on this? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
i am hoping that you might also like monoidal computer http://arxiv.org/abs/1208.5205 it's similar to robin's turing categories, but also quite different. it's all in string diagrams. there is also a complexity theory paper, with a much better string diagram language, which i still didn't upload on arxiv, but will do soon. comments welcome and appreciated. -- dusko On Jan 2, 2014, at 8:05 AM, Mike Stay <metaweta@gmail.com> wrote:
What's the right way to think about evaluation in category theory? I'm guessing it will look kind of like this: the category will be symmetric monoidal closed and equipped with an object S whose points are "source code", together with a collection of interpreter epimorphisms run_{X, Y}: S -> [X, Y] and some notion of composition in S that works well with composition of morphisms.
What are the right keywords for doing a literature search on this? -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (4)
-
dusko pavlovic -
Greg Meredith -
Mike Stay -
Robin Cockett