arXiv subjects
Publications and source records attributed to Jean-Yves Moyen.
We investigate computability in the lattice of equivalence relations on the natural numbers. We mostly investigate whether the subsets of appropriately defined subrecursive equivalence relations -for example the set of all polynomial-time decidable equivalence relations- form sublattices of the lattice.
Several techniques for analysis and transformations are used in compilers. Among them, the peeling of loops for hoisting quasi-invariants can be used to optimize generated code, or simply ease developers' lives. In this paper, we introduce a new concept of dependency analysis borrowed from the field of Implicit Computational Complexity (ICC), allowing to work with composed statements called Chunks to detect more quasi-invariants. Based on an optimization idea given on a WHILE language, we provide a transformation method - reusing ICC concepts and techniques - to compilers. This new analysis computes an invariance degree for each statement or chunks of statements by building a new kind of dependency graph, finds the maximum or worst dependency graph for loops, and recognizes if an entire block is Quasi-Invariant or not. This block could be an inner loop, and in that case the computational complexity of the overall program can be decreased. We already implemented a proof of concept on a toy C parser 1 analysing and transforming the AST representation. In this paper, we introduce the theory around this concept and present a prototype analysis pass implemented on LLVM. In a very near future, we will implement the corresponding transformation and provide benchmarks comparisons.
We consider the partition lattice $Π_κ$ on any set of transfinite cardinality $κ$ and properties of $Π_κ$ whose analogues do not hold for finite cardinalities. Assuming the Axiom of Choice we prove: (I) the cardinality of any maximal well-ordered chain is always exactly $κ$; (II) there are maximal chains in $Π_κ$ of cardinality $> κ$; (III) if, for every cardinal $λ< κ$, we have $2^λ < 2^κ$, there exists a maximal chain of cardinality $< 2^κ$ (but $\ge κ$) in $Π_{2^κ}$; (IV) every non-trivial maximal antichain in $Π_κ$ has cardinality between $κ$ and $2^κ$, and these bounds are realized. Moreover we can construct maximal antichains of cardinality $\max(κ, 2^λ)$ for any $λ\le κ$; (V) all cardinals of the form $κ^λ$ with $0 \le λ\le κ$ occur as the number of complements to some partition $\mathcal{P} \in Π_κ$, and only these cardinalities appear. Moreover, we give a direct formula for the number of complements to a given partition; (VI) Under the Generalized Continuum Hypothesis, the cardinalities of maximal chains, maximal antichains, and numbers of complements are fully determined, and we provide a complete characterization.
We present iSAPP (Imperative Static Analyser for Probabilistic Polynomial Time), a complexity verifier tool that is sound and extensionally complete for the Probabilistic Polynomial Time (PP) complexity class. iSAPP works on an imperative programming language for stack machines. The certificate of polynomiality can be built in polytime, with respect to the number of stacks used.
Quasi-interpretations are a technique to guarantee complexity bounds on first-order functional programs: with termination orderings they give in particular a sufficient condition for a program to be executable in polynomial time, called here the P-criterion. We study properties of the programs satisfying the P-criterion, in order to better understand its intensional expressive power. Given a program on binary lists, its blind abstraction is the nondeterministic program obtained by replacing lists by their lengths (natural numbers). A program is blindly polynomial if its blind abstraction terminates in polynomial time. We show that all programs satisfying a variant of the P-criterion are in fact blindly polynomial. Then we give two extensions of the P-criterion: one by relaxing the termination ordering condition, and the other one (the bounded value property) giving a necessary and sufficient condition for a program to be polynomial time executable, with memoisation.