IntervalUnion.h File Reference

Interval-union m-semiring over PostgreSQL multirange types. More...

#include "fmgr.h"
#include "catalog/pg_type.h"
#include "utils/fmgroids.h"
#include "utils/multirangetypes.h"
#include "utils/lsyscache.h"
#include <vector>
#include "Semiring.h"

Include dependency graph for IntervalUnion.h:

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

Go to the source code of this file.

Classes
class	semiring::IntervalUnion
	Interval-union m-semiring with Datum carrier, parameterised by a multirange type OID. More...

Namespaces
namespace	semiring

Detailed Description

Interval-union m-semiring over PostgreSQL multirange types.

The interval-union m-semiring associates each gate with a finite union of pairwise-disjoint intervals over a densely-ordered linear domain (timestamp, numeric, integer, ...). Addition is multirange union, multiplication is intersection, and monus is set difference. The class is parameterised by a multirange type OID, so a single implementation covers tstzmultirange (the temporal instance), nummultirange (numeric validity ranges), and int4multirange (integer page/line ranges) — and any other multirange type the user happens to define.

Operations:

• zero() → '{}' (empty multirange)
• one() → '{(,)}' (universal multirange)
• plus() → multirange union (multirange_union)
• times() → multirange intersection (multirange_intersect)
• monus() → multirange set difference (multirange_minus)
• delta() → identity (preserves the supporting multirange so that aggregated groups carry the actual time/parameter region of contributing rows rather than the universal range)

Absorptivity: absorptive() returns true. With inputs being subsets of the universal range, \(\mathbb{1} \oplus a = (-\infty,+\infty) \cup a = (-\infty,+\infty) = \mathbb{1}\).

Note

Requires PostgreSQL 14+ (multirange types). The polymorphic built-ins F_MULTIRANGE_UNION / F_MULTIRANGE_INTERSECT / F_MULTIRANGE_MINUS work for every multirange carrier and access fcinfo->flinfo->fn_extra for type-cache lookups, so they must be invoked through OidFunctionCall* (which builds a proper FmgrInfo) rather than DirectFunctionCall* (which leaves flinfo NULL and would crash).

See also

https://provsql.org/lean-docs/Provenance/Semirings/IntervalUnion.html Lean 4 verified instance: instSemiringWithMonusIntervalUnion, with proofs of IntervalUnion.absorptive and IntervalUnion.mul_sub_left_distributive.

Definition in file IntervalUnion.h.