$L$-fuzzy strongest postcondition predicate transformers as $L$-idempotent linear or affine operators between semimodules of monotonic predicates

TL;DR

This paper introduces $L$-fuzzy strongest postcondition predicate transformers as linear or affine operators between semimodules of fuzzy predicates, expanding the theoretical framework for fuzzy logic in program semantics.

Contribution

It establishes that under certain conditions, $L$-fuzzy strongest postcondition predicate transformers are linear or affine continuous mappings between specific semimodules.

Findings

Transformers are linear or affine under reasonable assumptions.

They are continuous mappings between $L$-idempotent semimodules.

Framework applies to fuzzy predicates in program semantics.

Abstract

For a completely distributive quantale $L$, $L$-fuzzy strongest postcondition predicate transformers are introduced, and it is shown that, under reasonable assumptions, they are linear or affine continuous mappings between continuous $L$-idempotent semimodules of $L$-fuzzy monotonic predicates.