从同一性到差异性：同一性类型的定量解释
From Identity to Difference: A Quantitative Interpretation of the Identity Type
摘要：
我们探讨了一个定量的解释2维直觉类型论（ITT）中的身份类型被解释为“类型的差异”。我们表明，一个片段的ITT，我们称之为差异类型论（dTT），产生一个一般的逻辑框架来谈论定量性质的程序，如近似等价和度量保存。为了证明这一事实，我们表明，dTT可以用来捕捉组合推理中存在的错误，因为任何程序都可以与“衍生”相关的错误输入与错误输出。此外，在有关的语义dTT的标准弱因子分解系统语义的ITT，我们描述了一些定量模型的近似程序转换，增量计算，程序分化和差分隐私的dTT的解释。
英文摘要：
We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a fragment of ITT, that we call difference type theory (dTT), yields a general logical framework to talk about quantitative properties of programs like approximate equivalence and metric preservation. To demonstrate this fact, we show that dTT can be used to capture compositional reasoning in presence of errors, since any program can be associated with a "derivative" relating errors in input with errors in output. Moreover, after relating the semantics of dTT to the standard weak factorization systems semantics of ITT, we describe the interpretation of dTT in some quantitative models developed for approximate program transformations, incremental computing, program differentiation and differential privacy.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
