Proving Properties about Lists Using Containers
Proving Properties about Lists Using Containers
复制标题
使用容器证明列表的属性
DOI：
10.1007/978-3-540-78969-7_9
复制
发表时间：
2008
影响因子：
3.2
通讯作者：
Conor McBride
中科院分区：
文献类型：
--
作者：
R. Prince;Neil Ghani;Conor McBride
Bundy 和 Richardson [7] 提出了一种使用省略号（1 + 2 + ... + 10 中的点）推理列表的技术，其中用 □ 表示的多态函数用于封装列表函数的递归定义，并且使用省略号的描述系统给出了非正式的证明。我们强调了该技术的某些局限性，并使用最近开发的容器理论解决了这些局限性，该理论捕捉到了许多重要数据类型由存储数据的模板组成的想法。我们在 Coq 中实现了我们的想法，并演示了如何使用它们来证明 Bundy 和 Richardson 在 [7] 中未能解决的定理。
Bundy and Richardson [7] presented a technique for reasoning about lists using ellipsis (the dots in 1 + 2 + ... + 10), where a polymorphic function, denoted by □, is used to encapsulate recursive definitions of list functions and a portrayal system using ellipsis gives an informal proof. We highlight certain limitations of this technique and address these limitations using the recently developed theory of containers which capture the idea that many important datatypes consist of templates where data is stored. We implement our ideas in Coq and demonstrate how they can be used to prove theorems that eluded Bundy and Richardson in [7].