MinMax.h File Reference

Min-max and max-min m-semirings over PostgreSQL enum types. More...

#include "fmgr.h"
#include "catalog/pg_enum.h"
#include "utils/catcache.h"
#include "utils/fmgroids.h"
#include "utils/syscache.h"
#include "utils/lsyscache.h"
#include "access/htup_details.h"
#include <vector>
#include <stdexcept>
#include "Semiring.h"

Include dependency graph for MinMax.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	semiring::MinMax
	Min-max / max-min m-semiring with Datum carrier over a PostgreSQL enum type. More...

Namespaces
namespace	semiring

Detailed Description

Min-max and max-min m-semirings over PostgreSQL enum types.

The min-max m-semiring associates each gate with an enum value drawn from a bounded linear order (the pg_enum.enumsortorder of the carrier enum type). Two instantiations are provided through a single class:

• MinMax (reverse = false): \(\oplus = \min\), \(\otimes = \max\), \(\mathbb{0} = \top\), \(\mathbb{1} = \bot\). This is the security / access-control shape: alternative derivations combine to the least sensitive label, and joins combine to the most sensitive label.
• MaxMin (reverse = true): \(\oplus = \max\), \(\otimes = \min\), \(\mathbb{0} = \bot\), \(\mathbb{1} = \top\). This is the fuzzy / availability / trust-level shape: alternatives combine to the most permissive label, and joins combine to the strictest label.

Operations (described for MinMax; MaxMin is symmetric):

• zero() → \(\top\) (largest enum value by sortorder)
• one() → \(\bot\) (smallest enum value by sortorder)
• plus() → enum-min over operands (empty list → zero())
• times() → enum-max over operands (empty list → one())
• monus() → \(\mathbb{0}\) if \(x \le_S y\), else \(x\), where \(\le_S\) is the semiring order
• delta() → identity (preserves the lattice value of the support so that aggregated groups carry the meaningful classification of contributing rows rather than a flattened one())

Absorptivity: absorptive() returns true. With inputs in the bounded order, \(\mathbb{1} \oplus a = a \oplus \mathbb{1} = \mathbb{1}\) in both instantiations.

Note

Bottom and top are looked up once in the constructor from pg_enum.enumsortorder via the ENUMTYPOIDNAME syscache. Element comparison goes through F_ENUM_CMP via OidFunctionCall2, which handles the typecache lookup internally.

See also

https://provsql.org/lean-docs/Provenance/Semirings/MinMax.html Lean 4 verified instance: instSemiringWithMonusMinMax (and MaxMin = MinMax(OrderDual)).

Definition in file MinMax.h.