Lukasiewicz.h File Reference

Łukasiewicz fuzzy m-semiring over \([0,1]\). More...

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

Include dependency graph for Lukasiewicz.h:

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

Go to the source code of this file.

Classes
class	semiring::Lukasiewicz
	The Łukasiewicz fuzzy m-semiring over double. More...

Namespaces
namespace	semiring

Detailed Description

Łukasiewicz fuzzy m-semiring over \([0,1]\).

The Łukasiewicz m-semiring ( \([0,1]\), \(\max\), \(\otimes_{\text{Ł}}\), 0, 1) is used to model graded-truth provenance: input gates carry degree-of-evidence values in \([0,1]\), \(\oplus = \max\) keeps the strongest alternative, and \(\otimes_{\text{Ł}}(a,b) = \max(a + b - 1, 0)\) is the Łukasiewicz t-norm, the bounded-loss conjunction.

Operations:

• zero() → 0
• one() → 1
• plus() → maximum of all operands (empty list → 0)
• times() → \(\max(\sum_i a_i - (n-1), 0)\) for \(n\) operands (empty list → 1)
• monus() → 0 if \(a \le b\), \(a\) otherwise
• delta() → 1 if x is non-zero, else 0

Absorptivity: absorptive() returns true. With inputs in \([0,1]\), \(\mathbb{1} \oplus a = \max(1, a) = 1\). The circuit evaluator may exploit the resulting idempotency to deduplicate operands.

Compared to Viterbi (which uses \(a \cdot b\) for ⊗): the Łukasiewicz t-norm preserves crisp truth ( \(0.7 \otimes 1 = 0.7\)) and does not collapse long conjunctions to near-zero, making it the standard fuzzy choice for graded but non-probabilistic conjunctions.

Note

No bounds checking is performed: it is the caller's responsibility to supply input values in \([0,1]\).

See also

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

Definition in file Lukasiewicz.h.