-
Notifications
You must be signed in to change notification settings - Fork 0
Reduce #1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Reduce #1
Conversation
- 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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
💡 Codex Review
Here are some automated review suggestions for this pull request.
i️ 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".
Uh oh!
There was an error while loading. Please reload this page.
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.