Spec: Performant Ordering Variable Numbering #334
Draft
Conversation
This file contains hidden or 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
This spec proposes migrating Strata's variable representation to Performant Ordering - a unified variable numbering scheme using globally unique natural numbers. Key changes: - All variables (lambda-bound and imperative) use unique Nat identifiers - Eliminates De Bruijn index shifting, weakening, and lifting - Replaces old() construct with dual identifiers in modifies clauses - Introduces NextFree structure to track fresh variable generation - Leverages existing HasVars typeclass infrastructure Files: - requirements.md: 13 requirements with acceptance criteria - design.md: Complete technical design and architecture - tasks.md: Detailed implementation plan across 6 phases
The content is already split into requirements.md, design.md, and tasks.md
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Overview
Specification for migrating Strata to Performant Ordering - a unified variable numbering scheme using globally unique natural numbers.
Problem
Current state: Mixed variable representations
old()as operator enables proving false (Soundness issue: old as operator. #257)Proposed
All variables use unique
Natidentifiers from a global counter.Benefits:
Key Changes
old()operator with dual identifiers in modifies clausesNextFreestructure tracks fresh variable counter with well-formedness invariantsHasVarstypeclass infrastructureSeeking Feedback
Specification for review (no implementation). Feedback wanted on approach, integration strategy, and migration phasing.