一句话:将定量代数推广到模糊关系和广义度量空间,不要求运算非扩张,并建立完备证明系统、自由代数与单子性结果。
经典定量代数由 Mardare、Panangaden 和 Plotkin 提出,其载体限定为度量空间,且代数运算必须是非扩张映射,这限制了可建模的系统。本文将定量代数推广到两个方向:载体可以是任意模糊关系或广义度量空间;运算解释无需非扩张。作者采用范畴论与泛代数方法研究其语义,主要结果包括:提出一个新的可靠且完备的证明系统,证明自由定量代数总是存在,证明由自由-遗忘伴随诱导的严格单子性,并表明所有提升集合上有限单子的模糊关系单子都具有定量等式表示。工作属于理论性结果,以数学证明而非实验评估。
We present a generalisation of the theory of quantitative algebras of Mardare, Panangaden and Plotkin where (i) the carriers of quantitative algebras are not restricted to be metric spaces and can be arbitrary fuzzy relations or generalised metric spaces, and (ii) the interpretations of the algebraic operations are not required to be nonexpansive. Our main results include: a novel sound and complete proof system, the proof that free quantitative algebras always exist, the proof of strict monadicity of the induced Free-Forgetful adjunction, the result that all monads (on fuzzy relations) that lift finitary monads (on sets) admit a quantitative equational presentation.
@article{paperbot2702,
title = {Universal Quantitative Algebra for Fuzzy Relations and Generalised Metric Spaces},
author = {Matteo Mio and Ralph Sarkis and Valeria Vignudelli},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:19)2024}
}