Recursive Functions on Lazy Lists via Domains and Topologies
Recursive Functions on Lazy Lists via Domains and Topologies
复制标题
通过域和拓扑的惰性列表上的递归函数
DOI：
10.1007/978-3-319-08970-6_22
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Johannes Hölzl
中科院分区：
文献类型：
--
作者：
Andreas Lochbihler;Johannes Hölzl
定理证明器中常用的定义工具无法处理懒惰列表上的所有递归函数;过滤器函数是一个主要的反例。我们提出了两种新的方法，直接定义功能，如过滤器，利用他们的双重性质，生产者和消费者。借用域理论和拓扑学，我们将它们定义为最小不动点（生产者视图）和连续扩展（消费者视图）。这两种构造都产生了允许优雅证明的证明原则。我们期望该方法扩展到有限截断的codatestries。
The usual definition facilities in theorem provers cannot handle all recursive functions on lazy lists; the filter function is a prime counterexample. We present two new ways of directly defining functions like filter by exploiting their dual nature as producers and consumers. Borrowing from domain theory and topology, we define them as a least fixpoint (producer view) and as a continuous extension (consumer view). Both constructions yield proof principles that allow elegant proofs. We expect that the approach extends to codatatypes with finite truncations.
登录
查看更多内容
Coq 中的一些领域理论和指称语义
DOI：
10.1007/978-3-642-03359-9_10
发表时间：
2009
期刊：
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Nick Benton;A. Kennedy;C. Varming
通讯作者：
C. Varming
高阶逻辑中的机械化共归纳和共递归
DOI：
10.1093/logcom/7.2.175
发表时间：
1997
期刊：
J. Log. Comput.
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
DOI：
--
发表时间：
1995
期刊：
International Conference on Theorem Proving in Higher Order Logics
影响因子：
--
作者：
Sten Agerholm
通讯作者：
Sten Agerholm
DOI：
10.1007/3-540-48256-3_6
发表时间：
1999
期刊：
Proceedings of the 2015 Conference on Certified Programs and Proofs
影响因子：
--
作者：
John Matthews
通讯作者：
John Matthews
Holcf 11：用于验证功能程序的定义域理论
DOI：
10.15760/etd.113
发表时间：
2012
期刊：
Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell
影响因子：
--
作者：
J. Hook;B. Huffman
通讯作者：
B. Huffman