feat: query model for single tape TM#416
feat: query model for single tape TM#416Shreyas4991 wants to merge 38 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.
you should base this onto your #372 branch instead of main so that the diff shows what you've added since then |
yes but specifically on GitHub on this PR you should also set the base branch, since currently it is showing the diff compared to main. click the pencil icon next to the title of the PR, then click the dropdown menu where it says |
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