Basil A. Karádais

Arbeitsgruppe Mathematische Logik

Mathematisches Institut der Universität München
Theresienstr. 39

Email: karadais at math dot lmu dot de

Tel: +49 (0)89 2180 4417
Büro: Block B, 4. Stock, B420

Sprechstunde: nach Vereinbarung

Work

Higher-type computability theory, Denotational semantics of programming languages, Constructive domain theory
(older webpage).

Nonflatness and totality (preprint)
Mathematical Structures in Computer Science, pp. 1–30, 2018. doi:10.1017/S0960129518000026

Abstract. 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 seperation property.
Normal forms, linearity, and prime algebraicity over nonflat domains (preprint)
Mathematical Logic Quarterly, 2018. doi:10.1002/malq.201600020

Abstract. Using representations of nonflat-based Scott domains to model type systems, it is natural to wish that they be "linear", in which case the complexity of the fundamental test for entailment of information drops from exponential to linear, the corresponding mathematical theory becomes much simpler, and moreover has ties to models of computation arising in the study of sequentiality, concurrency, and linear logic. Earlier attempts to develop a fully nonflat semantics based on linear domain representations for a rich enough type system allowing inductive types, were designed in a way that felt rather artificial, as it featured certain awkward and counter-intuitive properties; eventually, the focus turned on general, nonlinear representations.

Here we try to turn this situation around, by showing that we can work linearly in a systematic way within the nonlinear model, and that we may even restrict to a fully linear model whose objects are in a bijective correspondence with the ones of the nonlinear and are easily seen to form a prime algebraic domain. To obtain our results we study mappings of finite approximations of objects that can be used to turn approximations into normal and linear forms.

Outline (talk)
UNIPD 04.02.2015

Slides (talk)
Bridges between financial and constructive mathematics 2015
Atomicity, coherence of information, and point-free structures (preprint)
Annals of Pure and Applied Logic 167, pp. 753–769, 2016

Abstract. We prove basic facts about the properties of atomicity and coherence for Scott information systems, and we establish direct connections between coherent information systems and well-known point-free structures.
Implicit atomicity and finite density for nonflat domains (preprint)
LMU 2013

Note. This work has meanwhile been substantially superseded by more recent work, see "Normal forms, linearity, and prime algebraicity over nonflat domains" and "Nonflatness and totality" above.
Towards an arithmetic for partial computable functionals (phd thesis)
LMU 2013

Abstract. The thesis concerns itself with non-flat Scott information systems as an appropriate denotational semantics for the proposed theory \( \mathrm{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 non-atomic information systems feature implicit atomicity. We then establish connections between coherent information systems and various point-free structures. Finally, we introduce a fragment of \( \mathrm{TCF}^+ \) and show that extensionality can be eliminated.

Outline of the defense talk (talk)
LMU 12.08.2013
Atomicity in non-atomic information systems (talk)
Foundation of mathematics for computer-aided formalization 2013
Recognizing tokens in a finitary algebra (unpublished) (a theorem of Schröter, Gerneth & Hall)
LMU 2012

Abstract. I describe here a technique of recognizing in linear time trees over a free algebra given by constructors. The technique is arithmetical rather than automata theoretic, in that it depends on the arities of the constructors rather than on their names.

Note. The main observation in the text (Proposition, p. 3) is Theorem 2.3, part III, in P. M. Cohn's Universal algebra (1981), or Theorem 1 in Chapter IV, Section 1, in C. Rosenbloom's Elements of mathematical logic (1950).

Following the references in these textbooks, we find that the idea was already known in the early 30's. Karl Menger ("Eine elementare Bemerkung über die Struktur logischer Formeln", Ergebnisse eines mathematischen Kolloquiums, vol. 3, 1930/31, pp. 22–3) had it in the context of Łukasiewicz' prefix notation for the propositional calculus (also called "polish notation"), for the case of an alphabet with unary and binary constructors—the intuition stemming from the negation and the logical connectives respectively. He thus derived a necessary and sufficient condition for a string to be a well-formed formula. Rosenbloom informs us that the same observation was independently made by Kazimierz Ajdukiewicz as well.

Karl Schröter ("Axiomatisierung der Fregeschen Aussagenkalküle", Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, neue Folge, Heft 8, 1943) discusses the case of arbitrary arities, as does Dal Charles Gerneth later, independently ("Generalization of Menger's result on the structure of logical formulas", Bulletin of the American Mathematical Society, vol. 54, 1948, pp. 803–804). Rosenbloom again informs us that Philip Hall, also independently, had made the same general observation; indeed, Hall talks about this "paradox of the pointlessness of punctuation" several years later, in his fairly well-known address to the London Mathematical Society ("Some word-problems", Journal of the London Mathematical Society, second series, vol. 33, 1958, pp. 482–496).

One can only admire the wonderful robustness of mathematical activity...

Many-many thanks to Magnus Steinby, who kindly referred me to Cohn's book seven months ago in January 2014. I've been meaning to update the text and pay the necessary dues all this time, but...
Towards a formal theory of computability (preprint), with S. Huber and H. Schwichtenberg
Ways of proof theory (Pohler's festschrift), Ontos Mathematical Logic 2, pp. 257–282, 2010

Abstract. We sketch a constructive formal theory \( \mathrm{TCF}^+ \) of computable functionals, based on the partial continuous functionals as their intended domain. Such a task had long ago been started by Dana Scott under the well-known abbreviation \( \mathrm{LCF} \) (logic of computable functionals). The present approach differs from Scott's in two aspects.

(i) The intended semantical domains for the base types are non-flat free algebras, given by their constructors, where the latter are injective and have disjoint ranges; both properties do not hold in the flat case.

(ii) \(\mathrm{TCF}^+ \) has the facility to argue not only about the functionals themselves, but also about their finite approximations.

In this setting we give an informal proof (based on [Berger 1993]) of Kreisel's density theorem and an adaption of Plotkin's definability theorem. We then show that both proofs can be formalized in \( \mathrm{TCF}^+ \).

A case study (talk)
Arbeitstagung Bern–Munchen 2010
Plotkin definability theorem for atomic-coherent information systems (talk)
Computability in Europe 2008
Normal form of finite algebraic approximations (talk)
Seminar on proof theory WS 2006/7
Elaborating on Ishihara's 'WKL implies FAN' (talk)
EST training workshop 2005

Abstract. In 1990 Hajime Ishihara proved indirectly that the weak König's lemma implies the fan theorem. Here we reproduce a direct proof Ishihara provided for the same implication, which he presented in 2004 in Munich. This is a work done within a coordinated attempt of the Mathematical Logic Group in Munich to formalize Ishihara's arguments in theorem proving environments, an aim which was met in late spring by Stefan Schimanski on Coq and Nikolaus Thiel on Minlog.