Tropical.h File Reference

Tropical (min-plus) m-semiring over \(\mathbb{R} \cup \{+\infty\}\). More...

#include <algorithm>
#include <limits>
#include <numeric>
#include <vector>
#include "Semiring.h"

Include dependency graph for Tropical.h:

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

Go to the source code of this file.

Classes
class	semiring::Tropical
	Tropical (min-plus) m-semiring over double. More...

Namespaces
namespace	semiring

Detailed Description

Tropical (min-plus) m-semiring over \(\mathbb{R} \cup \{+\infty\}\).

The tropical m-semiring ( \(\mathbb{R} \cup \{+\infty\}\), \(\min\), \(+\), \(+\infty\), 0) is used to model shortest-path/least-cost provenance: input gates carry edge weights (or costs), \(\oplus = \min\) selects the cheapest derivation, and \(\otimes = +\) accumulates cost along a derivation.

Operations:

• zero() → \(+\infty\)
• one() → 0
• plus() → minimum of all operands (empty list → \(+\infty\))
• times() → sum of all operands (empty list → 0)
• monus() → \(+\infty\) if \(x \ge y\) in the usual order, \(x\) otherwise (note this is the reverse of the natural semiring order; see Lean reference)
• delta() → \(+\infty\) if x is \(+\infty\), else 0

Absorptivity: absorptive() returns false. The Lean formalisation proves absorptivity only for canonically-ordered carriers (e.g. \(\mathbb{N}\)); over arbitrary double values (including negatives) \(\mathbb{1} \oplus a = \min(0, a)\) is not always 0.

See also

https://provsql.org/lean-docs/Provenance/Semirings/Tropical.html Lean 4 verified instance: instSemiringWithMonusTropicalWithTop, with proofs of Tropical.absorptive (under CanonicallyOrderedAdd) and Tropical.mul_sub_left_distributive.

Definition in file Tropical.h.