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.
翻译:我们探索对二维直觉型理论(ITT)的定量解释,在这种理论中,身份类型被解释为一种“差异类型 ” 。 我们表明,IMT的片段,即我们称之为差异类型理论(dTT)的片段,产生了一个一般逻辑框架,用来讨论方案的量化性质,如近似等同和量的保存。为了证明这一事实,我们表明,dTT可以用来在出现错误的情况下捕捉构成推理,因为任何程序都可以与输入中与产出错误有关的“衍生”错误联系起来。此外,在将dTT的语义与ITT的标准弱化系数化系统语义联系起来之后,我们描述了为近似方案转换、递增计算、程序差异和隐私差异而开发的一些定量模型对 dTT的解释。