Related papers: A Formalization of Polytime Functions

Bellantoni and Cook have given a function-algebra characterization of the polynomial-time computable functions via an unbounded recursion scheme which is called safe recursion. Inspired by their work, we characterize the exponential-time…

Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have…

We examine two different ways of encoding a counting function, as a rational generating function and explicitly as a function (defined piecewise using the greatest integer function). We prove that, if the degree and number of input…

This paper introduces a more restrictive notion of feasibility of functionals on Baire space than the established one from second-order complexity theory. Thereby making it possible to consider functions on the natural numbers as running…

Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library…

An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and…

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying…

A famous result due to Ko and Friedman (1982) asserts that the problems of integration and maximisation of a univariate real function are computationally hard in a well-defined sense. Yet, both functionals are routinely computed at great…

Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can…

We exhibit a sound and complete implicit-complexity formalism for functions feasibly computable by structural recursions over inductively defined data structures. Feasibly computable here means that the structural-recursive definition runs…

The existence of string functions, which are not polynomial time computable, but whose graph is checkable in polynomial time, is a basic assumption in cryptography. We prove that in the framework of algebraic complexity, there are no such…

Kawamura and Cook specified the least set of information about a continuous function on the unit interval which is needed for fast function evaluation. This paper presents a variation of their result. To make the above statement precise,…

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying…

For the implementations of controllers on digital processors, certain limitations, e.g. in the instruction set and register length, need to be taken into account, especially for safety-critical applications. This work aims to provide a…

We prove a complexity dichotomy for Holant problems on the boolean domain with arbitrary sets of real-valued constraint functions. These constraint functions need not be symmetric nor do we assume any auxiliary functions as in previous…

We present polygraphic programs, a subclass of Albert Burroni's polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic…

We prove a characterization of the dual mixed volume in terms of functional properties of the polynomial associated to it. To do this, we use tools from the theory of multilinear operators on spaces of continuos functions. Along the way we…

Partition functions, also known as homomorphism functions, form a rich family of graph invariants that contain combinatorial invariants such as the number of k-colourings or the number of independent sets of a graph and also the partition…

We extend the framework for complexity of operators in analysis devised by Kawamura and Cook (2012) to allow for the treatment of a wider class of representations. The main novelty is to endow represented spaces of interest with an…

Given a function from $\mathbb{Z}_n$ to itself one can determine its polynomial representability by using Kempner function. In this paper we present an alternative characterization of polynomial functions over $\mathbb{Z}_n$ by constructing…