|
|
 |
|
Vendredi 14 Février
| Heure: |
00:59 - 12:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Two Intensional Phenomena: The Size of Church-Rosser Diagrams, and Characterization of PTIME via Overlapping Cons-Free Systems |
| Description: |
Jakob Grue Simonsen We will informally discuss two very different problems that both concern
the intensional behaviour of very simple calculi: First-order term
rewriting systems, respectively lambda calculus.
The first problem concerns finding bounds on the size of confluence and
Church-Rosser diagrams: If s is a term in a confluent, we know that
every "peak" t *<-s ->* t' has a corresponding "valley" t ->* s' *<- t',
but it is not at all clear how the number of steps in the "valley" relates
to the number of steps in the "peak" and to the size of the starting
term s. We will discuss how valley sizes can always be computed, how
the sizes may majorize any computable function on the integers, how
exponential bounds can be found for first-order term rewriting, and
for lambda calculus how there is an enormous difference between the
best-known upper bound (not even elementary recursive) and the
worst-case example known (doubly exponential).
The second problem concerns implicit complexity and how to characterize
the set of PTIME-decidable sets by first-order term rewriting systems
in the most liberal fashion possible: No restrictions on reduction
strategy (hence no insistence on call-by-name, call-by-value or other
functional-programming-inspired strategies), no restrictions on overlaps
between left-hand sides of rules, and as few linearity constraints as we
can get away with (and absolutely no explicit typing of any kind).
The talk will be kept at high-level and present the interesting problems
and challenges; we will only delve into technical details if the
audience feels like it. The material presented is based on joint,
ongoing, work with Jeroen Ketema and Daniel de Carvalho. |
|
|
