Continuous Functions on Final Coalgebras
Continuous Functions on Final Coalgebras
复制标题
最终余代数上的连续函数
DOI：
10.1016/j.entcs.2006.06.009
复制
发表时间：
2009
影响因子：
0.3
通讯作者：
D. Pattinson
中科院分区：
文献类型：
--
作者：
Neil Ghani;P. Hancock;D. Pattinson
它可以追溯到布劳威尔，连续函数的类型StrA→B，其中StrA是类型的无限流的元素A，可以表示为良好的基础，A-分支树的叶子是元素B。本文将上述对应关系推广到集合和函数范畴上幂级数函子的最终余代数上定义的函数。虽然我们的主要技术贡献是所有连续函数的特征，定义在一个最终的余代数，并采取值在离散空间的归纳类型的手段，方法的一点是，这些归纳类型是最方便制定的依赖型理论的框架。
It can be traced back to Brouwer that continuous functions of type StrA→B, where StrA is the type of infinite streams over elements of A, can be represented by well founded, A-branching trees whose leafs are elements of B. This paper generalises the above correspondence to functions defined on final coalgebras for power-series functors on the category of sets and functions. While our main technical contribution is the characterisation of all continuous functions, defined on a final coalgebra and taking values in a discrete space by means of inductive types, a methodological point is that these inductive types are most conveniently formulated in a framework of dependent type theory.