Room 285 (badged access, limited occupancy)
24 novembre 2022 - 10h00
Programmation récursive en Coq et intensionalité : oh le beau cas !
par Jean-François Monin de VERIMAG
24 novembre 2022 - 10h00
Programmation récursive en Coq et intensionalité : oh le beau cas !
par Jean-François Monin de VERIMAG
Résumé : L'exposé porte sur une solution d'un exercice issu d'une discussion
récente avec David : donner un programme itératif (récursif terminal)
pour l'aplatissement d'un arbre à embranchements non bornés et en
démontrer la correction.
Écrire un tel programme en OCaml n'est pas le plus difficile :
employer un style CPS ; ou mieux, en restant au premier ordre,
un zippeur qui code la pile des appels en suspens.
Mais, alors que le programme CPS est structurel récursif sur l'arbre
en entrée, une transcription directe en Coq de celui au premier ordre
ne respecte plus la condition de garde.
Je présenterai comment, en revanche, la méthode de Braga dégraissée de
son graphe et munie des progrès récents sur les petites inversions a
particulièrement bien fonctionné sur cet exemple.
Je militerai en passant pour une approche à contre-courant de la
fuite en avant vers l'extensionnalité qui prévaut si souvent :
les preuves de correction partielle sont ici allégées au moyen d'une
accentuation intensionnelle des programmes qui servent de trame, à
commencer par la concaténation de listes.
La production d'un certificat de terminaison, effectuée en dernier
est apparue extrêmement courte... mais involontairement subtile :
elle illustre en particulier que la récursion emboîtée est strictement
plus puissante que la récursion mutuelle.
Room with limited occupancy, please contact us if you plan to come.
La salle ayant une capacité limitée, merci de prendre contact si vous souhaitez venir.
