Termination of rewrite systems: revisiting the dependency pair

Pierre Lescanne, ENS de Lyon

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).

On domain theory over Girard quantales

Paweł Waszkiewicz, Jagiellonian University


Algebraic complexity and computational geometry

Hervé Fournier , Université de Versailles St-Quentin en Yvelines

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).

Object Complexity Examples and Tools

Edward Szczypka, Jagiellonian University

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.


On density of truth of infinite logic

Zofia Kostrzycka, Opole University of Technology

Abstract available in pdf file here.


On density of truth of infinite logic

Antoine Genitrini, Université de Versailles St-Quentin en Yvelines

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.

Dark matter among and/or trees

Jakub Kozik, Jagiellonian University

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).


On some combinatorial problems in lambda calculus

Katarzyna Grygiel, Jagiellonian University

The aim of this talk is to present the quantitative approach to lambda calculus. We will focus on posing some questions concerning the number of lambda terms and their asymptotic density. However, some attempts to solve the raised problems will be shown, as well.


Is a random lambda term strongly normalizable ? (discussion)

René David, Christophe Raffalli, Guillaume Theyssier, University of Savoie