"classical" computability theory and the category of Sets

"classical" computability theory and the category of Sets

[Vasili I. Galchin]

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

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

[Michael Barr]

A student of mine, James R. Otto worked on this for his thesis.
Unfortunately, it was famously unreadable.  I don't think it was published
and I have lost contact with him.  It was in the early 90s.

Michael

On Wed, 2 Jul 2014, Vasili I. Galchin 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
>
>

-- 
         Every gun that is made, every warship launched, every rocket fired
signifies, in the final sense, a theft from those who hunger and are not
fed, those who are cold and are not clothed. -Dwight D. Eisenhower



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

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

[Hiroyuki Miyoshi]

Hi, Michael and Vasya

I remember Jim Otto and his thesis.
It is downloadable from this page:

http://digitool.library.mcgill.ca/R/?func=dbin-jump-full&object_id=29104&local_base=GEN01-MCG02

Hiroyuki Miyoshi


2014-07-04 22:20 GMT+09:00 Michael Barr <barr@math.mcgill.ca>:
> A student of mine, James R. Otto worked on this for his thesis.
> Unfortunately, it was famously unreadable.  I don't think it was published
> and I have lost contact with him.  It was in the early 90s.
>
> Michael
>
> On Wed, 2 Jul 2014, Vasili I. Galchin wrote:
>

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

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

[Michael Barr]

I did finally get it, but only by downloading it and renaming it complexity.pdf (from complexity with no suffix).  It is clearly scanned in rather than an original pdf file.  It is readable, but relatively poor quality.  I suppose this form of publication has superceded University Microfilms (which produced much poorer quality, in part because the originals were just typed).

I had no idea McGill was doing this.  You live and learn.

Thanks, Michael

----- Original Message -----
From: "Hiroyuki Miyoshi" <hxm@cc.kyoto-su.ac.jp>
To: "Michael Barr" <barr@math.mcgill.ca>
Cc: "Vasili I. Galchin" <vigalchin@gmail.com>, "Categories mailing list" <categories@mta.ca>
Sent: Sunday, July 6, 2014 1:00:29 AM
Subject: Re: categories: Re: "classical" computability theory and the category of Sets

Hi, Michael and Vasya

I remember Jim Otto and his thesis.
It is downloadable from this page:

http://digitool.library.mcgill.ca/R/?func=dbin-jump-full&object_id=29104&local_base=GEN01-MCG02

Hiroyuki Miyoshi



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

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

[Rich Hilliard]

CiteSeer appears to have slightly better quality (not scanned) ps and pdf (=
probably generated from the ps) versions linked from this page:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=3D10.1.1.45.6517

  -- Rich

On Jul 6, 2014, at 8:45 AM, Michael Barr wrote:

> I did finally get it, but only by downloading it and renaming it complexi=
ty.pdf (from complexity with no suffix).  It is clearly scanned in rather t=
han an original pdf file.  It is readable, but relatively poor quality.  I =
suppose this form of publication has superceded University Microfilms (whic=
h produced much poorer quality, in part because the originals were just typ=
ed).
>=20
> I had no idea McGill was doing this.  You live and learn.
>=20
> Thanks, Michael
>=20
> ----- Original Message -----
> From: "Hiroyuki Miyoshi" <hxm@cc.kyoto-su.ac.jp>
> To: "Michael Barr" <barr@math.mcgill.ca>
> Cc: "Vasili I. Galchin" <vigalchin@gmail.com>, "Categories mailing list" =
<categories@mta.ca>
> Sent: Sunday, July 6, 2014 1:00:29 AM
> Subject: Re: categories: Re: "classical" computability theory and the cat=
egory of Sets
>=20
> Hi, Michael and Vasya
>=20
> I remember Jim Otto and his thesis.
> It is downloadable from this page:
>=20
> http://digitool.library.mcgill.ca/R/?func=3Ddbin-jump-full&object_id=3D29=
104&local_base=3DGEN01-MCG02
>=20
> Hiroyuki Miyoshi
>=20

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

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

[Robin Cockett]

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