scholarly journals Synthesis with Asymptotic Resource Bounds

2021 ◽  
pp. 783-807
Author(s):  
Qinheping Hu ◽  
John Cyphert ◽  
Loris D’Antoni ◽  
Thomas Reps
Keyword(s):  
Recurrence Relations ◽  
Analysis Of Algorithms ◽  
Type System ◽  
Divide And Conquer ◽  
Resource Usage ◽  
Recursive Functions ◽  
Functional Specification ◽  
Synthesis Procedure ◽  
Asymptotic Complexity ◽  
Resource Bound

AbstractWe present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity $$O(n\log (n))$$ O ( n log ( n ) ) .Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, SynPlexity, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.

Classifying Predicates and Languages

1997 ◽  
Vol 08 (01) ◽  
pp. 15-41 ◽  
Author(s):  
Carl H. Smith ◽  
Rolf Wiehagen ◽  
Thomas Zeugmann
Keyword(s):  
Learning Theory ◽  
Classification Problems ◽  
Attention In Learning ◽  
Recursive Functions ◽  
Standard Classification ◽  
Resource Bound ◽  
Multi Classification

The present paper studies a particular collection of classification problems, i.e., the classification of recursive predicates and languages, for arriving at a deeper understanding of what classification really is. In particular, the classification of predicates and languages is compared with the classification of arbitrary recursive functions and with their learnability. The investigation undertaken is refined by introducing classification within a resource bound resulting in a new hierarchy. Furthermore, a formalization of multi-classification is presented and completely characterized in terms of standard classification. Additionally, consistent classification is introduced and compared with both resource bounded classification and standard classification. Finally, the classification of families of languages that have attracted attention in learning theory is studied, too.

scholarly journals Implicit self-adjusting computation for purely functional programs

2014 ◽  
Vol 24 (1) ◽  
pp. 56-112 ◽  
Author(s):  
YAN CHEN ◽  
JOSHUA DUNFIELD ◽  
MATTHEW A. HAMMER ◽  
UMUT A. ACAR
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Source Program ◽  
Target Program ◽  
Implicit Approach ◽  
Asymptotic Complexity ◽  
Cost Semantics ◽  
Output Behavior

AbstractComputational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems, but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create, and operate on data that can change over time. We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well- typed self-adjusting programs and preserves the source program's input–output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.

scholarly journals Exponential bounds and tails for additive random recursive sequences

2007 ◽  
Vol Vol. 9 no. 1 (Analysis of Algorithms) ◽  
Author(s):  
Ludger Rüschendorf ◽  
Eva-Maria Schopp
Keyword(s):  
Analysis Of Algorithms ◽  
Sufficient Conditions ◽  
Random Trees ◽  
Divide And Conquer ◽  
Recursive Sequences ◽  
Recursive Structures ◽  
International Audience ◽  
Exponential Bounds ◽  
The Moment

Analysis of Algorithms International audience Exponential bounds and tail estimates are derived for additive random recursive sequences, which typically arise as functionals of recursive structures, of random trees or in recursive algorithms. In particular they arise as parameters of divide and conquer type algorithms. We derive tail bounds from estimates of the Laplace transforms and of the moment sequences. For the proof we use some classical exponential bounds and some variants of the induction method. The paper generalizes results of Rösler (% \citeyearNPRoesler:91, % \citeyearNPRoesler:92) and % \citeNNeininger:05 on subgaussian tails to more general classes of additive random recursive sequences. It also gives sufficient conditions for tail bounds of the form \exp(-a t^p) which are based on a characterization of \citeNKasahara:78.

Synthesizing Functional Mechanisms From a Link Soup1

2016 ◽  
Vol 138 (6) ◽  
Author(s):  
Pouya Tavousi ◽  
Kazem Kazerounian ◽  
Horea Ilies
Keyword(s):  
Systematic Approach ◽  
Divide And Conquer ◽  
Synthesis Methods ◽  
Mechanism Synthesis ◽  
New Approach ◽  
Positional Analysis ◽  
Systematic Process ◽  
Synthesis Procedure ◽  
Functional Mechanisms ◽  
Classical Mechanism

The synthesis of functional molecular linkages is constrained by difficulties in fabricating nanolinks of arbitrary shapes and sizes. Thus, classical mechanism synthesis methods, which assume the ability to manufacture any designed links, cannot provide a systematic process for assembling such linkages. We propose a new approach to building functional mechanisms with prescribed mobility by using only elements from a predefined “link soup.” First, we enumerate an exhaustive set of topologies, while employing divide-and-conquer algorithms to control the generation and elimination of redundant topologies. Then, we construct the linkage arrangements for each valid topology. Finally, we output a set of feasible geometries through a positional analysis step that minimizes the error associated with closure of the loops in the linkage while avoiding geometric interference. The proposed systematic approach outputs the ATLAS of candidate mechanisms, which can be further processed for downstream applications. The resulting synthesis procedure is the first of its kind that is capable of synthesizing functional linkages with prescribed mobility constructed from a soup of primitive entities.

scholarly journals On rates of convergence in the probabilistic analysis of algorithms

