BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Alexander Kurz

Alexander Kurz appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer Sciencehep-phmath.CTmath.LOFormal Languages and Automata Theory

Catalog footprint

What is connected

20works
5topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

20 published item(s)

preprint2020arXiv

Logic-Induced Bisimulations

We define a new logic-induced notion of bisimulation (called $ρ$-bisimulation) for coalgebraic modal logics given by a logical connection, and investigate its properties. We show that it is structural in the sense that it is defined only in terms of the coalgebra structure and the one-step modal semantics and, moreover, can be characterised by a form of relation lifting. Furthermore we compare $ρ$-bisimulations to several well-known equivalence notions, and we prove that the collection of bisimulations between two models often forms a complete lattice. The main technical result is a Hennessy-Milner type theorem which states that, under certain conditions, logical equivalence implies $ρ$-bisimilarity. In particular, the latter does \emph{not} rely on a duality between functors $\mathsf{T}$ (the type of the coalgebras) and $\mathsf{L}$ (which gives the logic), nor on properties of the logical connection $ρ$.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Electron contribution to the muon anomalous magnetic moment at four loops

We present results for the QED contributions to the anomalous magnetic moment of the muon containing closed electron loops. The main focus is on perturbative corrections at four-loop order where the external photon couples to the external muon. Furthermore, all four-loop contributions involving simultaneously a closed electron and tau loop are computed. In combination with our recent results on the light-by-light-type corrections (see Ref. \cite{Kurz:2015bia}) the complete four-loop electron-loop contribution to the anomalous magnetic moment of the muon has been obtained with an independent calculation. Our calculation is based on an asymptotic expansion in the ratio of the electron and the muon mass and shows the importance of higher order terms in this ratio. We perform a detailed comparison with results available in the literature and find good numerical agreement. As a by-product we present analytic results for the on-shell muon mass and wave function renormalization constants at three-loop order including massive closed electron and tau loops, which we also calculated using the method of asymptotic expansion.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Multi-type Sequent Calculi

Display calculi are generalized sequent calculi which enjoy a `canonical' cut elimination strategy. That is, their cut elimination is uniformly obtained by verifying the assumptions of a meta-theorem, and is preserved by adding or removing structural rules. In the present paper, we discuss a proof-theoretic setting, inspired both to Belnap's Display Logic and to Sambin's Basic Logic, which generalises these calculi in two directions: by explicitly allowing different types, and by weakening the so-called display and visibility properties. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals, or logics that are not closed under uniform substitution. In the present paper, we give a general overview of the calculi which we refer to as multi-type calculi, and we discuss their canonical cut elimination meta-theorem.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Tool support for reasoning in display calculi

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, that allows us to adapt the tool for a wide variety of user defined calculi.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Light-by-light-type corrections to the muon anomalous magnetic moment at four-loop order

The numerically dominant QED contributions to the anomalous magnetic moment of the muon stem from Feynman diagrams with internal electron loops. We consider such corrections and present a calculation of the four-loop light-by-light-type corrections where the external photon couples to a closed electron or muon loop. We perform an asymptotic expansion in the ratio of electron and muon mass and reduce the resulting integrals to master integrals which we evaluate using analytical and numerical methods. We confirm the results present in the literature which are based on different computational methods.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Hadronic contribution to the muon anomalous magnetic moment to next-to-next-to-leading order

We compute the next-to-next-to-leading order hadronic contribution to the muon anomalous magnetic moment originating from the photon vacuum polarization. The corresponding three-loop kernel functions are calculated using asymptotic expansion techniques which lead to analytic expressions. Our final result, $a_μ^{\rm had,NNLO} = 1.24 \pm 0.01 \times 10^{-10}$, has the same order of magnitude as the current uncertainty of the leading order hadronic contribution and should thus be included in future analyses.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Higher-order hadronic and heavy-lepton contributions to the anomalous magnetic moment

We report about recent results obtained for the muon anomalous magnetic moment. Three-loop kernel functions have been computed to obtain the next-to-next-to-leading-order hadronic vacuum polarization contributions. The numerical result, $a_μ^{\rm{had,NNLO}}=1.24\pm 0.01 \times 10^{-10}$, is of the same order of magnitude as the current uncertainty from the hadronic contributions. For heavy-lepton corrections, analytical results are obtained at four-loop order and compared with the known results.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Simplified Coalgebraic Trace Equivalence

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. LTS. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard LTS and probabilistic labelled transition systems.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Nominal Regular Expressions for Languages over Infinite Alphabets. Extended Abstract

We propose regular expressions to abstractly model and study properties of resource-aware computations. Inspired by nominal techniques -- as those popular in process calculi -- we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Relation lifting, with an application to the many-valued cover modality

We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Completeness for the coalgebraic cover modality

We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, and we employ Pattinson's stratification method, showing that our derivation system can be stratified in countably many layers, corresponding to the modal depth of the formulas involved. In the proof of our main result we identify some new concepts and obtain some auxiliary results of independent interest. We survey properties of the notion of relation lifting, induced by an arbitrary but fixed set functor. We introduce a category of Boolean algebra presentations, and establish an adjunction between it and the category of Boolean algebras. Given the fact that our derivation system involves only formulas of depth one, it can be encoded as a endo-functor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the Lindenbaum-Tarski algebra of our logic can be identified with the initial algebra for this functor.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Relation Liftings on Preorders and Posets

The category Rel(Set) of sets and relations can be described as a category of spans and as the Kleisli category for the powerset monad. A set-functor can be lifted to a functor on Rel(Set) iff it preserves weak pullbacks. We show that these results extend to the enriched setting, if we replace sets by posets or preorders. Preservation of weak pullbacks becomes preservation of exact lax squares. As an application we present Moss's coalgebraic over posets.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Strongly Complete Logics for Coalgebras

Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over ind-completions and extends the theorem of J{ó}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finite-sets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Algebraic Theories over Nominal Sets

We investigate the foundations of a theory of algebraic data types with variable binding inside classical universal algebra. In the first part, a category-theoretic study of monads over the nominal sets of Gabbay and Pitts leads us to introduce new notions of finitary based monads and uniform monads. In a second part we spell out these notions in the language of universal algebra, show how to recover the logics of Gabbay-Mathijssen and Clouston-Pitts, and apply classical results from universal algebra.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

On coalgebras over algebras

We extend Barr's well-known characterization of the final coalgebra of a $Set$-endofunctor as the completion of its initial algebra to the Eilenberg-Moore category of algebras for a $Set$-monad $\mathbf{M}$ for functors arising as liftings. As an application we introduce the notion of commuting pair of endofunctors with respect to the monad $\mathbf{M}$ and show that under reasonable assumptions, the final coalgebra of one of the endofunctors involved can be obtained as the free algebra generated by the initial algebra of the other endofunctor.

0 citations0 reviewsNo code linkedOpen access