A decision procedure for linear ``big O equations

DOI10.1007/S10817-007-9066-1MaRDI QIDQ2642465zbMATH OpenOpenAlexFDO

Authors Jeremy Avigad, Kevin Donnelly

Publication date 17 August 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0701073

zbMATH Keywords

Asymptotic equationsDecision proceduresBig O

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Abstract: Let $F$ be the set of functions from an infinite set, $S$, to an ordered ring, $R$. For $f$, $g$, and $h$ in $F$, the assertion $f=g+O(h)$ means that for some constant $C$, $|f(x)-g(x)|leqC|h(x)|$ for every $x$ in $S$. Let $L$ be the first-order language with variables ranging over such functions, symbols for $0,+,-,min,max$, and absolute value, and a ternary relation $f=g+O(h)$. We show that the set of quantifier-free formulas in this language that are valid in the intended class of interpretations is decidable, and does not depend on the underlying set, $S$, or the ordered ring, $R$. If $R$ is a subfield of the real numbers, we can add a constant 1 function, as well as multiplication by constants from any computable subfield. We obtain further decidability results for certain situations in which one adds symbols denoting the elements of a fixed sequence of functions of strictly increasing rates of growth.

Recommendations

• scientific article; zbMATH DE number 139625
• scientific article; zbMATH DE number 4215257
• scientific article; zbMATH DE number 437553
• On Linear-Time Deterministic Algorithms for Optimization Problems in Fixed Dimension
• Complexity of linear problems with a fixed output basis
• scientific article; zbMATH DE number 19091
• scientific article; zbMATH DE number 898014
• Upper bounds on the complexity of solving systems of linear equations
• An O(n log n)-algorithm for solving a special class of linear programs
• Analysis of the binary complexity of asymptotically fast algorithms for linear system solving

Cites work

• scientific article; zbMATH DE number 3943824 (Why is no real title available?)
• scientific article; zbMATH DE number 1219584 (Why is no real title available?)
• scientific article; zbMATH DE number 718142 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A formally verified proof of the prime number theorem
• A new polynomial-time algorithm for linear programming
• Applying Linear Quantifier Elimination
• Automated Reasoning
• Combining decision procedures for the reals
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Principles of Constraint Programming
• The complexity of linear problems in fields

Cited in

(5)

• Decidability in elementary analysis. II
• scientific article; zbMATH DE number 3965440 (Why is no real title available?)
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Minimal characterization of O-notation in algorithm analysis
• A general definition of the \(O\)-notation for algorithm analysis

Describes a project that uses

Uses Software

• HOL
• PVS
• Isabelle/HOL
• ML
• Coq

This page was built for publication: A decision procedure for linear ``big O equations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2642465)