Deterministic computations in functional languages: a survey of confluence
- LecturerProf. Jean-Pierre Jouannaud (INRIA and Tsinghua University)
Host: Bow-Yaw Wang - Time2013-04-30 (Tue.) 14:00 ~ 16:00
- LocationAuditorium 106 at new IIS Building
Abstract
Modern functional languages mix two computation paradigms: Church's lambda calculus, and Herbrand-Goedel equational definitions in a rewrite rules format. Both computation mechanisms are inherently non-deterministic. After explaining how determinacy relates to a graph-theoretic property of computations, namely confluence, we review the various methods used to show confluence of functional computations. Classically, we proceed in two steps. First, we review the sufficient conditions of Newmann (1942) and Hindley (1967) based on properties of locally diverging computations, before to introduce a recent complete method, decreasing diagrams, that captures therefore both. This then leads to an analysis of diverging computations in concrete languages introduced by Knuth under the name of critical pairs, that assumes either termination (Newmann), or left-linearity (Hindley) of the rewriting rules.
In presence of non-left linear non-terminating computations, the only current known methodology for showing confluence is based on a divide and conquer schema, assuming that the non-left linear subset terminates.
Confluence can the be deduced for the whole system by using Toyama's modularity result.
Both the completeness of decreasing diagrams and Toyama's modularity theorem can be proved by using Klop's characterization of confluence by the existence of a cofinal derivation (1980). We will sketch at least one of these two proofs, both if time permits.