Metadata-Version: 2.4
Name: pollywog
Version: 0.1.1
Summary: Polynomials over bounded distributive lattices, as multi-terminal binary decision diagrams
Author-Email: Anand Balakrishnan <anandbala1597@gmail.com>
License-Expression: BSD-3-Clause
License-File: LICENSE
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: C++
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Programming Language :: Python :: Implementation :: CPython
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: Topic :: Software Development :: Libraries
Classifier: Typing :: Typed
Project-URL: Repository, https://git.anandb.dev/pollywog.git
Project-URL: Documentation, https://docs.anandb.dev/pollywog
Requires-Python: >=3.12
Description-Content-Type: text/x-rst

``pollywog``: Polynomials Over Bounded Distributive Lattices
============================================================

A *lattice polynomial* is a term built from variables and constants
using only the lattice operations *meet* and *join*. Over a bounded
distributive lattice :math:`(K, \vee, \wedge, \bot, \top)` every such
term has a normal form, and the functions they denote are exactly the
monotone functions generated by the lattice operations. ``pollywog``
represents these functions canonically as multi-terminal binary decision
diagrams (MTBDDs), so equal polynomials are equal objects, and provides
the operations you would expect on them: meet, join, dual (on De Morgan
algebras), and substitution.

The diagrams are CUDD ADDs, so the variable order can be reordered
dynamically or imposed by hand. There is a C++ core with Python bindings
on top of it.

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
   :math:`\wedge = \min`, :math:`\vee = \max`, :math:`\bot = -\infty`,
   :math:`\top = +\infty`, and :math:`\neg a = -a`.
-  ``MaxMinUnitInterval`` - the unit interval :math:`[0, 1]` with
   :math:`\wedge = \min`, :math:`\vee = \max`, :math:`\bot = 0`,
   :math:`\top = 1`, and the fuzzy negation :math:`\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 <https://github.com/tulip-control/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,
:math:`f : \mathbb{B}^n \to \mathbb{B}`, and its API is the Boolean
connectives. A ``pollywog`` polynomial is lattice-valued,
:math:`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 :math:`\{ \mathbf{a} : f(\mathbf{a}) \ge c
\}`. What that costs:

-  One object instead of :math:`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 :math:`f = f_\bot \vee (x \wedge
   f_\top)` under the invariant :math:`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 :math:`\le` ---
``pollywog``.

Building
--------

The project builds with scikit-build-core and nanobind. With
`pixi <https://pixi.sh>`__:

.. code:: console

   pixi install
   pixi run python -c "import pollywog"

C++ tests:

.. code:: console

   ctest --test-dir build

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

.. code:: console

   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.
