More Like this

1. Testing a unified model of arithmetic

   Braithwaite, David W.; Siegler, Robert S. (January 2022, Proceedings of the 44th Annual Conference of the Cognitive Science Society)

   Culbertson, J.; Perfors, A.; Rabagliati, H.; Ramenzoni, V. (Ed.)

   We describe UMA (Unified Model of Arithmetic), a theory of children’s arithmetic implemented as a computational model. UMA extends a theory of fraction arithmetic (Braithwaite et al., 2017) to include arithmetic with whole numbers and decimals. We evaluated UMA in the domain of decimal arithmetic by training the model on problems from a math textbook series, then testing it on decimal arithmetic problems that were solved by 6th and 8th graders in a previous study. UMA’s test performance closely matched that of children, supporting three assumptions of the theory: (1) most errors reflect small deviations from standard procedures, (2) between-problem variations in error rates reflect the distribution of input that learners receive, and (3) individual differences in strategy use reflect underlying variation in learning parameters. 

   more » « less
2. Affordances of Fractions and Decimals for Arithmetic

   Braithwaite, David W.; Liu, Qiushan (January 2022, Journal of experimental psychology)

   Rational numbers are represented by multiple notations: fractions, decimals, and percentages. Whereas previous studies have investigated affordances of these notations for representing different types of information (DeWolf, Bassok, & Holyoak, 2015; Tian, Braithwaite, & Siegler, 2020), the present study investigated their affordances for solving different types of arithmetic problems. We hypothesized that decimals afford addition better than fractions do and that fractions afford multiplication better than decimals do. This hypothesis was tested in two experiments with university students (Ns = 77 and 80). When solving fraction and decimal arithmetic problems, participants converted addition problems from fraction to decimal form more than vice versa, and converted multiplication problems from decimal to fraction form more than vice versa, thus revealing preferences favoring decimals for addition and fractions for multiplication. Accuracies paralleled these revealed preferences: Addition accuracy was higher with decimals than fractions, whereas multiplication accuracy was higher with fractions than decimals. Variations in notation preferences as a function of the types of operands involved (e.g., equal versus unequal denominator fractions) were more consistent with an explanation based on adaptive strategy choice (Siegler, 1996) than with one based on semantic interpretations associated with each notation. 

   more » « less
3. UltraPrecise: A GPU-Based Framework for Arbitrary-Precision Arithmetic in Database Systems

   https://doi.org/10.1109/ICDE60146.2024.00294  

   Li, Xin; Xiao, Mengbai; Yu, Dongxiao; Lee, Rubao; Zhang, Xiaodong (May 2024, IEEE)

   Fixed-point decimal operations in databases with arbitrary-precision arithmetic refer to the ability to store and operate decimal fraction numbers with an arbitrary length of digits. This type of operation has become a requirement for many applications, including scientific databases, financial data processing, geometric data processing, and cryptography. However, the state-of-the-art fixed-point decimal technology either provides high performance for low-precision operations or supports arbitrary-precision arithmetic operations at low performance. In this paper, we present a design and implementation of a framework called UltraPrecise which supports arbitraryprecision arithmetic for databases on GPU, aiming to gain high performance for arbitrary-precision arithmetic operations. We build our framework based on the just-in-time compilation technique and optimize its performance via data representation design, PTX acceleration, and expression scheduling. UltraPrecise achieves comparable performance to other high-performance databases for low-precision arithmetic operations. For highprecision, we show that UltraPrecise consistently outperforms existing databases by two orders of magnitude, including workloads of RSA encryption and trigonometric function approximation. 

   more » « less
4. A Decidable Logic for Tree Data-Structures with Measurements

   https://doi.org/10.1007/978-3-030-11245-5_15  

   Qiu, Xiaokang; Wang, Yanjun (January 2019, 20th International Conference on Verification, Model Checking, and Abstract Interpretation)

   We present DRYADdec, a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on Max or Sum, and recursive predicates based on these measure functions, such as AVL trees or red-black trees. We prove that the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of DRYADdec to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that DRYADdec can encode a variety of verification and synthesis problems, including natural proof verification conditions for functional correctness of recursive tree-manipulating programs, legality conditions for fusing tree traversals, synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 220+ DRYADdec formulae raised from these application scenarios, including verifying functional correctness of programs manipulating AVL trees, red-black trees and treaps, checking the fusibility of height-based mutually recursive tree traversals, and counterexample-guided synthesis from linear integer arithmetic specifications. To our knowledge, DRYADdec is the first decidable logic that can solve such a wide variety of problems requiring flexible combination of measure-related, data-related and shape-related properties for trees. 

   more » « less
5. When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic

   https://doi.org/10.1145/3571237  

   Kincaid, Zachary; Koh, Nicolas; Zhu, Shaowei (January 2023, Proceedings of the ACM on Programming Languages)

   This paper presents a theory of non-linear integer/real arithmetic and algorithms for reasoning about this theory. The theory can be conceived of as an extension of linear integer/real arithmetic with a weakly-axiomatized multiplication symbol, which retains many of the desirable algorithmic properties of linear arithmetic. In particular, we show that the conjunctive fragment of the theory can be effectively manipulated (analogously to the usual operations on convex polyhedra, the conjunctive fragment of linear arithmetic). As a result, we can solve the following consequence-finding problem: given a ground formula F , find the strongest conjunctive formula that is entailed by F . As an application of consequence-finding, we give a loop invariant generation algorithm that is monotone with respect to the theory and (in a sense) complete. Experiments show that the invariants generated from the consequences are effective for proving safety properties of programs that require non-linear reasoning. 

   more » « less