论文标题
有序的功能决策图：二进制决策图的功能语义
Ordered Functional Decision Diagrams: A Functional Semantics For Binary Decision Diagrams
论文作者
论文摘要
我们介绍了一个新颖的框架，称为$λ$ DD，从纯粹的功能角度重新审视二进制决策图。该框架允许对已经存在的变体进行分类，包括最新的变体，例如链-DD和ESRBDD，作为特殊类别模型的实现。我们以原则上的方式列举了该类别的所有模型，并隔离了其最具表现力的模型。这种称为$λ$ dd-o-nucx的新模型适用于密集和稀疏的布尔功能，而且由于否定而不变。 $λ$ DD-O-NUCX的规范性使用COQ证明助手正式验证。此外，我们给出了不同图表的大小的边界：更具表现力模型所获得的潜在增益最多可以是变量n数量的线性。
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.
