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的解释。

0
下载
关闭预览

相关内容

【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
机器学习在材料科学中的应用综述,21页pdf
专知会员服务
48+阅读 · 2019年9月24日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
人工智能 | 国际会议/SCI期刊约稿信息9条
Call4Papers
3+阅读 · 2018年1月12日
【论文】深度学习的数学解释
机器学习研究会
10+阅读 · 2017年12月15日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
VIP会员
相关VIP内容
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
机器学习在材料科学中的应用综述,21页pdf
专知会员服务
48+阅读 · 2019年9月24日
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
Disentangled的假设的探讨
CreateAMind
9+阅读 · 2018年12月10日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
人工智能 | 国际会议/SCI期刊约稿信息9条
Call4Papers
3+阅读 · 2018年1月12日
【论文】深度学习的数学解释
机器学习研究会
10+阅读 · 2017年12月15日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Top
微信扫码咨询专知VIP会员