Fast and loose reasoning is morally correct
Fast and loose reasoning is morally correct
复制标题
快速而宽松的推理在道德上是正确的
DOI：
10.1145/1111320.1111056
复制
发表时间：
2006
影响因子：
--
通讯作者：
Danielsson N
中科院分区：
文献类型：
--
作者：
Danielsson N
函数式程序员经常对程序进行推理，就好像它们是用整体语言编写的一样，期望结果可以延续到非整体（部分）语言。我们证明了这种推理的合理性。定义了两种语言，一种是完全语言，一种是部分语言，具有相同的语法。部分语言的语义包括部分值和无限值，并且所有类型都被提升，包括函数空间。然后定义部分等价关系（PER），其域是部分语言的总子集。对于不包含函数空间的类型，PER 关联相等的值，如果函数将相关值映射到相关值，则函数是相关的。证明了，如果两个封闭项在总语言中具有相同的语义，则它们在部分语言中具有相关语义。它还表明，PER 产生了一个双笛卡尔封闭范畴，可以用来推理关系域中的值。
Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.
登录
查看更多内容
使用香蕉、镜头、信封和铁丝网进行函数式编程
DOI：
--
发表时间：
1991
期刊：
Conference on Functional Programming Languages and Computer Architecture
影响因子：
--
作者：
E. Meijer;M. Fokkinga;R. Paterson
通讯作者：
R. Paterson
追底：存在部分和无限值的程序验证案例研究
DOI：
10.1007/978-3-540-27764-4_6
发表时间：
2004
期刊：
Comparative biochemistry and physiology. Toxicology & pharmacology : CBP
影响因子：
--
作者：
Nils Anders Danielsson;Patrik Jansson
通讯作者：
Patrik Jansson
影响因子：
0.5
作者：
G. Hutton;J. Gibbons
通讯作者：
J. Gibbons
DOI：
--
发表时间：
1990
期刊：
影响因子：
--
作者：
J. Jeuring
通讯作者：
J. Jeuring
Richard Bird 和 Oege de Moor 的《编程代数》，Prentice Hall，1996 年（日期 1997 年）。
影响因子：
1.1
作者：
E. Poll;S. Thompson
通讯作者：
S. Thompson