Interfaces as functors, programs as coalgebras - A final coalgebra theorem in intensional type theory

摘要

In [P. Hancock, A. Setzer, Interactive programs in dependent type theory, in: P. Clote, H. Schwichtenberg (Eds.), Proc. 14th Annu. Conf. of EACSL, CSL'00, Fischbau, Germany, 21-26 August 2000, Vol. 1862, Springer, Berlin, 2000, pp. 317-331, URL (citeseer.ist.psu.edu/article/hancock00interactive.html); P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in: L. Crosilla, P. Schuster (Eds.), From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, Clarendon Press, 2005, URL 〈www.cs.swan.ac.uk/～csetzer/〉] Hancock and Setzer introduced rules to extend Martin-Lof's type theory in order to represent interactive programming. The rules essentially reflect the existence of weakly final coalgebras for a general form of polynomial functor. The standard rules of dependent type theory allow the definition of inductive types, which correspond to initial algebras. Coalgebraic types are not represented in a direct way. In this article we show the existence of final coalgebras in intensional type theory for these kind of functors, where we require uniqueness of identity proofs (UIP) for the set of states S and the set of commands C which determine the functor. We obtain the result by identifying programs which have essentially the same behaviour, viz. are bisimular. This proves the rules of Setzer and Hancock admissible in ordinary type theory, if we replace definitional equality by bisimulation. All proofs [M. Michel-brink, Verifications of final coalgebra theorem in: Interfaces as Functors, Programs as Coalgebras - A Final Coalgebra Theorem in Intensional Type Theory, 2005, URL 〈www.cs.swan.ac.uk/～csmichey〉] are verified in the theorem prover agda [C. Coquand, Agda, Internet, URL 〈www.cs.chalmers.se/～catarina/agda〉]; K. Peterson, A programming system for type theory, Technical Report, S-412 96, Chalmers University of Technology, Goteborg, 1982], which is based on intensional Martin-Lof type theory.