feat(Computability): Abstract machine model.

[crei]

This is a proposal to define machine models in a much more abstract way that proposed until now.

It is not meant to replace #550 but instead to build on top of it. The reason I started this is because I am working on a machine model that is not based on a transition system and thus the definitions in #550 do not apply.

Main features of this PR:

It allows each machine type to define its own input/output data type and requires just a generic "run" function that returns the output, the number of time steps used and the space consumed (as a Part value).

Furthermore, it defines a MachineEncodable class that allows to define machine-type-specific encodings of lean types. When defining a new computation model, it could be very counter-productive to use a globally defined way to encode e.g. a list or a tuple.

To tie two machine models with differing encodings together again, it defines LinearlySpaceRelated and PolynomiallyTimeRelated - two properties that essentially say that two machine models capture the same kind of complexity.

To illustrate how this can be used, I implemented the classes for SigleTapeTM and for LambdaCalculus. I think it should be useful to prove in which way they are related as computational mechanisms and probably also add more models. Furthermore, via LinearlySpaceRelated and PolynomiallyTimeRelated, we can mix at match computational models when proving generic results in complexity theory.

Note that because this model allows each computational model to specify its own input/output type, lambda calculus does not need to encode and decode terms but instead can be directly applied.

Finally, it is very convenient to specify things like

RAMMachineModel.ComputableInOTime Nat.sqrt (fun n => n^2)
TuringMachineModel.ComputabelInOTime (fun m a b : Matrix (Fin m) (Fin m) Nat => a * b) (fun n => n^3)

and of course such function can then be composed, regardless of the model, as long as they are related.

[crei]

Even if a machine model is only linearly space related for space bounds starting from linear to e.g. the multi-tape Turing machine model with read-only input tape, then using the idea outlined in this zulip thread, it can be automatically extended to make it fully linearly space related.

Furthermore, we can define nondeterministic space, alternating time and space, randomization, oracles and other concepts on top of the machine model defined here (i.e. on top of any machine model that fits this class) without having to "open it up" and modify it to explain what we mean by "oracles" or "alteration".

[ctchou]

Just wondering if you have been following the discussion here:
#CSLib > Typeclasses for computation models

[crei]

Just wondering if you have been following the discussion here: #CSLib > Typeclasses for computation models

Yes, that's why I linked to #550. I will add something to the thread.