feat: query model for single tape TM#416
feat: query model for single tape TM#416Shreyas4991 wants to merge 39 commits intoleanprover:mainfrom
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…o query-final-squash
Co-authored-by: Shreyas Srinivas <Shreyas4991@users.noreply.github.com> Co-authored-by: Eric Wieser <eric-wieser@users.noreply.github.com> Co-authored-by: Tanner Duve <tannerduve@gmail.com>
|
Things todo:
|
| /-- `writeCells` is a set of cells that were previously unwritten -/ | ||
| writeCells : ℕ |
There was a problem hiding this comment.
Based on the type, it's not a set of cells. Based on the definition below it appears to be more like the maximum amount of cells without counting the input length
There was a problem hiding this comment.
Correct. As discussed in the Zulip thread, the current TM formulation doesn't have a notion of tape indices. So I am trying to short circuit the process by only counting non-input cells. Of course this also ends up counting output cells of the tape. This is what I hope will be different in a multi tape setting, with distinct work tapes.
There was a problem hiding this comment.
Yes, so the docstring should reflect that.
There was a problem hiding this comment.
Thanks. Will do. Fwiw any design suggestions are welcome. The PR is still a WIP.
There was a problem hiding this comment.
It is still referred to as a set while being a natural number after your recent update.
There was a problem hiding this comment.
Apologies. I'll change it asap.
you should base this onto your #372 branch instead of main so that the diff shows what you've added since then |
4 participants
Draft PR to explore the design of a monadic language for single tape TMs. Multi tape TMs will be similar.
Depends on #372