Towards an arithmetic for partial computable functionals

Karadais, Basil A. (2013): Towards an arithmetic for partial computable functionals. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

The thesis concerns itself with nonflat Scott information systems as an appropriate denotational semantics for the proposed theory TCF+, a constructive theory of higher-type partial computable functionals and approximations. We prove a definability theorem for type systems with at most unary constructors via atomic-coherent information systems, and give a simple proof for the density property for arbitrary finitary type systems using coherent information systems. We introduce the notions of token matrices and eigen-neighborhoods, and use them to locate normal forms of neighborhoods, as well as to demonstrate that even nonatomic information systems feature implicit atomicity. We then establish connections between coherent information systems and various pointfree structures. Finally, we introduce a fragment of TCF+ and show that extensionality can be eliminated.

Abstract

Diese Dissertation befasst sich mit nichtflachen Scott-Informationssystemen als geeignete denotationelle Semantik für die vorgestellte Theorie TCF+, eine konstruktive Theorie von partiellen berechenbaren Funktionalen und Approximationen in höheren Typen. Auf Basis von atomisch-kohärenten Informationssystemen wird ein Definierbarkeitssatz für Typsysteme mit höchstens einstelligen Konstruktoren gegeben und ein einfacher Beweis des Dichtheitssatzes von beliebigen finitären Typsystemen auf kohärenten Informationssystemen erbracht. Token-Matrizen und Eigenumgebungen werden eingeführt und verwendet, um Normalformen von Umgebungen aufzufinden und um aufzuzeigen, dass auch nichtatomische Informationssysteme über implizite Atomizität verfügen. Im Anschluss werden Verbindungen zwischen kohärenten Informationssystemen und verschiedenen punktfreien Strukturen geknüpft. Schlussendlich wird ein Fragment von TCF+ vorgestellt und gezeigt, dass Extensionalität umgangen werden kann.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Keywords: atomicity of information, algebras given by constructors, coherence of information, comparability properties, constructive mathematics, definability theorem, denotational semantics, density theorem, domain theory, elimination of extensionality, higher-type computability theory, nonflat domains, normal forms, pointfree topology, Scott information systems, semantics of programming languages
• Themengebiete: 500 Naturwissenschaften und Mathematik ; 500 Naturwissenschaften und Mathematik > 510 Mathematik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 12. August 2013
• 1. Bericht­erstatter:in: Schwichtenberg, Helmut