Homomorphism Calculus for User-Defined Aggregations
summary
Introduces a decidable homomorphism calculus and a synthesis tool Inc that reduces dataframe homomorphism verification to a local per-row check via a normalizer and uses type-directed decomposition plus proof rules to refute impossible cases. Implementation synthesizes merge operators for 43 of 45 homomorphic UDAFs in a 50-benchmark corpus, successfully refutes all 5 non-homomorphic tasks, finds many developer bugs (e.g., several hand-written merges are incorrect), and outperforms prior synthesizers.
AI-written summary · about
chapters (10)
- 0:00Homomorphism calculus intro
- 1:03User-defined aggregations
- 3:53Merge function correctness
- 6:42Goal of homomorphism calculus
- 7:25Verifying merge functions
- 9:55Local verification method
- 11:19Refuting non-homomorphic UDAFs
- 12:23Type-directed decomposition
- 14:30Inc evaluation
- 16:17Questions and answers session
related talks
46mIsomer
56mEfficient array (and data) processing by leveraging structure
41mIntroducing Cascalog: Functional Data Processing for Hadoop
21mDataEngBytes 2023 - SYD-T3-04 - Abhinav Goyal
14mMaking Data Quality an integral part of developing Machine Learning and Data Products
47mKeeping the fun in Apache Spark Datasets and FP
45mBidirectional Data Transformations
39mEventually Consistent Data Structures