paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On the axiomatizability of quantitative algebras

论定量代数的可公理化性
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 1/10 · 该论文研究定量代数的公理化与簇/拟簇定理,属于纯数学逻辑与形式语义基础理论,与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析及其交叉方向没有直接关联。引用 48 inbox
Radu Mardare, Prakash Panangaden, Gordon Plotkin
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:系统刻画定量代数可由简单定量等式、受限及一般 Horn 子句公理化的范围,并证明相应簇/拟簇定理。

定量代数(QAs)是由定量等式理论定义的度量空间上的代数,为概率、随机及其他定量系统的度量语义提供数学基础。本文研究 QAs 的可公理化问题,考察可用于公理化理论的定量等式谱系:简单定量等式;以不超过 c 个变量间等式为前提的 Horn 子句(c 为基数);以及最一般的 Horn 子句。作者分别刻画相应的 QA 类,并证明簇/拟簇定理,推广了经典代数与一阶结构模型论中的结果。该工作为定量语义的代数公理化提供统一框架。

问题
研究定量代数能否以及如何由不同类型的定量等式与 Horn 子句公理化,并刻画相应代数类。
方法
按简单定量等式、受限 Horn 子句和一般 Horn 子句三个层次分析公理化能力,证明相应的 variety/quasivariety 表示定理。
评估
通过数学定理证明与模型论比较进行理论评估,不涉及实现或实验。
原文摘要(Abstract)

Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by us in 2016. They provide the mathematical foundation for metric semantics of probabilistic, stochastic and other quantitative systems. This paper considers the issue of axiomatizability of QAs. We investigate the entire spectrum of types of quantitative equations that can be used to axiomatize theories: (i) simple quantitative equations; (ii) Horn clauses with no more than c equations between variables as hypotheses, where c is a cardinal and (iii) the most general case of Horn clauses. In each case we characterize the class of QAs and prove variety/quasivariety theorems that extend and generalize classical results from model theory for algebras and first-order structures.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{MardarePP17,
  title = {On the axiomatizability of quantitative algebras},
  author = {Radu Mardare and Prakash Panangaden and Gordon Plotkin},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005102}
}