2020/03/20 by Joan Thibault, Thibault, Joan, Khalil Ghorbal +1
Computer Science · #Advanced Database Systems and Queries #Advanced Software Engineering Methodologies #Artificial Intelligence (cs.AI) #D.3.1 #E.1 #FOS: Computer and information sciences #Formal Methods in Verification #G.2.2 #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.2003.09340
openalex publication_date 2020/03/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We introduce a novel framework, termed λDD, that revisits Binary Decision Diagrams from a purely functional point of view. The framework allows to classify the already existing variants, including the most recent ones like Chain-DD and ESRBDD, as implementations of a special class of ordered models. We enumerate, in a principled way, all the models of this class and isolate its most expressive model. This new model, termed λDD-O-NUCX, is suitable for both dense and sparse Boolean functions, and is moreover invariant by negation. The canonicity of λDD-O-NUCX is formally verified using the Coq proof assistant. We furthermore give bounds on the size of the different diagrams: the potential gain achieved by more expressive models can be at most linear in the number of variables n.