Achim Jung

CSL Conference 2017 Conference Paper

Diagrammatic Semantics for Digital Circuits

• Dan R. Ghica
• Achim Jung
• Aliaume Lopez

We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.

TCS Journal 2015 Journal Article

All cartesian closed categories of quasicontinuous domains consist of domains

• Xiaodong Jia
• Achim Jung
• Hui Kou
• Qingguo Li
• Haoran Zhao

Quasicontinuity is a generalisation of Scott's notion of continuous domain, introduced in the early 80s by Gierz, Lawson and Stralka. In this paper we ask which cartesian closed full subcategories exist in qCONT, the category of all quasicontinuous domains and Scott-continuous functions. The surprising, and perhaps disappointing, answer turns out to be that all such subcategories consist entirely of continuous domains. In other words, there are no new cartesian closed full subcategories in qCONT beyond those already known to exist in CONT. To prove this, we reduce the notion of meet-continuity for dcpos to one which only involves well-ordered chains. This allows us to characterise meet-continuity by “forbidden substructures”. We then show that each forbidden substructure has a non-quasicontinuous function space.

TCS Journal 2013 Journal Article

Convergence of preference functions

• Achim Jung
• Jonathan E. Rowe

A preference function is a function which selects a subset of objects based on (partial) information. As information increases, different objects may be selected. We examine conditions under which the selection of objects converges to the choice that would be made if full information were available, making use of tools from domain theory. The work is motivated by previous research on co-evolutionary algorithms in which an evolving population of agents interact with each other and, it is hoped, produce better and better quality behaviour. The formalisation of how quality can be measured in this context has introduced the concept of a convex preference function (or “solution concept”). We simplify and extend the scope of this previous work, examining the relationship between convexity and convergence properties.

TCS Journal 2006 Journal Article

A logical approach to stable domains

• Yi-Xiang Chen
• Achim Jung

Building on earlier work by Guo-Qiang Zhang on disjunctive information systems, and by Thomas Ehrhard, Pasquale Malacaria, and the first author on stable Stone duality, we develop a framework of disjunctive propositional logic in which theories correspond to algebraic L-domains. Disjunctions in the logic can be indexed by arbitrary sets (as in geometric logic) but must be provably disjoint. This raises several technical issues which have to be addressed before clean notions of axiom system and theory can be defined. We show soundness and completeness of the proof system with respect to distributive disjunctive semilattices, and prove that every such semilattice arises as the Lindenbaum algebra of a disjunctive theory. Via stable Stone duality, we show how to use disjunctive propositional logic for a logical description of algebraic L-domains.

TCS Journal 2004 Journal Article

Preface

• Lars Birkedal
• Martín Escardó
• Achim Jung
• Giuseppe Rosolini

TCS Journal 2004 Journal Article

The probabilistic powerdomain for stably compact spaces

• Mauricio Alvarez-Manilla
• Achim Jung
• Klaus Keimel

This paper reviews the one-to-one correspondence between stably compact spaces (a topological concept covering most classes of semantic domains) and compact ordered Hausdorff spaces. The correspondence is extended to certain classes of real-valued functions on these spaces. This is the basis for transferring methods and results from functional analysis to the non-Hausdorff setting. As an application of this, the Riesz Representation Theorem is used for a straightforward proof of the (known) fact that every valuation on a stably compact space extends uniquely to a Radon measure on the Borel algebra of the corresponding compact Hausdorff space. The view of valuations and measures as certain linear functionals on function spaces suggests considering a weak topology for the space of all valuations. If these are restricted to the probabilistic or sub-probabilistic case, then another stably compact space is obtained. The corresponding compact ordered space can be viewed as the set of (probability or sub-probability) measures together with their natural weak topology.

CSL Conference 2002 Conference Paper

A Logic for Probabilities in Semantics

• M. Andrew Moshier
• Achim Jung

Abstract Probabilistic computation has proven to be a challenging and interesting area of research, both from the theoretical perspective of denotational semantics and the practical perspective of reasoning about probabilistic algorithms. On the theoretical side, the probabilistic powerdomain of Jones and Plotkin represents a significant advance. Further work, especially by Alvarez-Manilla, has greatly improved our understanding of the probabilistic powerdomain, and has helped clarify its relation to classical measure and integration theory. On the practical side, such researchers as Kozen, Segala, Desharnais, and Kwiatkowska, among others, study problems of verification for probabilistic computation by defining various suitable logics for the classes of processes under study. The work reported here begins to bridge the gap between the domain theoretic and verification (model checking) perspectives on probabilistic computation by exhibiting sound and complete logics for probabilistic powerdomains that arise directly from given logics for the underlying domains.

TCS Journal 1991 Journal Article

The dependent product construction in various categories of domains

• Achim Jung

TCS Journal 1991 Journal Article

Using powerdomains to generalize relational databases

• Peter Buneman
• Achim Jung
• Atsushi Ohori

Much of relational algebra and the underlying principles of relational database design have a simple representation in the theory of domains that is traditionally used in the denotational semantics of programming languages. By investigating the possible orderings on powerdomains that are well known in the study of nondeterminism and concurrency it is possible to show that many of the ideas in relational databases apply to structures that are much more general than relations. This also suggests a method of representing database objects as typed objects in programming languages. In this paper we show how operations such as natural join and projection—which are fundamental to relational database design—can be generalized, and we use this generalized framework to give characterizations of several relational database concepts including functional dependencies and universal relations. All of these have a simple-minded semantics in terms of the underlying domains, which can be thought of as domains of partial descriptions of “real-world” objects. We also discuss the applicability of relational database theory to nonrelational structures such as records with variants, higher-order relations, recursive structures and other ordered spaces.

TCS Journal 1990 Journal Article

Cartesian closed categories of algebraic CPOs

• Achim Jung

The results presented in this paper were inspired by the work of Smyth, who showed that there is a largest cartesian closed full subcategory inside the category of countably based algebraic cpos with least element, namely the category of profinite domains. Removing the countability condition, we show that there are exactly two maximal cartesian closed full subcategories inside the category of algebraic cpos with least element. One is the natural extension of the class of profinite domains to the uncountable case, the other is a new class of domains, which are characterized by the property that every principal ideal is a complete lattice. The name L-domain is introduced for cpos with this property. Passing to the general situation where no least element is required anymore, we find a pair of categories in place of each the profinite domains and the algebraic L-domains. Thus there are four maximal cartesian closed categories of algebraic cpos in this case. This complete overview over the possible classes of domains allows to prove general theorems about them. This is illustrated by the result that a cpo has an algebraic function space if and only if its space of strict continuous functions is algebraic.