量化 lambda 演算与加性析取
Quantalic lambda-calculus and additive disjunction
浏览论文内容
中文总结 AI 辅助
本文将量化线性 lambda 演算扩展为含加性析取的系统，证明其可靠性与近似完备性，给出多类模型并结合 Banach 空间概率模型实现随机游走柯西序列的量化推理，推动程序语义向量化视角转变。
中文摘要 AI 辅助
出于对条件语句进行量化推理的需求，我们将量化线性 lambda 演算扩展为包含加性析取的系统。我们证明所得等式系统是可靠的；当采用基础 quantale 的某些连续性性质时，该系统还具备（近似）完备性。我们给出了扩展演算的若干模型，包括范畴逻辑中的元理论性质（胶合）、概率计算与量子计算等。作为具体应用，我们展示了基于 Banach 空间的概率模型如何与演算的等式系统协同使用，以对随机游走的柯西序列进行推理。这凸显了从“程序语义作为程序等价性的科学”向包含泛函分析等领域的灵活量化视角的新兴转变。
英文摘要
Motivated by the need to reason about case statements quantitatively, we extend quantalic linear lambda-calculus with additive disjunction. We show that the resulting equational system is sound. We also show that when certain continuity properties (of the underlying quantale) are adopted, it is additionally (approximately) complete. We present several models of the extended calculus, involving for example meta-theoretical properties in categorical logic (gluing), probabilistic, and quantum computation. As a concrete application, we illustrate how a probabilistic model, based on Banach spaces, can be synergistically used with the calculus' equational system to reason about Cauchy sequences of random walks. This highlights the emergent shift from "program semantics as the science of program equivalence" to flexible, quantitative perspectives, involving functional analysis and beyond.
