Topological Characterization of Gurevich Modelization of Sequential Algorithms
Serge Grigorieff (LIAFA, Paris 7) and Pierre Valarcher.
Soumis à ICALP (2011)
Sequential algorithms over countable data structures are modelized by Gurevich’s Abstract State Machines as the iteration of a functional which goes from a finite product of function spaces into itself. ASM functionals have the following properties for some k: (1)_k they modify their argument on at most k points, (2)_k their modulus of continuity is k-bounded. We show that these properties characterize ASM functionals and that property (2)_k^2 then holds with a modulus of continuity given by ground terms. This k -> k^2 blow-up is optimal. We also give a topological interpretation of property (2) in terms of uniform continuity. The effective version also holds but is harder to prove and involves a super-exponential blow-up due to the use of Ramsey’s theorem.
A theorem of representation for primitive recursive algorithms
Philippe Andary, Bruno Patrou (LITIS, Rouen) and Pierre Valarcher.
Fondamenta Informaticae (2011)
We plan to formalize the set of algorithms computing elements of the set of primitive recursive functions (PR) as the set of abstract state machines (ASMs) which have their running lengths computable by PR functions. Then we show that there exists a programming language (only com- puting PR functions) which implements any previously defined algorithm preserving complexity.
Habilitation à Diriger des Recherches
Document et Transparents (2010)
Evolving Multialgebras unify all kinds of sequential computation models
Serge Grigorieff (LIAFA, Paris 7) and Pierre Valarcher.
STACS (2010)
It is well-known that Abstract State Machines (ASMs) can simulate “step by step” any type of machines (Turing machines, RAMs, etc.). We aim to overcome two facts: 1) simulation is not identification, 2) the ASMs simulating machines of some type do not constitute a natural class among all ASMs.
We modify Gurevich’s notion of ASM to that of LEA (“Local Evolving Algebra”) by replacing the program (which is a syntactic object) by a semantic object: a functional which has to be very simply definable over the static part of the ASM. We prove that very natural classes of LEAs correspond via literal identifications to slight extensions of the usual machine models and also to grammar models. Though we modify these models, we keep their computation approach: only some contingencies are modified.
Thus, LEAs appear as the mathematical model unifying all kinds of sequential computation paradigms.
B-ASM: Specification of ASM à la B
David Michel, Frédéric Gervais, and Pierre Valarcher.
ABZ2010 (2010)
We try to recover the proof correctness strength of the B method and the smartness of the Abstract State Machine model (ASM) by constructing a B-ASM language. The language inherits from the lan- guage of substitution and from ASM program. The process of refinement leads us to a program expressed in the ASM syntax only. As each step of refinement is correct towards the specification, we obtain an ASM that is proved to be correct towards the specification.
A total functional programming language that computes Primitive Recursive Algorithms
David Michel and Pierre Valarcher.
Special issues of Weak Arithmetics Day (CSLI) (2009)
We recall the definition of the class of primitive recursive algorithms (APRA) and we prove that there exists a functional programming language (primitive recursion with variable parameters or fragment of system T 1 of Gœdel) that simulates all algorithms of APRA in lock-step. The class APRA is a large class of algorithms defined from abstract state machine (ASM) of Y. Gurevich. The functional language admits a mixed-reduction strategy to be efficient and the simulation through an intermediate language with a bounded-conditional loop.
Extending the loop language with higher-order procedural variables.
Tristan Crolard, Emmanuel Polonovsky and Pierre Valarcher.
ACM Transactions on Computational Logic (Volume 10 - Number 4) ()2009)
We plan to formalize the set of algorithms computing elements of the set of primitive recursive functions (PR) as the set of abstract state machines (ASMs) which have their running lengths computable by PR functions. Then we show that there exists a programming language (only com- puting PR functions) which implements any previously defined algorithm preserving complexity.
A complete characterization of primitive recursive intensional behaviours
Pierre Valarcher.
RAIRO Theoretical Informatics and Applications (2008)
We give a complete characterization of the class of functions that are the intensional behaviours of Primitive Recursive algorithms. This class is the set of primitive recursive functions that have a null basic case of recursion. This result is obtained using the property of ultimate unarity and a geometrical approach of sequential functions on N the set of positive integers.
Mahler’s expansion and boolean functions
Jean-Francis Michon (LITIS, Rouen), Pierre Valarcher and Jean-Baptiste Yunès (LIAFA, Paris 7).
Journal of Integer Sequences (Volume 10) (2007)
The substitution of X by X2 in the binomial polynomials generates sequences of integers by Mahler’s expansion. We give some properties of these integers and a combinatorial interpretation with covers by pro- jection. Applications to boolean functions classification are given. This sequence arose from our previous research on classification and complexity of Binary Decision Diagrams (BDD) attached to boolean functions.
On the expressive power of Loop language
Tristan Crolard, Samuel Lacas and Pierre Valarcher.
Nordic Journal of Computing (Volume 13) (2006)
We define a translation of Meyer and Ritchie’s Loop language into a subsystem of Godel’s system T (with product types). Then we show that this translation actually provides a lock-step simulation if a call-by-value strategy is assumed for system T. Some generalizations and possible applications are discussed.
On maximal QROBDD’s boolean functions
Jean-Francis Michon (LITIS, Rouen), Pierre Valarcher and Jean-Baptiste Yunès (LIAFA, Paris 7).
RAIRO - Theoretical Informatics and Applications, 39 (2005)
We investigate the structure of “worst-case” quasi reduced ordered decision diagrams and boolean functions whose truth tables are associated to: we suggest different ways to count and enumerate them. We, then, introduce a notion of complexity which leads to the concept of “hard” boolean functions as functions whose QROBDD are “worst-case” ones. So we exhibit the relation between hard functions and the Storage Access function (also known as Multiplexer).
HFE and BDDs : A practical attempt at cryptanalysis
Jean-Francis Michon (LITIS, Rouen), Pierre Valarcher and Jean-Baptiste Yunès (LIAFA, Paris 7).
Progress in Computer Science and Applied Logic (2003)
HFE (Hidden Field Equations) is a public key cryptosystem using univariate polynomials over finite fields. It was proposed by J. Patarin in 1996. Well chosen parameters during the construction produce a system of quadratic multivariate polynomials over F2 as the public key. An enclosed trapdoor is used to decrypt messages. We propose a ciphertext-only attack which mainly consists in satisfying a boolean formula. Our algorithm is based on BDDs (Binary Decision Diagrams), introduced by Bryant in 1986, which allow to represent and manipulate, possibly efficiently, boolean functions. This paper is devoted to some experimental results we obtained while trying to solve the Patarin’s challenge. This approach was not successful, nevertheless it provided some interesting information about the security of HFE cryptosystem.
About implementation of primitive recursive algorithms
Philippe Andary, Bruno Patrou (LITIS, Rouen) and Pierre Valarcher.
Proceedings of the 12th International Workshop on Abstract State Machines (2005)
On the expressive power of loop language
Tristan Crolard, Samuel Lacas and Pierre Valarcher.
17th Nordic workshop on Programming Theory, Copenhague (2005)
Call-by-value and call-by-name in primitive recursion : storage operator
Pierre Valarcher.
5th International Workshop on Reduction Strategies in Rewriting and Programming, Nara (Japon) (2005)
Analysis of HFE from BDD point of view
J.F. Michon (LITIS), P. Valarcher and J.-B. Yunès (LIAFA, Paris 7)
CCC’03, Chine (2003)
Intensional semantics of system T of Godel.
Pierre Valarcher.
Workshop on Domain IV, Dagsthul, ENTCS, volume 35, 2000