Copenhagen Programming Language Seminar


Convergence of some extended systems of reductions in simply-typed lambda-calculus with inductive types.

Sergei Soloviev,
IRIT, Toulouse, France

Thursday, November 10, 15:15-16:00
DIKU, Universitetsparken 1, room N026


The interest of extended systems of reductions is that some computational rules are presented as reductions and this may help to obtain more efficient algorithms for equality of lambda-terms (and functions they represent). It is well known that the reasoning based on extensional equality (for example, in proof assistants) could be extremely heavy. At the same time, the attempt to add reductions based on all extensional equalities usually results in systems that are not strongly normalizing and do not have Church-Rosser property (i.e., are not convergent). We studied the possibility to add reductions related to some extensional equalities of special interest in such a way that convergence is preserved.

Maybe most interesting case we studied was the case of isomorphic copy, i.e., the functions f: A --> A', f': A' --> A where A, A' are inductive type and its isomorphic copy (the names of constructors are changed and possibly some parameters are replaced by isomorphic types). The functions f, f' are mutually inverse w.r.t. extensional equality and new reduction is f' o f --> id, f o f' --> id. In the talk we consider this and other cases in the context of possible applications. The talk is based on joint works with D. Chemouil and F. Barral.

Scientific host: Andrzej Filinski. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org