What is the correct reply to a mathematician, who has never formalized anything, asking how they would go about formalizing a research paper of theirs?
@MartinEscardo@andrejbauer It's the study of algorithms for computing things about points, lines, polyhedra, etc. in three-dimensional space, usually Euclidean. The sort of thing one generally wants to prove is "this algorithm always produces the correct solution to this problem in a number of elementary steps that has this asymptotic bound". The model of computation needs to be carefully specified but often it is relatively clean (a decision tree in which each branch is chosen according to the sign of a low-degree polynomial of input coefficients).
@MartinEscardo@andrejbauer Yes, I'm less worried about the asymptotics than about formalizing what an algorithm is, how to say something about what its time complexity is, and how to say something about what it computes, for a problem domain where some models of computing used widely elsewhere (like Turing machines) don't match standard assumptions that the inputs are specified by real numbers, and at a high enough level of abstraction to make it possible to describe complicated algorithms and not just low-level sequences of operations.
@11011110@MartinEscardo@andrejbauer This is something some of us have been thinking about. We organized a reading group this semester on some potentially relevant background material.
Even for more "discrete" domains like graph algorithms, one would like to prove things about their complexity, and formalizing that complexity ultimately ends up related to some "base" computational model that needs to be polynomially related to TMs.
Formalizing TMs is a huge pain, but I don't yet know how to get around it. It'd be nice to have a "synthetic" theory of computation... I'm currently thinking to revisit some of Gurevich's writings about "what is an algorithm" in thinking about this. Would be very happy to chat about it at some point.
@joshuagrochow@11011110@MartinEscardo@andrejbauer - for better models of computation, it might be worth looking at Pavlovic's papers on the monoidal computer, and also Yanofsky's book Theoretical Computer Science for the Working Category Theorist.
My experience so far has been that while categorical approaches to computation are nice in a similar way to functional programming being nice, they can be difficult to work with when one wants to do more advanced stuff with computational complexity. Maybe I just don't have enough experience working with them though...I guess we'll see.
@joshuagrochow@11011110@MartinEscardo@andrejbauer - they could be difficult to work with, but at least Yanofsky sets up and studies categories corresponding to various complexity classes; it's a start.
Because formalizing Turing Machines is, indeed, a "huge pain", as you say, back in 2017, my former student Cory Knapp and I came up with "Abstract Turing Machines" to ease the pain.
@MartinEscardo@11011110@andrejbauer Ooh, this makes me really glad I said something here (which I was initially wavering on). I was not aware of this work, and it looks very interesting. I will definitely check it out, thanks!
@joshuagrochow@MartinEscardo@11011110 You should also pay attention to the work of @yforster and the gang. Yannick's thesis is a good start, and now that he's been pinged, perhaps he can tell us whether they've thought about complexity in addition to computability.
@andrejbauer@MartinEscardo@11011110@yforster Yes, that's one line of research we've already been reading. Didn't realize he was on here though, thanks.
Add comment