arXiv subjects

Michael Benedikt

Publications and source records attributed to Michael Benedikt.

At least 37 records · Page 2Linked to original sources

arXiv2024

Embedded Finite Models Beyond Restricted Quantifier Collapse

We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as an interpreted vocabulary over an infinite domain. This formalism was denoted embedded finite model theory in the past. It is clear that the expressiveness and evaluating complexity of formulas of this type depends heavily on the infinite structure. If we embed in a wild structure like the integers with additive and multiplicative arithmetic, logic is extremely expressive and formulas are impossible to evaluate. On the other hand, for some well-known decidable structures, the expressiveness and evaluating complexity are similar to the situation without the additional infrastructure. The latter phenomenon was formalized via the notion of ``Restricted Quantifier Collapse'': adding quantification over the infinite structure does not add expressiveness. Beyond these two extremes little was known. In this work we show that the possibilities for expressiveness and complexity are much wider. We show that we can get almost any possible complexity of evaluation while staying within a decidable structure. We also show that in some decidable structures, there is a disconnect between expressiveness of the logic and complexity, in that we cannot eliminate quantification over the structure, but this is not due to an ability to embed complex relational computation in the logic. We show failure of collapse for the theory of finite fields and the related theory of pseudo-finite fields, which will involve coding computation in the logic. As a by-product of this, we establish new lower-bounds for the complexity of decision procedures for several decidable theories of fields, including the theory of finite fields. In the process of investigating this landscape, we investigate several weakenings of collapse.

cs.LO↗

arXiv2024

Two variable logic with ultimately periodic counting

We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the ``biregular graph method''. In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

cs.LO↗

arXiv2023

Towards Unbiased Exploration in Partial Label Learning

We consider learning a probabilistic classifier from partially-labelled supervision (inputs denoted with multiple possibilities) using standard neural architectures with a softmax as the final layer. We identify a bias phenomenon that can arise from the softmax layer in even simple architectures that prevents proper exploration of alternative options, making the dynamics of gradient descent overly sensitive to initialisation. We introduce a novel loss function that allows for unbiased exploration within the space of alternative outputs. We give a theoretical justification for our loss function, and provide an extensive evaluation of its impact on synthetic data, on standard partially labelled benchmarks and on a contributed novel benchmark related to an existing rule learning challenge.

cs.LG↗

arXiv2022

Rewriting the Infinite Chase

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase - a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where GTGDs are transformed to a Datalog program that entails the same base facts on each base instance. We show that the rewriting can be seen as containing "shortcut" rules that circumvent certain chase steps, we present several algorithms that compute the rewriting by simulating specific types of chase steps, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

cs.LO↗

arXiv2022

Synthesizing Nested Relational Queries from Implicit Specifications

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset $O$ in terms of datasets $\vec{I}$) is a logical specification involving the source data $\vec{I}$ and the interface data $O$. It is a valid definition of $O$ in terms of $\vec{I}$, if any two models of the specification agreeing on $\vec{I}$ agree on $O$. In contrast, an explicit definition is a query that produces $O$ from $\vec{I}$. Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous effective implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be effectively converted to explicit definitions in the nested relational calculus NRC. As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.

cs.DB↗

arXiv2022

When Can We Answer Queries Using Result-Bounded Data Interfaces?

We consider answering queries on data available through access methods, that provide lookup access to the tuples matching a given binding. Such interfaces are common on the Web; further, they often have bounds on how many results they can return, e.g., because of pagination or rate limits. We thus study result-bounded methods, which may return only a limited number of tuples. We study how to decide if a query is answerable using result-bounded methods, i.e., how to compute a plan that returns all answers to the query using the methods, assuming that the underlying data satisfies some integrity constraints. We first show how to reduce answerability to a query containment problem with constraints. Second, we show "schema simplification" theorems describing when and how result-bounded services can be used. Finally, we use these theorems to give decidability and complexity results about answerability for common constraint classes.

cs.LO↗

arXiv2022

Query Answering with Transitive and Linear-Ordered Data

We consider entailment problems involving powerful constraint languages such as frontier-guarded existential rules in which we impose additional semantic restrictions on a set of distinguished relations. We consider restricting a relation to be transitive, restricting a relation to be the transitive closure of another relation, and restricting a relation to be a linear order. We give some natural variants of guardedness that allow inference to be decidable in each case, and isolate the complexity of the corresponding decision problems. Finally we show that slight changes in these conditions lead to undecidability.

cs.LO↗

arXiv2021

Challenges for the interaction region design of the Future Circular Collider FCC-ee

The FCC-ee is a proposed future high-energy, high-intensity and high-precision lepton collider. Here, we present the latest development for the FCC-ee interaction regions, which shall ensure optimum conditions for the particle physics experiments. We discuss measures of background reduction and a revised interaction region layout including a low impedance compact beam chamber design. We also discuss the possible impact of the radiation generated in the interaction region including beamstrahlung.

physics.acc-ph↗

arXiv2020

Reasoning about disclosure in data integration in the presence of source constraints

Data integration systems allow users to access data sitting in multiple sources by means of queries over a global schema, related to the sources via mappings. Data sources often contain sensitive information, and thus an analysis is needed to verify that a schema satisfies a privacy policy, given as a set of queries whose answers should not be accessible to users. Such an analysis should take into account not only knowledge that an attacker may have about the mappings, but also what they may know about the semantics of the sources. In this paper, we show that source constraints can have a dramatic impact on disclosure analysis. We study the problem of determining whether a given data integration system discloses a source query to an attacker in the presence of constraints, providing both lower and upper bounds on source-aware disclosure analysis.

