The Dependency Pair method is one of the most successful method for proving mechanically the termination of rewriting systems. In this talk, after presenting quickly the method, I will show how it can be derivable constructively and I wish this will lead to new certified proofs of termination, with the argument of termination based on a certificate. This is a research in progress in collaboration with Keiichiro Kukasari of the University of Nagoya (Japan).

We consider the complexity of geometric problems in unit cost models, such as the real-Random Access Machine and Algebraic Computation Trees. In these models of computations, a memory cell can hold a real number, and an arithmetic operation on two real numbers is performed in unit time. I'll present some problems related to computing the diameter (joint work with A. Vigneron). This will be the opportunity to review known bounds and techniques for fundamental problems such as element-distinctness or Hopcroft's problem (given some points and lines in the plane, decide if one of the points lies on one of the lines).

The computational complexity of the algorithm is defined as quantity of computer resources like time and space needed for performance of the algorithm. Certainly, the required resources depend on the complexity of input data so it is really essential to determine the relation between resources and complexity of input data.

The level of complexity of input data is usually called the size of input data. It is most frequently defined as a number of isolated parts forming the input data. While such a definition usually works well for analysis of number sorting algorithms, the "reasonable" definition of complexity of computer structures such as trees or graphs seems to be quite difficult.

In my speach I will try to shed some light on this problem by examining various aspects of functions that measure the complexity of different input structures. We will be able to see what they measure, when they measure it in a similar way, and if they differ, what this difference is.

Abstract available in pdf file here.

Growth processes have been studied for several years, so as to obtain some basic recursive constructions and short formulae for boolean functions such as majority. There exists a classification of growth processes according to the properties of the single logical connector that defines them. But what does happen when the connector is not the same from one step to the next? In this talk we consider growth processes built from two connectors And and Or, and characterize the boolean functions they lead to.

And/or trees are representations of boolean functions built from conjunction, disjunction and positive and negative literals. For a fixed set of k variables, the uniform probability distribution on the set of all and/or trees of size n, induces in a natural way distribution P(k,n) on the set of all k-ary boolean function. When n goes to infinity we obtain some limiting distribution P(k), we call it Catalan measure.

I will show that there exists a family of functions whose Catalan measure tends to 1 while its uniform measure tends to 0 (when the number of variables k goes to infinity).