Start general definitions for computation models#550
Conversation
|
THe corresponding topic on zulip is #CSLib > Typeclasses for computation models |
Thank you to Christian Reitwiessner for suggestions https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Typeclasses.20for.20computation.20models/near/593283668
| step {a : τ} : cfg a → Option (cfg a) | ||
|
|
||
| /-- An abstract version of a turing machine with input alphabet `Γ₀` and output alphabet `Γ₁`. -/ | ||
| class Transducer (τ : Type*) (Γᵢₙ Γₒᵤₜ : Type) extends TransitionSystem τ where |
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Yes, that is true, and I changed it accordingly
kesslermaximilian
changed the title
kesslermaximilian
changed the title
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
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.
| -/ | ||
| class TransitionSystem (τ : Type u) where | ||
| cfg (t : τ) : Type* | ||
| step {t : τ} : cfg t → Option (cfg t) |
There was a problem hiding this comment.
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?
3 participants
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.