Nondeterministic multi-stack machine

Stream: general

[Martin Dvořák]

I want to define Nondeterministic multi-stack machines, as an auxiliary model for Computability theory. I think I should build them in a way that will allow to include them in mathlib (even if the theory build on top of them doesn't end up in mathlib).

I am not sure it is a good idea. If I understand correctly TM2 is a multi-stack machine that computes an output (as opposed to accept/reject the input). This isn't the framework in which nondeterminism is typically considered.

I end up with a decision paralysis because there are many options what model of computation I may use. Unfortunately, none of them looks easy to implement and none of them seems to be clearly superior to other options.

[Wojciech Nawrocki]

@Martin Dvořák there are people here better equipped than me to talk about models of computation specifically, but as far as choosing definitions at the beginning of the formalization of an area of study, as far as I can tell the only workable approach is the experimental approach of building up the beginnings of a theory starting from a couple of different definitions and then choosing the one that seems to work best, perhaps adjusting later in an iterative manner based on some new intuitions.