Evaluation of source code, category theoretically?

Evaluation of source code, category theoretically?

[Mike Stay]

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/ ]

Re: Evaluation of source code, category theoretically?

[dusko pavlovic]

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/ ]

Re: Evaluation of source code, category theoretically?

[Mike Stay]

Thanks, all for your responses so far; many of you have asked what my
motivation was for the question.  I'm trying to understand pi
calculus.  I've got a bicategorical model of a fragment of pi calculus
where prefixing is composition, but in order to prevent reduction
under a prefix, the remainder of the term needs to be suspended; one
way to do that is to treat it as "source code" and evaluate it in an
environment with bindings, thus my question.

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/ ]

Re: Evaluation of source code, category theoretically?

[Greg Meredith]

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/ ]