Continuous Functions on Final Coalgebras

作     者：Ghani, Neil Hancock, Peter Pattinson, Dirk 

作者机构：Univ Nottingham Sch Comp Sci & IT Nottingham England Univ Leicester Dept Comp Sci Leicester Leics England 

出 版 物：《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)

年 卷 期：2006年第164卷第1期

页      面：141-155页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Continuous Functions Final Coalgebras Constructive Mathematics 

摘      要：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.