pollywog 0.1.1

Lattices

Leaves are double. A lattice is a small trait supplying bottom, top, meet, and join; a De Morgan algebra adds dual. Two are built in:

• MaxMinExtendedReal - the extended reals with \(\wedge = \min\), \(\vee = \max\), \(\bot = -\infty\), \(\top = +\infty\), and \(\neg a = -a\).

• MaxMinUnitInterval - the unit interval \([0, 1]\) with \(\wedge = \min\), \(\vee = \max\), \(\bot = 0\), \(\top = 1\), and the fuzzy negation \(\neg a = 1 - a\), giving a Kleene algebra.

Each lattice carries its polynomial type as a nested Polynomial class.

Example

>>> from pollywog import Context, Var, MaxMinExtendedReal
>>> ctx = Context[str]()
>>> K = ctx.over(MaxMinExtendedReal)
>>> x, y = K.var("x"), K.var("y")

>>> # (x AND y) OR 3.0
>>> f = x.meet(y).join(K.terminal(3.0))
>>> ctx.support(f) == {"x", "y"}
True

>>> bottom = K.lattice.bottom()
>>> f.let({Var(0): bottom, Var(1): bottom}).leaf_value()
3.0

Context maps arbitrary hashables to the integer indices CUDD keys its tables on, so you can name variables with states, atomic predicates or formula subterms. Substitution is keyed by Var, not by the bare index.

ctx.over fixes the lattice and the manager, which are constant across any stretch of code working in one lattice, so the constructors take only what varies. The context underneath stays lattice-agnostic: views over different lattices share its variable naming, so their polynomials share a support and a variable order.

Also in the Box

• Manager - owns the unique table, operation cache and variable order. There is no global runtime to start; construct one and build diagrams from it.

• BooleanFunction - BDDs, for the ordinary Boolean reasoning the polynomials omit: complementation, quantifiers, cube and prime-implicant enumeration.

• AlgebraicFunction - ADDs under CUDD’s own arithmetic, with conversions to and from BDDs.

Why not dd?

If what you want is BDDs in Python, use dd. It wraps CUDD, Sylvan and BuDDy, it has ZDDs, an expression parser and quantifiers, and it has a pure-Python backend that installs anywhere. pollywog is not trying to replace it.

The difference is at the leaves. A dd function is Boolean-valued, \(f : \mathbb{B}^n \to \mathbb{B}\), and its API is the Boolean connectives. A pollywog polynomial is lattice-valued, \(f : K^n \to K\), and its API is the lattice: meet, join, dual, substitution. CUDD has ADDs underneath, but dd does not expose them, so there is no multi-terminal diagram in it to build this on.

A finite lattice can of course be encoded as a family of Boolean functions, one BDD per cut \(\{ \mathbf{a} : f(\mathbf{a}) \ge c \}\). What that costs:

• One object instead of \(k\). Equality, hashing, node counts and substitution apply to the function itself, and sharing between the cuts is CUDD’s problem rather than yours.

• Real leaves. MaxMinExtendedReal has continuum-many values and no finite family of cuts.

• The normal form. A node is read as \(f = f_\bot \vee (x \wedge f_\top)\) under the invariant \(f_\bot \le f_\top\), so there is no complement anywhere and substitution is one meet and one join per node. Encoded into Shannon-expanded BDDs, monotonicity is an invariant you maintain by hand.

The Boolean side is still there when you want it: BooleanFunction lives in the same manager and the same variable order as the polynomials, so a skeleton and the polynomial over it share nodes instead of crossing a library boundary.

So: Boolean functions, dd. Functions valued in a lattice — fuzzy truth values, min-max robustness, weights ordered by \(\le\) — pollywog.

Building

The project builds with scikit-build-core and nanobind. With pixi:

pixi install
pixi run python -c "import pollywog"

C++ tests:

ctest --test-dir build

Documentation (needs Doxygen and Sphinx, both in the docs dependency group):

cmake --build build --target docs

The rendered output lands in build/docs/html.

Documentation

docs/ is split by audience. The concept pages — the representation and its normalization invariant, variables and ordering, managers and lifetimes — carry the long-form prose. docs/api/ documents the end-user surface of each language binding, deliberately selectively.

Internals are documented in the source rather than in the manual, so read the headers for the custom CUDD operators and the reference-counting.