SearcharxivSearch

arXiv subjects

Scott McCallum

Publications and source records attributed to Scott McCallum.

10 recordsLinked to original sources

Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints

This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present in the given input formula $\phi^*$. The first enhancement provides more detail in the output when there is a conceptual partition of the set of variables of $\phi^*$ into parameters and unknowns. In such cases, we describe how to partition the parameter space so that: (1) in each open set of the partition the number $\nu$ of associated unknowns is a finite constant or is infinite; and (2) for each such open set for which $\nu$ is finite, an expression for the unknowns in terms of the parameters is provided. The second enhancement is an efficiency gain achievable in certain situations. Indeed, when certain conditions are met, the second CAD equational projection step can be reduced more significantly than is supported by the prior existing theory. Relevant theorems and worked examples for both enhancements are provided. Application areas include approximation theory, cuspidal manipulator classification, and biological/chemical systems.

cs.SC

Linear Regression in p-adic metric spaces

Many real-world machine learning problems involve inherently hierarchical data, yet traditional approaches rely on Euclidean metrics that fail to capture the discrete, branching nature of hierarchical relationships. We present a theoretical foundation for machine learning in p-adic metric spaces, which naturally respect hierarchical structure. Our main result proves that an n-dimensional plane minimizing the p-adic sum of distances to points in a dataset must pass through at least n + 1 of those points -- a striking contrast to Euclidean regression that highlights how p-adic metrics better align with the discrete nature of hierarchical data. As a corollary, a polynomial of degree n constructed to minimise the p-adic sum of residuals will pass through at least n + 1 points. As a further corollary, a polynomial of degree n approximating a higher degree polynomial at a finite number of points will yield a difference polynomial that has distinct rational roots. We demonstrate the practical significance of this result through two applications in natural language processing: analyzing hierarchical taxonomies and modeling grammatical morphology. These results suggest that p-adic metrics may be fundamental to properly handling hierarchical data structures in machine learning. In hierarchical data, interpolation between points often makes less sense than selecting actual observed points as representatives.

cs.LG

Iterated Resultants and Rational Functions in Real Quantifier Elimination

This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic. First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport and England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum and Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an unhelpful typo and provide a proof missing from that paper. We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative.

cs.SC

Singularities and Catastrophes in Economics: Historical Perspectives and Future Directions

Economic theory is a mathematically rich field in which there are opportunities for the formal analysis of singularities and catastrophes. This article looks at the historical context of singularities through the work of two eminent Frenchmen around the late 1960s and 1970s. René Thom (1923-2002) was an acclaimed mathematician having received the Fields Medal in 1958, whereas Gérard Debreu (1921-2004) would receive the Nobel Prize in economics in 1983. Both were highly influential within their fields and given the fundamental nature of their work, the potential for cross-fertilisation would seem to be quite promising. This was not to be the case: Debreu knew of Thom's work and cited it in the analysis of his own work, but despite this and other applied mathematicians taking catastrophe theory to economics, the theory never achieved a lasting following and relatively few results were published. This article reviews Debreu's analysis of the so called ${\it regular}$ and ${\it crtitical}$ economies in order to draw some insights into the economic perspective of singularities before moving to how singularities arise naturally in the Nash equilibria of game theory. Finally a modern treatment of stochastic game theory is covered through recent work on the quantal response equilibrium. In this view the Nash equilibrium is to the quantal response equilibrium what deterministic catastrophe theory is to stochastic catastrophe theory, with some caveats regarding when this analogy breaks down discussed at the end.

econ.GN

Validity proof of Lazard's method for CAD construction

In 1994 Lazard proposed an improved method for cylindrical algebraic decomposition (CAD). The method comprised a simplified projection operation together with a generalized cell lifting (that is, stack construction) technique. For the proof of the method's validity Lazard introduced a new notion of valuation of a multivariate polynomial at a point. However a gap in one of the key supporting results for his proof was subsequently noticed. In the present paper we provide a complete validity proof of Lazard's method. Our proof is based on the classical parametrized version of Puiseux's theorem and basic properties of Lazard's valuation. This result is significant because Lazard's method can be applied to any finite family of polynomials, without any assumption on the system of coordinates. It therefore has wider applicability and may be more efficient than other projection and lifting schemes for CAD.

math.AG

Truth Table Invariant Cylindrical Algebraic Decomposition

When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

cs.SC

On Lazard's Valuation and CAD Construction

In 1990 Lazard proposed an improved projection operation for cylindrical algebraic decomposition (CAD). For the proof he introduced a certain notion of valuation of a multivariate Puiseux series at a point. However a gap in one of the key supporting results for the improved projection was subsequently noticed. In this report we study a more limited but rigorous concept of Lazard's valuation: namely, we study Lazard's valuation of a multivariate polynomial at a point. We prove some basic properties of the limited Lazard valuation and identify some relationships between valuation-invariance and order-invariance.

math.AG

A Pilot Study on Coupling CT and MRI through Use of Semiconductor Nanoparticles

CT and MRI are the two most widely used imaging modalities in healthcare, each with its own merits and drawbacks. Combining these techniques in one machine could provide unprecedented resolution and sensitivity in a single scan, and serve as an ideal platform to explore physical coupling of x-ray excitation and magnetic resonance. Molecular probes such as functionalized nanophosphors present an opportunity to demonstrate a synergy between these modalities. However, a simultaneous CT-MRI scanner does not exist at this moment. As a pilot study, here we propose a mechanism in which water solutions containing LiGa5O8:Cr3+ nanophosphors can be excited with x-rays to store energy, and these excited particles may subsequently influence the T2 relaxation times of the solutions so that a difference in T2 can be measured by MRI before and after x-ray excitation. The trends seen in our study suggest that a measurable effect may exist from x-ray excitation of the nanophosphors. However, there are several experimental conditions that hinder the clarity of the results to be statistically significant up to a commonly accepted level (p=0.05), including insoluble nanoparticles and inter-scan variability. Nevertheless, the initial results from our experiments seem a consistent and inspiring story that x-rays modify MRI T2 values around nanophosphors. Upon availability of soluble nanophosphors, we will repeat our experiments to confirm these observations.

physics.med-ph

Cylindrical Algebraic Decompositions for Boolean Combinations

This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.

cs.SC

Quantifier elimination for approximate Beals-Kartashova factorization

The only known constructive factorization algorithm for linear partial differential operators (LPDOs) is Beals-Kartashova (BK) factorization \cite{bk2005}. One of the most interesting features of BK-factorization: at the beginning all the first-order factors are constructed and afterwards the factorization condition(s) should be checked. This leads to the important application area - namely, numerical simulations which could be simplified substantially if instead of computation with one LPDE of order $n$ we will be able to proceed computations with $n$ LPDEs all of order 1. In numerical simulations it is not necessary to fulfill factorization conditions exactly but with some given accuracy, which we call approximate factorization. The idea of the present paper is to look into the feasibility of solving problems of this kind using quantifier elinination by cylindrical algebraic decomposition.

math-ph