Suite définie par récurrence

En mathématiques, une suite définie par récurrence est une suite définie par son (ou ses) premier(s) terme(s) et par une relation de récurrence, qui définit chaque terme à partir du précédent ou des précédents lorsqu'ils existent. Une relation de récurrence est une équation dans laquelle l'expression de plusieurs termes de la suite apparait, par exemple : :u_{n+2} - \sqrt{2 u _{n+3} + u_n} = 0 ou :u_{n^2} = u_n ou :(u_{n+2})^2 - u_n - u_{n+1} = 0 ou si l'on se place dans les suites de mots sur l'alphabet {a, b} : : \alpha_{n+1} = a\alpha_n b b Si la relation de récurrence a une « bonne » présentation, cela permet de calculer l'expression du terme d'indice le plus élevé en fonction de l'expression des autres. Par exemple dans la dernière équation, si l'on admet que les u_n sont des réels positifs, on peut écrire : :u_{n+2} = \sqrt{u _{n+1} + u_n}. Une relation de récurrence et la don

DynaProg for Scala

Thierry Coppey

Dynamic programming is an algorithmic technique to solve problems that follow the Bellman’s principle: optimal solutions depends on optimal sub-problem solutions. The core idea behind dynamic programming is to memoize intermediate results into matrices to avoid multiple computations. Solving a dynamic programming problem consists of two phases: filling one or more matrices with intermediate solutions for sub-problems and recomposing how the final result was constructed (backtracking). In textbooks, problems are usually described in terms of recurrence relations between matrices elements. Expressing dynamic programming problems in terms of recursive formulae involving matrix indices might be difficult, if often error prone, and the notation does not capture the essence of the underlying problem (for example aligning two sequences). Moreover, writing correct and efficient parallel implementation requires different competencies and often a significant amount of time. In this project, we present DynaProg, a language embedded in Scala (DSL) to address dynamic programming problems on heterogeneous platforms. DynaProg allows the programmer to write concise programs based on ADP [1], using a pair of parsing grammar and algebra; these program can then be executed either on CPU or on GPU. We evaluate the performance of our implementation against existing work and our own hand-optimized baseline implementations for both the CPU and GPU versions. Experimental results show that plain Scala has a large overhead and is recommended to be used with small sequences (≤1024) whereas the generated GPU version is comparable with existing implementations: matrix chain multiplication has the same performance as our hand-optimized version (142% of the execution time of [2]) for a sequence of 4096 matrices, Smith-Waterman is twice slower than [3] on a pair of sequences of 6144 elements, and RNA folding is on par with [4] (95% running time) for sequences of 4096 elements. [1] Robert Giegerich and Carsten Meyer. Algebraic Dynamic Programming. [2] Chao-Chin Wu, Jenn-Yang Ke, Heshan Lin and Wu Chun Feng. Optimizing dynamic programming on graphics processing units via adaptive thread-level parallelism. [3] Edans Flavius de O. Sandes, Alba Cristina M. A. de Melo. Smith-Waterman alignment of huge sequences with GPU in linear space. [4] Guillaume Rizk and Dominique Lavenier. GPU accelerated RNA folding algorithm.

2013

Aligator: A mathematica package for invariant generation

Laura Ildiko Kovacs

We describe the new software package Aligator for automatically inferring polynomial loop invariants, The package combines algorithms from symbolic summation and polynomial algebra with computational logic, and is applicable to the rich class of P-solvable loops. Aligator contains routines for checking the P-solvability of loops, transforming them into a system of recurrence equations, solving recurrences and deriving closed forms of loop variables, computing the ideal of polynomial invariants by variable elimination, invariant filtering and completeness check of the resulting set of invariants.

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2008

Finding Loop Invariants for Programs over Arrays Using a Theorem Prover

Laura Ildiko Kovacs

We present a new method for automatic generation of loop invariants for programs containing arrays. Unlike all previously known methods, our method allows one to generate first-order invariants containing alternations of quantifiers. The method is based on the automatic analysis of the so-called update predicates of loops. An update predicate for an array A expresses updates made to A. We observe that many properties of update predicates can be extracted automatically from the loop description and loop properties obtained by other methods such as a simple analysis of counters occurring in the loop, recurrence solving and quantifier elimination over loop variables. We run the theorem prover Vampire on some examples and show that non-trivial loop invariants can be generated.

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa2009

DynaProg for Scala

Thierry Coppey

2013