Tiered Objects

• Autorzy: Alessi F. , Cardone F.

Identyfikatory

DOI

10.3233/FI-2016-1449

• Języki publikacji: EN

Abstrakty

EN

We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.

Słowa kluczowe

EN

complete Heyting algebras; sheave; initial algebras; final coalgebras; infinite data structures; approximation lemma

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 149, nr 3
• Strony: 263--295
• Opis fizyczny: Bibliogr. 39 poz., rys.

Twórcy

autor

Alessi F.

• Dipartimento di Scienze Matematiche Informatiche e Fisiche, Università di Udine, via delle Scienze 206, I-33100 Udine, Italy

autor

Cardone F.

• Dipartimento di Informatica, Università di Torino, corso Svizzera 185 I-10149 Torino, Italy

Bibliografia

• [1] Bruce K, Mitchell JC. PER models of subtyping, recursive types and higher-order polymorphism. In: Proceedings of the ACM Fourth Symposium on Principles of Programming Languages. ACM; 1992. p. 316–327. doi:10.1145/143165.143230.
• [2] Baier C, Majster-Cederbaum ME. Metric Semantics from Partial Order Semantics. Acta Informatica. 1997;34(9):701–735. doi:10.1007/s002360050104.
• [3] Kummetz R. From Partial Orders with Projections to Domains. Electronic Notes in Theoretical Computer Science. 1999;20:334-345. doi:10.1016/S1571-0661(04)80082-3.
• [4] Herrlich H, Ehrig H. The construct PRO of projection spaces: Its internal structure. In: Ehrig H, Herrlich H, Kreowski HJ, Preuß G, editors. Categorical Methods in Computer Science – with Aspects from Topology. vol. 393 of Lecture Notes in Computer Science. Berlin: Springer-Verlag; 1989. p. 286–293. Available from: http://dl.acm.org/citation.cfm?id=94846.94886.
• [5] Bergstra JA, Klop JW. An introduction to process algebra. In: Baeten JCM, editor. Applications of Process Algebra. No. 17 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press; 1990. p. 1–21.
• [6] Kranakis E. Fixed point equations with parameters in the projective model. Information and Computation. 1987;75(3):264-288. doi:10.1016/0890-5401(87)90003-4.
• [7] Monteiro L. Semantic domains based on sets with families of equivalences. Electronic Notes in Theoretical Computer Science. 1998;11:71–104. doi:10.1016/S1571-0661(04)00054-4.
• [8] Stoltenberg-Hansen V, Lindström I, Griffor ER. Mathematical Theory of Domains. No. 22 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press; 1994.
• [9] Buchholz W. A term calculus for (co-)recursive definitions on streamlike data structures. Annals of Pure and Applied Logic. 2005;136(1-2):75–90. doi:10.1016/j.apal.2005.05.006.
• [10] Matthews J. Recursive functions defined over coinductive types. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Théry L, editors. Proceedings of TPHOL ’99. vol. 1690 of Lecture Notes in Computer Science. Berlin: Springer-Verlag; 1999. p. 73–90. Available from: http://dl.acm.org/citation.cfm?id=646526.756867.
• [11] Bukatin MA, Kopperman R, Matthews SG, Pajoohesh H. Partial Metric Spaces. The American Mathematical Monthly. 2009;116(8):708–718. doi:10.4169/193009709X460831.
• [12] Fourman MP, Scott DS. Sheaves and Logic. In: Fourman MP, Mulvey C, Scott DS, editors. Applications of Sheaves. vol. 753 of Lecture Notes in Mathematics. Berlin: Springer-Verlag; 1979. p. 302–401. doi:10.1007/BFb0061824.
• [13] Gianantonio PD, Miculan M. Unifying Recursive and Co-recursive Definitions in Sheaf Categories. In: Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004. vol. 2987 of Lecture Notes in Computer Science. Springer; 2004, p 136–150. doi:10.1007/978-3-540-24727-2_11.
• [14] Barr M. Terminal coalgebras in well-founded set theory. Theoretical Computer Science. 1993; 114:299–315.
• [15] Adámek J. Final coalgebras are ideal completions of initial algebras. Journal of Logic and Computation. 2002;12(2):217–242. doi: 10.1093/logcom/12.2.217.
• [16] Gibbons J, Hutton G. Proof Methods for Corecursive Programs. Fundamenta Informaticae. 2005; 66(4):353–366. Available from: http://dl.acm.org/citation.cfm?id=2370162.2370165.
• [17] Brandt M, Henglein F. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informatica. 1998; 33:309–338. Available from: http://dl.acm.org/citation.cfm?id=2379036.2379037.
• [18] Coquand T. Infinite objects in type theory. In: Barendregt H, Nipkow T, editors. Types for Proofs and Programs. vol. 806 of Lecture Notes in Computer Science. Berlin: Springer-Verlag; 1993. p. 62–78. doi:10.1007/3-540-58085-9_72.
• [19] Horn A. Logic with truth values in a linearly ordered Heyting algebra. Journal of Symbolic Logic. 1969;34(3):395–408. Available from: http://dx.doi.org/10.2307/2270905.
• [20] Goldblatt R. Topoi. The Categorial Analysis of Logic. Amsterdam: North-Holland Co., 1979. ISBN-13: 978-0486450261, 10: 0486450260.
• [21] Simmons H. The Point-Free Approach to Sheafification; 2001. Available from: http://www.cs.man.ac.uk/~hsimmons/DOCUMENTS/PAPERSandNOTES/Omegasets.pdf.
• [22] Bird RS. Introduction to Functional Programming Using Haskell. Prentice-Hall; 1998. ISBN-13: 978-0134843469, 10: 0134843460.
• [23] Hutton G, Gibbons J. The Generic Approximation Lemma. Information Processing Letters. 2001; 79(4):197–201.
• [24] Dedekind R. Essays on the Theory of Numbers. Open Court Publishing Company; 1901. Translation by W.W. Beman of Stetigkeit und irrationale Zahlen (1872) and Was sind und was sollen die Zahlen? (1888), reprinted 1963 by Dover Press.
• [25] Henkin L. On mathematical induction. American Mathematical Monthly. 1960;67:323–338. doi:10.2307/2308975.
• [26] Flagg B, Kopperman R. Computational models for ultrametric spaces. Electronic Notes in Theoretical Compututer Science. 1997; 6:151–159. doi:10.1016/S1571-0661(05)80164-1.
• [27] Ehrig H, Parisi-Presicce F, Boehm P, Rieckhoff C, Dimitrovici C, Grosse-Rhode M. Algebraic data type and process specification based on projection spaces. In: Recent trends in data type specifications. No.332 in Lecture Notes in Computer Science. Springer; 1988. p. 23–43. Available from: http://dl.acm.org/citation.cfm?id=55432.55434.
• [28] Walters RFC. Sheaves and Cauchy-complete categories. Cahiers de Topologie et Geometrie Differentielle. 1981; 22:283–286. Available from: http://eudml.org/doc/91273.
• [29] Walters RFC. Sheaves on sites as Cauchy-complete categories. Journal of Pure and Applied Algebra. 1982; 24:95–102. doi:10.1016/0022-4049(82)90061-5.
• [30] Wagner KR. Solving recursive domain equations with enriched categories. Carnegie Mellon University; July 1994. Technical Report CMU-CS-94-159. Available from: https://books.google.pl/books?id=rZnfoQEACAAJ.
• [31] Wagner KR. Liminf convergence in Ω-categories. Theoretical Computer Science. 1997;184:61–104. doi:10.1016/S0304-3975(96)00223-X.
• [32] Majster-Cederbaum ME, Baier C. Metric completion versus ideal completion. Theoretical Computer Science. 1996;170(1-2):145–171. doi:10.1016/0304-3975(95)00262-6.
• [33] Kelley JL. General Topology. Springer Verlag; 1975. ISBN:978-0-387-90125-1.
• [34] Mac Lane S. Categories for the Working Mathematician. Springer-Verlag; 1998. doi:10.1007/978-1-4757-4721-8.
• [35] Barendregt HP, Dekkers WJM, Statman R. Lambda Calculus with Types. Perspectives in Mathematical Logic. Cambridge University Press/Association for Symbolic Logic; 2013. ISBN-13:978-0521766142, 10:0521766141.
• [36] Winskel G. The Formal Semantics of Programming Languages: An Introduction. Cambridge, MA, USA: MIT Press; 1993. ISBN:0-262-23169-7.
• [37] Kozen D. Coinductive Proof Principles for Stochastic Processes. Logical Methods in Computer Science. 2007;3(4):1–14. doi:10.2168/LMCS-3(4:8)2007.
• [38] Kozen D, Ruozzi N. Applications of Metric Coinduction. Logical Methods in Computer Science. 2009;5(3). doi:10.2168/LMCS-5(3:10)2009.
• [39] Dijkstra EW. Proving the equality of infinite sequences; 1991. Circulated privately. Available from: http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1093.PDF.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).