Reduce #1
Open
Reduce #1
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
- Move 'Partial Reducers' remark to after Theorem 4 (was prematurely placed) - Add proper definition of algebraic aggregates in Section 3.2 - Remove incoherent 'partial average reducer' paragraph - you cannot maintain average incrementally with only the average value (need count too) - Clarify min reducer as canonical example of non-invertible aggregate - Explain Skip's strategies for handling partial reducers
…ssumptions" This reverts commit a72cc21.
- Rewrite abstract to emphasize first-class combinators vs callbacks - Contrast with Flink, Kafka Streams, FRP, and incremental computation frameworks - Add 'What distinguishes Skip's design' paragraph with 3 key differentiators - Qualify claims about formal correctness to acknowledge DBSP/differential dataflow foundations - Add 'Reactive JS and FRP streams' paragraph to related work
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
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.
Summary
This PR adds a formal semantics for Skip's reactive
reducecombinator, including a paper and a Lean formalization.What's Included
reduce.tex): Formal semantics for Skip'sreducecombinator with correctness proofslean-formalisation/): Machine-checked proofs of the main theoremsKey Contributions
reduceas a derived view over collections⊖is the inverse of⊕)Main Results
(fold_⊕(ι, M) ⊕ v) ⊖ v = fold_⊕(ι, M)for all reachable accumulator statesWhat Distinguishes This Work
Unlike related systems (Flink, Kafka Streams, FRP frameworks), Skip exposes reducers as:
⊖operation, not hidden internally)The Lean formalization provides machine-checked verification of the main correctness theorem and supporting lemmas.