遗传有限集、阿克曼编码和配对函数的泛函漫游指南
A Functional Hitchhiker's Guide to Hereditarily Finite Sets, Ackermann Encodings and Pairing Functions
摘要：
本文是组织作为一个独立的文学Haskell程序，实现了可执行的有限集理论的元素，重点是组合生成和算术编码。该代码在GHC 6.6.1下测试，可在http://logic.csci.unt.edu/tarau/research/2008/fSET.zip上获得。我们引入排名和unranking功能推广阿克曼的编码的遗传有限集与Urelements的宇宙。然后，我们建立一个懒惰的枚举遗传有限集与Urelements相匹配的unranking功能提供的逆阿克曼的编码，我们描述他们之间的函子导致算术编码的幂集，超图，序数和选择功能。在实现了遗传有限集的有向图表示之后，我们定义了{ \em装饰函数}，该装饰函数可以从其相关联的无环有向图的编码中恢复良基集。我们的结论与任意有向图的编码，并讨论了一个概念的对偶诱导的集合隶属关系。保留字：遗传有限集，排序和非排序函数，可执行集合论，算术编码，Haskell数据表示，函数式编程和计算数学
英文摘要：
The paper is organized as a self-contained literate Haskell program that implements elements of an executable finite set theory with focus on combinatorial generation and arithmetic encodings. The code, tested under GHC 6.6.1, is available at http://logic.csci.unt.edu/tarau/research/2008/fSET.zip . We introduce ranking and unranking functions generalizing Ackermann's encoding to the universe of Hereditarily Finite Sets with Urelements. Then we build a lazy enumerator for Hereditarily Finite Sets with Urelements that matches the unranking function provided by the inverse of Ackermann's encoding and we describe functors between them resulting in arithmetic encodings for powersets, hypergraphs, ordinals and choice functions. After implementing a digraph representation of Hereditarily Finite Sets we define {\em decoration functions} that can recover well-founded sets from encodings of their associated acyclic digraphs. We conclude with an encoding of arbitrary digraphs and discuss a concept of duality induced by the set membership relation. Keywords: hereditarily finite sets, ranking and unranking functions, executable set theory, arithmetic encodings, Haskell data representations, functional programming and computational mathematics
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
