Mardi 07/12/2010, à partir de 10h30, en salle Byron Blanc.
Orateur : Yves Bertot.
Titre : Induction et co-induction mêlées.
Résumé :
Plusieurs expériences montrent que les types de données qui mélangent de l’induction et de la co-induction peuvent être utiles pour la programmation. En particulier, cela permet de décrire la productivité de certains algorithmes qui ne respectent pas les conditions de garde du système Coq. Dans cet exposé, nous nous concentrerons sur une description particulière de la séquence de Fibonacci, qui est bien formée du point de vue sémantique, mais qui est rejetée par la condition de garde. Nous montrerons comment cette description peut être modélisée en combinant de la co-récursion acceptée par Coq et de la récursion relative à un prédicat inductif.
