A decision procedure for linear ``big O equations

DOI10.1007/S10817-007-9066-1zbMATH Open1122.03004arXivcs/0701073OpenAlexW2140507616MaRDI QIDQ2642465FDOQ2642465

Authors: Jeremy Avigad, Kevin Donnelly 

Publication date: 17 August 2007

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

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.

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

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

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)

Cites Work

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

Cited In (5)

• Decidability in elementary analysis. II
• Title not available (Why is that?)
• 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

Uses Software

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

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)