2021 ◽  
Author(s):  
◽  
Jasmin Straub
Keyword(s):  
Normal Limit ◽  
Analysis Of Algorithms ◽  
Rates Of Convergence ◽  
Random Trees ◽  
Divide And Conquer ◽  
Complexity Measures ◽  
Limit Laws ◽  
Contraction Method ◽  
Normal Limits ◽  
Recursive Structures

Within the last thirty years, the contraction method has become an important tool for the distributional analysis of random recursive structures. While it was mainly developed to show weak convergence, the contraction approach can additionally be used to obtain bounds on the rate of convergence in an appropriate metric. Based on ideas of the contraction method, we develop a general framework to bound rates of convergence for sequences of random variables as they mainly arise in the analysis of random trees and divide-and-conquer algorithms. The rates of convergence are bounded in the Zolotarev distances. In essence, we present three different versions of convergence theorems: a general version, an improved version for normal limit laws (providing significantly better bounds in some examples with normal limits) and a third version with a relaxed independence condition. Moreover, concrete applications are given which include parameters of random trees, quantities of stochastic geometry as well as complexity measures of recursive algorithms under either a random input or some randomization within the algorithm.

scholarly journals Analysis of the multiplicity matching parameter in suffix trees

2005 ◽  
Vol DMTCS Proceedings vol. AD,... (Proceedings) ◽  
Author(s):  
Mark Daniel Ward ◽  
Wojciech Szpankowski
Keyword(s):  
Suffix Tree ◽  
Recurrence Relations ◽  
Complex Analysis ◽  
Analysis Of Algorithms ◽  
Suffix Trees ◽  
Logarithmic Series Distribution ◽  
International Audience ◽  
Number Of Leaves ◽  
Branching Point ◽  
Logarithmic Series

International audience In a suffix tree, the multiplicity matching parameter (MMP) $M_n$ is the number of leaves in the subtree rooted at the branching point of the $(n+1)$st insertion. Equivalently, the MMP is the number of pointers into the database in the Lempel-Ziv '77 data compression algorithm. We prove that the MMP asymptotically follows the logarithmic series distribution plus some fluctuations. In the proof we compare the distribution of the MMP in suffix trees to its distribution in tries built over independent strings. Our results are derived by both probabilistic and analytic techniques of the analysis of algorithms. In particular, we utilize combinatorics on words, bivariate generating functions, pattern matching, recurrence relations, analytical poissonization and depoissonization, the Mellin transform, and complex analysis.

scholarly journals A type system for extracting functional specifications from memory-safe imperative programs

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Paul He ◽  
Eddy Westbrook ◽  
Brent Carmer ◽  
Chris Phifer ◽  
Valentin Robert ◽  
...  
Keyword(s):  
Type System ◽  
Functional Language ◽  
Memory Safety ◽  
Type Checking ◽  
Significant Time ◽  
Functional Specification

Verifying imperative programs is hard. A key difficulty is that the specification of what an imperative program does is often intertwined with details about pointers and imperative state. Although there are a number of powerful separation logics that allow the details of imperative state to be captured and managed, these details are complicated and reasoning about them requires significant time and expertise. In this paper, we take a different approach: a memory-safe type system that, as part of type-checking, extracts functional specifications from imperative programs. This disentangles imperative state, which is handled by the type system, from functional specifications, which can be verified without reference to pointers. A key difficulty is that sometimes memory safety depends crucially on the functional specification of a program; e.g., an array index is only memory-safe if the index is in bounds. To handle this case, our specification extraction inserts dynamic checks into the specification. Verification then requires the additional proof that none of these checks fail. However, these checks are in a purely functional language, and so this proof also requires no reasoning about pointers.

Synthesizing Functional Mechanisms From a Link Soup

2015 ◽  
Author(s):  
Pouya Tavousi ◽  
Kazem Kazerounian ◽  
Horea Ilies
Keyword(s):  
Divide And Conquer ◽  
Synthesis Process ◽  
Synthesis Methods ◽  
Mechanism Synthesis ◽  
New Approach ◽  
Positional Analysis ◽  
Synthesis Procedure ◽  
Functional Mechanisms ◽  
Systematic Synthesis ◽  
Classical Mechanism

The synthesis of functional molecular linkages is constrained by difficulties in fabricating nano-links of arbitrary shapes and sizes. However, the classical mechanism synthesis methods, which assume the ability to manufacture any designed links, do not provide a systematic synthesis process for molecular linkages. We propose a new approach to build functional mechanisms with prescribed mobility by only using elements from a predefined link soup. First, we enumerate an exhaustive set of topologies, while employing divide-and-conquer algorithms to control the generation and elimination of redundant topologies. Then, we construct the linkage arrangements for each valid topology. Finally, we output a set of feasible geometries through a positional analysis step that minimizes the error associated with closure of the loops in the linkage while avoiding geometric interference. The proposed systematic approach outputs the ATLAS of candidate mechanisms, which can be further processed for downstream applications. The resulting synthesis procedure is the first of its kind that is capable of synthesizing functional linkages with prescribed mobility constructed from a soup of primitive entities.

Sign in / Sign up

Export Citation Format

Share Document