Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-09T02:23:05.882Z Has data issue: false hasContentIssue false
  • English
  • Français

Nonflatness and totality

Published online by Cambridge University Press:  16 April 2018

BASIL A. KARÁDAIS
BASIL A. KARÁDAIS*
Affiliation:
Mathematisches Institut, Ludwig-Maximilians-Universität München, Munich 80333, Germany Email: karadais@math.lmu.de
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We interpret finite types as domains over nonflat inductive base types in order to bring out the finitary core that seems to be inherent in the concept of totality. We prove a strong version of the Kreisel density theorem by providing a total compact element as a witness, a result that we cannot hope to have if we work with flat base types. To this end, we develop tools that deal adequately with possibly inconsistent finite sets of information. The classical density theorem is reestablished via a ‘finite density theorem,’ and corollaries are obtained, among them Berger's separation property.

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 2 , February 2019 , pp. 309 - 338
Copyright
Copyright © Cambridge University Press 2018 

References

Bauer, A. and Birkedal, L. (2000). Continuous functionals of dependent types and equilogical spaces. In: Proceedings of the 14th EASCL Annual Conference on Computer Science Logic (CSL '2000), Fischbachau, Germany, August 21–26, Springer, 202–216.Google Scholar
Berger, U. (1990). Totale Objekte und Mengen in der Bereichstheorie (Total objects and sets in domain theory). Univ. München, Fak. für Mathematik. ii, 122 S.Google Scholar
Berger, U. (1993). Total sets and objects in domain theory. Annals of Pure and Applied Logic 60 (2) 91–117.Google Scholar
Berger, U. (1999a). Continuous functionals of dependent and transfinite types. In: Models and Computability. Invited Papers from the Logic Colloquium '97, European Meeting of the Association for Symbolic Logic, Leeds, UK, July 6–13, Cambridge University Press, 1–22.Google Scholar
Berger, U. (1999b). Effectivity and density in domains: A survey. In: A Tutorial Workshop on Realizability Semantics and Applications. A Workshop Associated to the Federated Logic Conference, Trento, Italy, June 30–July 1, Elsevier, 13.Google Scholar
Berger, U. (2002). Computability and totality in domains. Mathematical Structures in Computer Science 12 (3) 281–294.Google Scholar
Berger, U. (2009). Realisability and adequacy for (co)induction. In: Proceedings of the 6th International Conference on Computability and Complexity in Analysis (CCA'09), August 18–22, Ljubljana, Slovenia, Schloss Dagstuhl – Leibniz Zentrum für Informatik, 12.Google Scholar
Berger, U. (2011). From coinductive proofs to exact real arithmetic: Theory and applications. Logical Methods in Computer Science 7 (1) 24.Google Scholar
Berger, U., Miyamoto, K., Schwichtenberg, H. and Seisenberger, M. (2011). Minlog–-A tool for program extraction supporting algebras and coalgebras. In: Algebra and Coalgebra in Computer Science – Proceedings of the 4th International Conference (CALCO '11), Winchester, UK, August 30–September 2, 393–399.Google Scholar
Berger, U., Miyamoto, K., Schwichtenberg, H. and Tsuiki, H. (2016). Logic for gray-code computation. In Dieter, P. and Peter, S. (eds.): Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter.Google Scholar
Berger, U. and Seisenberger, M. (2012). Proofs, programs, processes. Theory of Computing Systems 51 (3) 313–329.Google Scholar
Ershov, Y.L. (1975a). Maximal and everywhere-defined functionals. Algebra Logic 13 210–225.Google Scholar
Ershov, Y.L. (1975b). Theorie der Numerierungen. II (Theory of numberings. II) Übersetzung aus dem Russischen: H.-D. Hecker. Wissenschaftliche Redaktion: G. Asser. Berlin: VEB Deutscher Verlag der Wissenschaften. M 15.00 (1976). Sonderdruck aus Z. math. Logik Grundl. Math. 21 473–584 (1975).Google Scholar
Ershov, Y.L. (1977). Model ℂ of partial continuous functionals. In: Logic Colloquium 76, Proceedings of a Conference held at Oxford in 1976, Studies in Logic and the Foundations of Mathematics, vol. 87, 455–467.Google Scholar
Escardó, M.H. (2007). Infinite sets that admit fast exhaustive search. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS '07), Washington, DC, USA, IEEE Computer Society, 443–452.Google Scholar
Escardó, M.H. (2008). Exhaustible sets in higher-type computation. Logical Methods in Computer Science 4 (3) 37.Google Scholar
Ghani, N., Hancock, P.G. and Pattinson, D. (2009). Continuous functions on final coalgebras. In: Proceedings of the 25th Conference on the Mathematical Foundations of Programming Semantics (MFPS '09), Oxford, UK, April 3–7, Elsevier, 3–18.Google Scholar
Hancock, P.G., Ghani, N. and Pattinson, D. (2009). Representations of stream processors using nested fixed points. Logical Methods in Computer Science 5 (3) 17.Google Scholar
Huber, S. (2010). On the computational content of choice axioms. Master's thesis, Mathematisches Institut, LMU.Google Scholar
Huber, S., Karádais, B.A. and Schwichtenberg, H. (2010). Towards a formal theory of computability. In: Ways of Proof Theory (Pohler's Festschrift), Ontos Verlag, 257–282.Google Scholar
Karádais, B.A. (2013). Towards an Arithmetic with Approximations. Ph.D. thesis, Mathematisches Institut, LMU.Google Scholar
Karádais, B.A. (2016). Atomicity, coherence of information, and point-free structures. Annals of Pure and Applied Logic 167 (9) 753–769.Google Scholar
Karádais, B.A. (2018). Normal forms, linearity, and prime algebraicity over nonflat domains. Mathematical Logic Quarterly, to appear.Google Scholar
Kleene, S.C. (1959). Countable functionals. In: Heyting, A. (ed.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam in 1957, Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co, 81–100.Google Scholar
Kreisel, G. (1959). Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (eds.) Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957, Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co, 101–128.Google Scholar
Longley, J. and Normann, D. (2015). Higher-Order Computability, Springer.Google Scholar
Miyamoto, K., Forsberg, F.N. and Schwichtenberg, H. (2013). Program extraction from nested definitions. In: Interactive Theorem Proving – Proceedings of the 4th International Conference (ITP '13), Rennes, France, July 22–26, 370–385.Google Scholar
Miyamoto, K. and Schwichtenberg, H. (2015). Program extraction in exact real arithmetic. Mathematical Structures in Computer Science 25 (8) 1692–1704.Google Scholar
Normann, D. (1981). Countable functionals and the projective hierarchy. Journal of Symbolic Logic 46 209–215.Google Scholar
Normann, D. (1989). Kleene-spaces. In: Logic Colloqium '88, Proceedings of the Colloqium held at Padova/Italy in 1988, Studies in Logic and the Foundations of Mathematics, vol. 127 91–109.Google Scholar
Normann, D. (1996). A hierarchy of domains with totality, but without density. In: Computability, Enumerability, Unsolvability. Directions in Recursion Theory, Cambridge University Press, 233–257.Google Scholar
Normann, D. (1997). Closing the gap between the continuous functionals and recursion in 3E. Archive for Mathematical Logic 36 (4–5) 269–287.Google Scholar
Normann, D. (1999). The continuous functionals. In: Handbook of Computability Theory, Elsevier, 251–275.Google Scholar
Normann, D. (2000a). Computability over the partial continuous functionals. Journal of Symbolic Logic 65 (3) 1133–1142.Google Scholar
Normann, D. (2000b). The Cook–Berger problem. A guide to the solution. In: Proceedings of the Domains IVth Workshop, Haus Humboldtstein, Remagen-Rolandseck, Germany, October 2–4, Elsevier, 9.Google Scholar
Normann, D. (2009). Applications of the Kleene-Kreisel density theorem to theoretical computer science. In: New Computational Paradigms. Changing Conceptions of What is Computable, Springer, 119–138.Google Scholar
Plotkin, G.D. (1978). Tω as a universal domain. Journal of Computer and System Sciences 17 (2) 209–236.Google Scholar
Plotkin, G.D. (1999). Full abstraction, totality and PCF. Mathematical Structures in Computer Science 9 (1) 1–20.Google Scholar
Rinaldi, D. (2014). Formal methods in the theories of rings and domains. Ph.D. thesis, Mathematisches Institut, LMU.Google Scholar
Rutten, J.J.M.M. (2000). Universal coalgebra: A theory of systems. Theoretical Computer Science 249 (1) 3–80.Google Scholar
Sambin, G. (1987). Intuitionistic formal spaces-–A first communication. In Skordev, D. G. (ed.): Mathematical Logic and its Applications (Druzhba, 1986), Plenum, 187–204.Google Scholar
Schwichtenberg, H. (1996). Density and choice for total continuous functionals. In Odifreddi, P. (ed.): Kreiseliana: About and Around Georg Kreisel, A K Peters, 335–362.Google Scholar
Schwichtenberg, H. (2007). Recursion on the partial continuous functionals. In: Dimitracopoulos, C., Newelski, L., Normann, D. and Steel, J. (eds.), Logic Colloquium ('05), Lecture Notes in Logic, vol. 28, Association for Symbolic Logic, 173–201.Google Scholar
Schwichtenberg, H. and Wainer, S.S. (2012). Proofs and Computations, Perspectives in Logic, Cambridge University Press.Google Scholar
Scott, D.S. (1982). Domains for denotational semantics. In: Automata, Languages and Programming (Aarhus, 1982), Lecture Notes in Computer Science, vol. 140, Springer, 577–613.Google Scholar
Stoltenberg-Hansen, V., Lindström, I. and Griffor, E.R. (1994). Mathematical Theory of Domains, Cambridge Tracts in Theoretical Computer Science, vol. 22, Cambridge University Press.Google Scholar
Winskel, G. and Larsen, K.G. (1984). Using information systems to solve recursive domain equations effectively. In Kahn, G., MacQueen, D. B., Plotkin, G. D. (eds.): Semantics of Data Types, Springer-Verlag, 109–129.Google Scholar