To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 22/02/10 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 22 février, 10h30 ------------------ Arthur Charguéraud ------------------ INRIA ========================================= Le combinateur de "points fixes optimaux" ========================================= Dans le lambda calcul pur, on peut définir un combinateur de point fixe générique, comme par exemple "Y". En Coq, ce n'est pas possible, car tous les programmes doivent terminer. Dans cet exposé, je vous montrerai comment contourner le problème, en définissant un combinateur qui prend en argument une fonctionelle arbitraire et retourne son point fixe "optimal". Ce point fixe est la fonction partielle solution de l'équation de point fixe qui a le plus grand domaine possible. Mon combinateur fournit une solution pratique à la formalisation de fonctions récursives et corécursives. Il permet aux utilisateurs d'échapper aux critères syntaxiques de terminaison et de productivité utilisés par Coq, facilitant ainsi la formalisation de définitions circulaires non triviales.