reductions to HaltLclosed and L_computable_closed without the L framework
#226
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…rk / MetaCoq added MMA_computable to L_computable_closed without the L framework / MetaCoq added MM_computable_to_MMA_computable made HaltLclosed more prominent in reduction chains generalized deterministic simulation to uniformly confluent simulation
yforster
approved these changes
Oct 1, 2024
There was a problem hiding this comment.
I have no strong opinion, but I'm also not opposed, this indeed probably makes long-term maintainability easier. I'd not like to drop the reduction relying on the framework completely from the code to keep the framework alive (but if I'm not missing something this PR is not deleting the reduction anyway, it's just making sure the main loop does not rely on the framework)
Yes, this PR just adds different options and does not delete reductions. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
MMA_HALTINGtoHaltLclosedwithout theLframeworkMMA_computabletoL_computable_closedwithout theLframeworkMM_computabletoMMA_computablereduction to close the loopHaltLclosedmore prominent in reduction chainsLreductions)Now we have no
_undecresults which depend on theLframework / MetaCoq.The only computability result which depends on the
Lframework / MetaCoq isMuRec_computable_to_L_computable.