Start general definitions for computation models

[kesslermaximilian]

This is a draft so far and should accompany the discussion on zulip.
If we think this design pattern is useful and should be part of cslib, I'll extend these definitiions and also add appropriate documentation etc.

[kesslermaximilian]

THe corresponding topic on zulip is #CSLib > Typeclasses for computation models

[crei]

At least on github web, Γₒᵤₜ renders super weirdly (at least in the monospace font). So I take my suggestion from zulip back a bit. Maybe Γᵢ and Γₒ ? Please also update the comment above.

[kesslermaximilian]

Yes, that is true, and I changed it accordingly

[ctchou]

In general, I find it difficult to review basic definitions like these in isolation. We need to see them "in action" before we can judge their quality. I would recommend that they be used to at least express some nontrivial results before we accept them.

[ctchou]

First, I don't understand why you need the cfg field. What's wrong with dropping cfg and replacing every cfg t by τ? In general, it's more hassle dealing with a family of types than just a single type.

Second, there is already a theory of partial function is mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFun.html
Any reason you want to develop your own theory of partial functions?

[kesslermaximilian]

The idea is to think of τ as, for example, "the type of single tape turing machines". Then cfg t is the "type of configurations of the specific turing machine t, which is (potentially) different for any specific one-tape turing machine, since they can have different state types. So with cfg` I wanted to capture that the "computation context / configuration" is actually dependent on the machine / system you started with.

Regarding the theory of partial functions: I don't really want to work with PFun, because what we're dealing here is a special case of it, namely that we have a well-defined domain (where we return some values). For me, this seemed easier to work with than PFun.

[ctchou]

The distinction between t and cfg t is irrelevant to the theory you are developing here. So far as I can tell, you can define and prove all you have here by using step : T → Option T. As a concrete example, take a look at how I use LTS to model the transition relation of a distributed algorithm:
https://github.com/ctchou/cslib/blob/flp-work/Cslib/Computability/Distributed/FLP/Algorithm.lean
where for each distributed algorithm a, I define an LTS a.LTS representing the transition relation of a. I'm sure you can do the same for Turing machines.

For that matter, a partial transition function is equivalent to a deterministic LTS:
https://api.cslib.io/docs/Cslib/Foundations/Semantics/LTS/Basic.html#Cslib.LTS.Deterministic
in which the label type is a singleton. What you define and prove here can be defined and proved in terms of deterministic LTS. For example, EvalsToInTime t a b n can be stated as something like t.LTS.MTr a xs b ∧ xs.length ≤ n, where t.LTS is the LTS representing the transition relation of the Turing machine t and a and b are configurations of t. Note that we don't need to "lift" a and b to their Option-ed versions. (Indeed, by using relational statements, I think we suspect Option only rarely.) For another example, the theorem EvalsToInTime.trans is an easy consequence of LTS.MTr.comp:
https://api.cslib.io/docs/Cslib/Foundations/Semantics/LTS/Basic.html#Cslib.LTS.MTr.comp
The theorem OutputsInTime.output_unique doesn't have a counterpart in LTS yet, but that's only because not many theorems have been proved about deterministic LTS, which can be easily remedied.

[kesslermaximilian]

In general, I find it difficult to review basic definitions like these in isolation. We need to see them "in action" before we can judge their quality. I would recommend that they be used to at least express some nontrivial results before we accept them.

Yes, that is very fair. These definitions stem from a previous project of mine (which was based on mathlib and I'm trying to adapt to CSLib while reworking / polishing), and you can find it here: https://git.abstractnonsen.se/max/mathlib4

In particular, examples of the code in action are the instances in this file here: https://git.abstractnonsen.se/max/mathlib4/src/commit/0f4c50edbe7ac8b5f92fee9f514b4385446c4bd6/Mathlib/Computability/TM0Computable.lean#L82-L86, https://git.abstractnonsen.se/max/mathlib4/src/commit/0f4c50edbe7ac8b5f92fee9f514b4385446c4bd6/Mathlib/Computability/TM0Computable.lean#L164-L168, which describe how different (pre-existing) variants of turing machines can be viewed as these typeclasses.
This allows to state things like https://git.abstractnonsen.se/max/mathlib4/src/commit/0f4c50edbe7ac8b5f92fee9f514b4385446c4bd6/Mathlib/Computability/TM0Computable.lean#L294-L297 (that the two turing models are equivalent up to polynomial time factors), and use it for things like stating the definition of P (https://git.abstractnonsen.se/max/mathlib4/src/commit/0f4c50edbe7ac8b5f92fee9f514b4385446c4bd6/Mathlib/Computability/NP.lean#L166-L167) and deducing that it is independent of the specific turing model because of the equivalence: https://git.abstractnonsen.se/max/mathlib4/src/commit/0f4c50edbe7ac8b5f92fee9f514b4385446c4bd6/Mathlib/Computability/NP.lean#L228-L230

I will try to port more of my code in the near future and also demonstrate how I would envision these definitions being used in CSLib.