When does 0–1 Principle Hold for Prefix Sums?

New Gener. Comput.(2023)

Cited 0|Views0
No score
Abstract
Knuth’s 0–1 principle argues that the correctness of any swap-based sorting network can be verified by testing arbitrary sequences over Boolean values (i.e., 0 and 1). Voigtländer (Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2008, San Francisco, California, USA, January 7–12, 2008. ACM, New York, NY, pp 29–35, 2008. https://doi.org/10.1145/1328438.1328445 ) proved a similar result for prefix-sum networks that consist of associative binary operators: the correctness can be verified by testing arbitrary sequences and associative binary operators over three values, namely 0, 1, and 2. He raised the question of whether testing over Boolean values is sufficient if the binary operator is idempotent in addition to associative. This paper answers his question. First, there is an incorrect prefix-sum network for associative idempotent operators, the flaw of which cannot be detected by testing over Boolean values. Second, testing over Boolean values is sufficient if the binary operators are restricted to commutative in addition to associative and idempotent.
More
Translated text
Key words
Prefix sum,0–1 principle,Relational parametricity,Testing
AI Read Science
Must-Reading Tree
Example
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined