Room 285 (badged access, limited occupancy)
24 November 2022 - 10h00
Recursive Programming in Coq and Intensionality : oh happy case !
by Jean-François Monin from VERIMAG
24 November 2022 - 10h00
Recursive Programming in Coq and Intensionality : oh happy case !
by Jean-François Monin from 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.
