Re: "classical" computability theory and the category of Sets

[Robin Cockett <robin@ucalgary.ca>]

A slightly different take on computability is given by Pieter Hofstra and I
in "Introduction to Turing Categories" (APAL 156, issue 2-3, 2010,
183-209). This described a continuation of the program of doing "recursion
theory without elements" initiated by Alex Heller and Robert Di Paola --
which we refer to more prosaically as abstract computability.  We extended
the original ideas to not only cover the standard setting of recursion
theory but also, for example, the total models (from the lambda calculus).

Essentially a Turing category can be characterized as the computable
functions of a pca living somewhere. As the pca need not live in sets the
total functions of a Turing category can be considerably less than all the
computable functions (of course they could also include much more).
  Significantly the total functions can be any "functional complexity
class".  Thus, there are Turing categories whose total functions are
precisely the PTIME functions (and similarly for the LOGSPACE functions
etc.).  These examples are the basis for claiming that abstract
computability might be useful in unifying  computability and complexity.

The basis for the statement that there are Turing categories with these
properties is spelled out in "Timed  sets, functional complexity, and
computability" (ENTCS 286, 2012 pages 117-137).  This year in MFPS Pieter
Hofstra (with Pavel Hrubes and I) continued this work and described
abstractly exactly which categories can be the total maps of a Turing
category.

-robin
(Robin Cockett)






On Wed, Jul 2, 2014 at 11:55 AM, Vasili I. Galchin <vigalchin@gmail.com>
wrote:

> Hello Cat Theory list,
>
>      Please be gentle.
>
>      In the past I studied computability theory. It seems to me that
> this theory  is built on the category of Sets(elementary topos), i.e.
> this computability theory assumes using classical logic with LEM and
> boolean subobject classifier for concepts like semi-decidability, etc.
> Is there a notion of intuitionistic computability theory built on
> other topoi where LEM is absent from the accompanying higher logic and
> the topos' subobject classifier has a internal Heyting algebra(that is
> not boolean)?? Is this what realizibility delves into(I have yet to
> study realizibility concepts).
>
> Kind regards,
>
> Vasya
>

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]