Timeline for Defining computable functions categorically
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 17, 2018 at 20:07 | answer | added | François G. Dorais | timeline score: 10 | |
| May 16, 2018 at 16:43 | answer | added | Andrej Bauer | timeline score: 18 | |
| May 16, 2018 at 13:30 | answer | added | Peter Gerdes | timeline score: 2 | |
| Feb 28, 2018 at 14:33 | comment | added | Joel David Hamkins | Oh, I had understood the question to be specifically about the category that was mentioned there. Obviously one can capture the notion of computability with a richer category. | |
| Feb 28, 2018 at 7:03 | comment | added | N. Virgo | @DmitriPavlov great, fantastic! I don't yet have the background to understand that page, but I'm happy to know what I should be aiming for. (Answers are welcome that gently outline how this approach works, in the context of my question. I'll look into it in my own time also of course.) | |
| Feb 28, 2018 at 6:23 | comment | added | Dmitri Pavlov | This is formalized in the notion of a realizability topos, and Frey's theorem characterizes such toposes axiomatically. See ncatlab.org/nlab/show/realizability%20topos | |
| Feb 28, 2018 at 2:53 | comment | added | Joel David Hamkins | I like this question a lot. I wonder one can answer it by showing that pointwise evaluation of the functions can be defined in the monoid structure, with finitely many parameters (for the zero functions, succssor and perhaps a few others, such as the pairing function projections). From this, it would follow that in any isomorphic copy of that category, one can "compute" the function by translating through the isomorphism. This would show a sense in which that category captures computability. I am a little worried, however, about the fact that your category has only unary composition. | |
| Feb 28, 2018 at 0:41 | history | asked | N. Virgo | CC BY-SA 3.0 |