/ 
Aion-2.4
⭐ Starred 1 / Aion::Type::DNF

NAME

Aion::Type::DNF - casting an expression type to DNF by equivalent conversions

SYNOPSIS

use Aion::Types qw/Range None/;

my $gap = Range[-10, 0] & Range[4, 8];
$gap->_simplify eq None   # -> 1

DESCRIPTION

This is the role that Aion::Type includes. Contains utility methods for expanding an expression type (combinations &, |, ~) into DNF - disjunctive normal form.

This module implements algorithm No. 1 from the list of methods for constructing DNFs:

1. Equivalent transformations based on the laws of Boolean algebra ✅ (implemented here).
2. Truth table method (construction of SDNF).
3. Tseitin’s algorithm (introduction of “garbage” variables).
4. Algorithms based on BDD (Binary Decision Diagrams).

Explanation of the remaining options (for context):

  • Truth Table Method (TRMT) - iterates through all sets of variable values and collects a perfect DNF based on the units of the function. It is exponential in the number of variables and therefore is not applicable to “large” types.

  • Tseitin's algorithm - introduces auxiliary variables and builds CNF with linear size (mainly for SAT solvers), rather than DNF.

  • BDD - collapses the decision tree, separating identical subtrees.

Here the DNF is obtained purely algebraically: by opening the brackets according to the law of distributivity.

ALGORITHM

General chain of transformations (see _simplify method in Aion::Type):

_unfolding -> _pushing -> _distribute

Each step is an equivalent transformation according to the laws of Boolean algebra:

  • _unfolding - opens the chain of limiting types A as B as C into an equivalent intersection of A & B & C “head-on”, preventing combination with already set-theoretical operations.

  • _pushing — “pushes” negations to terms according to De Morgan’s laws and inversion of ranges/enumerations: ~(A | B) => ~A & ~B, ~(A & B) => ~A | ~B, ~~A => A.

  • _distribute - applies the law of distributivity and expands the intersection of unions into an intersection union (DNF):

    (A | B) & (C | D | E) & F => (A & C & F) | (A & D & F) | (A & E & F) | (B & C & F) | (B & D & F) | (B & E & F)

Intersections/unions are then collapsed by auxiliary functions _intersection and _union, which result in terms (by ranges - _intersection_ranges/_union_ranges, by enumerations - _union_enums/_intersection_enums).

A term is considered an atom: a type without set-theoretic operators or explicitly allocated "chunks" after _unfolding and _pushing.

AUTHOR

Yaroslav O. Kosmina mailto:dart@cpan.org

LICENSE

⚖ GPLv3

COPYRIGHT

The Aion::Type::DNF module is copyright © 2026 Yaroslav O. Kosmina. Rusland. All rights reserved.