cs.LO↗

arXiv2020

Scalable Querying of Nested Data

While large-scale distributed data processing platforms have become an attractive target for query processing, these systems are problematic for applications that deal with nested collections. Programmers are forced either to perform non-trivial translations of collection programs or to employ automated flattening procedures, both of which lead to performance problems. These challenges only worsen for nested collections with skewed cardinalities, where both handcrafted rewriting and automated flattening are unable to enforce load balancing across partitions. In this work, we propose a framework that translates a program manipulating nested collections into a set of semantically equivalent shredded queries that can be efficiently evaluated. The framework employs a combination of query compilation techniques, an efficient data representation for nested collections, and automated skew-handling. We provide an extensive experimental evaluation, demonstrating significant improvements provided by the framework in diverse scenarios for nested collection programs.

cs.DB↗

arXiv2020

Generating collection transformations from proofs

Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets. In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig's interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them. We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.

cs.LO↗

arXiv2020

FCC-hh Experimental Insertion Region Design

The Future Circular Collider study is exploring possible designs of circular colliders for the post-LHC era, as recommended by the European Strategy Group for High Energy Physics. One such option is FCC-hh, a proton-proton collider with a centre-of-mass energy of 100 TeV. The experimental insertion regions are key areas defining the performance of the collider. This paper presents the first insertion region designs with a complete assessment of the main challenges, as collision debris with two orders of magnitude larger power than current colliders, beam-beam interactions in long insertions, dynamic aperture for optics with peak $β$ functions one order of magnitude above current colliders, photon background from synchrotron radiation and cross talk between the insertion regions. An alternative design avoiding the use of crab cavities with a small impact on performance is also presented.

physics.acc-ph↗

arXiv2020

Balancing expressiveness and inexpressiveness in view design

We study the design of data publishing mechanisms that allow a collection of autonomous distributed datasources to collaborate to support queries. A common mechanism for data publishing is via views: functions that expose derived data to users, usually specified as declarative queries. Our autonomy assumption is that the views must be on individual sources, but with the intention of supporting integrated queries. In deciding what data to expose to users, two considerations must be balanced. The views must be sufficiently expressive to support queries that users want to ask -- the utility of the publishing mechanism. But there may also be some expressiveness restriction. Here we consider two restrictions, a minimal information requirement, saying that the views should reveal as little as possible while supporting the utility query, and a non-disclosure requirement, formalizing the need to prevent external users from computing information that data owners do not want revealed. We investigate the problem of designing views that satisfy both an expressiveness and an inexpressiveness requirement, for views in a restricted declarative language (conjunctive queries), and for arbitrary views.

cs.LO↗

arXiv2020

Some Model Theory of Guarded Negation

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. This version of the paper contains streamlined and corrected versions of results concerning entailment of a conjunctive query from a set of ground facts and a theory consisting of GNFO sentences of a special form ("dependencies").

cs.LO↗

arXiv2020

On monotonic determinacy and rewritability for recursive queries and views

A query Q is monotonically determined over a set of views if Q can be expressed as a monotonic function of the view image. In the case of relational algebra views and queries, monotonic determinacy coincides with rewritability as a union of conjunctive queries, and it is decidable in important special cases, such as for CQ views and queries. We investigate the situation for views and queries in the recursive query language Datalog. We give both positive and negative results about the ability to decide monotonic determinacy, and also about the co-incidence of monotonic determinacy with Datalog rewritability.

cs.LO↗

arXiv2020

Finite Open-World Query Answering with Number Restrictions

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study finite open-world query answering (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies; and the guarded fragment with number restrictions but on a signature of arity only two. In this paper, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: we show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies. Our result relies on new techniques to construct finite universal models of such constraints, for any bound on the maximal query size.

cs.LO↗

arXiv2019

Polarization and Centre-of-mass Energy Calibration at FCC-ee

The first stage of the FCC (Future Circular Collider) is a high-luminosity electron-positron collider (FCC-ee) with centre-of-mass energy ranging from 88 to 365 GeV, to study with high precision the Z, W, Higgs and top particles, with samples of $5 \times 10^{12}$ Z bosons, $10^8$ W pairs, $10^6$ Higgs bosons and $10^6$ top quark pairs. A cornerstone of the physics program lays in the precise (ppm) measurements of the W and Z masses and widths, as well as forward-backward asymmetries. To this effect the centre-of-mass energy distribution should be determined with the high precision. This document describes the capacity offered by FCC-ee, starting with transverse polarization of the beams around the Z pole and the W pair threshold. A running scheme based on regular measurements of the beam energy by resonant depolarization of pilot bunches, during physics data taking, is proposed. The design for polarization wigglers, polarimeter and depolarizer is outlined. The $e^\pm$ beam energies will be monitored with a relative precision of $10^{-6}$. The centre-of-mass energy is derived subject to further corrections, related to the beam acceleration, synchrotron radiation and beamstrahlung; these effects are identified and evaluated. Dimuon events $e^+e^- \to μ^+ μ^-$, recorded in the detectors, provide with great precision the beam crossing angle, the centre-of-mass energy spread, and the $e^+$ and $e^-$ energy difference. Monitoring methods to minimize absolute error and relative uncertainties are discussed. The impact on the physics measurements is given. A programme of further simulations, design, monitoring and R&D is outlined.

physics.acc-ph↗

arXiv2019

Definability and Interpolation within Decidable Fixpoint Logics

We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back and forth between relational logics and logics over trees.

cs.LO↗