ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy
Wed 4 Sep 2024 15:48 - 16:06 at Green 1-2-3 - Verification and Cost Analysis Chair(s): Clément Pit-Claudel

This paper describes a purely functional library for computing level-p-complexity of Boolean functions and applies it to two-level iterated majority. Boolean functions are simply functions from n bits to one bit, and they can describe digital circuits, voting systems, etc. An example of a Boolean function is majority, which returns the value that has majority among the n input bits for odd n. The complexity of a Boolean function f measures the cost of evaluating it: how many bits of the input are needed to be certain about the result of f. There are many competing complexity measures, but we focus on level-p-complexity — a function of the probability p that a bit is 1. The level-p-complexity Dp(f) is the minimum expected cost when the input bits are independent and identically distributed with Bernoulli(p) distribution. We specify the problem as choosing the minimum expected cost of all possible decision trees — which directly translates to a clearly correct, but very inefficient implementation. The library uses thinning and memoization for efficiency and type classes for separation of concerns. The complexity is represented using (sets of) polynomials, and the order relation used for thinning is implemented using polynomial factorization and root counting. Finally, we compute the complexity for two-level iterated majority and improve on an earlier result by J. Jansson.

Wed 4 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:30 - 16:42
Verification and Cost AnalysisJFP First Papers / ICFP Papers and Events at Green 1-2-3
Chair(s): Clément Pit-Claudel EPFL
15:30
18m
Talk
Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
ICFP Papers and Events
Li-yao Xia Unaffiliated, Laura Israel Portland State University, Maite Kramarz University of Toronto, Nicholas Coltharp Portland State University, Koen Claessen Chalmers University of Technology, Stephanie Weirich University of Pennsylvania, Yao Li Portland State University
DOI Pre-print
15:48
18m
Talk
Level-p-complexity of Boolean functions using thinning, memoization, and polynomialsJFP First Paper
JFP First Papers
Julia Jansson , Patrik Jansson Chalmers University of Technology and University of Gothenbrug
DOI
16:06
18m
Talk
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
ICFP Papers and Events
Cole Kurashige University of California at San Diego, Ruyi Ji Peking University, Aditya Giridharan University of California at San Diego, Mark Barbone University of California at San Diego, Daniel Noor Technion, Shachar Itzhaky Technion, Ranjit Jhala University of California at San Diego, Nadia Polikarpova University of California at San Diego
DOI
16:24
18m
Talk
Contract Lenses: Reasoning about Bidirectional Programs via CalculationJFP First Paper
JFP First Papers
Hanliang Zhang University of Bristol, UK, Wenhao Tang University of Edinburgh, Ruifeng Xie Peking University, Meng Wang University of Bristol, Zhenjiang Hu Peking University
DOI