Direct application of Braga on the Ackermann function

[DmxLarchey]

Following an exercise started by David Monniaux, we use the Braga method to implement the Ackermann function, prove its termination (in just two lines of Ltac). Here is the extracted code:

let rec ack m n =
  match m, n with
  |   0 ,   _ -> S n
  | S m ,   0 -> ack m (S 0)
  | S m , S n -> ack m (ack (S m) n))

In the file ackermann_factored.v, there is the extraction of a much more difficult variant where the match n is factored between two branches:

let rec ack m n =
  match m with
  |   0 -> S n
  | S m -> ack m 
   (match n with
    |   0 -> S 0
    | S n -> ack (S m) n)

[DmxLarchey]

Adding the extraction of

let rec ack m n =
  match m with
  |   0 -> S n
  | S m -> ack m 
   (match n with
    |   0 -> S 0
    | S n -> ack (S m) n)

[moninjf]

C'est assez proche de ce qu'on peut faire avec les petites inversions exposées en 2021, à quelques modifs près non neutres :

• comme discuté par email, l'inductif "de départ" est directement exprimé sous forme "small invertible", en intégrant ce qu'on appelle avec Pierre les "inductifs partiels" sous forme mutuelle ; cela permet de définir plus rapidement les fonctions pred_inv et, comme prévu, de récupérer d'un coup toutes les composantes.
• une contrainte des inductifs mutuels est d'avoir les mêmes paramètres partout ; en l'occurrence ici, aucun, ce qui entraîne des destruct (ou des mach) plus lourds (avec les petites inversions 2021 on peut être beaucoup plus fin) ; mais les conséquences sont peu graves dans les circonstances présentes ;
• le procédé exposé en 2021est le même pour tous les constructeurs de la relation à inverser ; ici ce procédé a été employé seulement pour le constructeur ack1_mS, tandis que ack1_m0 est traité de façon ad-hoc, ce qui explique les eq_refl et autres "_ = n". On peut coller de plus près, le gain sur ack123 serait peut-être cosmétique, mais pas en nb de lignes de code.

Encore une fois, il n'y a pas encore de publi officielle sur les petites inversions à base d'inductifs partiels et je dois faire attention à ce qui se passe avec la thèse que je co-encadre avec Pierre sur ce sujet.

Je proposerais donc de juste mentionner qu'il y a une parenté avec ce que j'ai exposé en 2021 (et rappelé lapidairement à TYPES 2022), si tu es d'accord.

[DmxLarchey]

Encore une fois, il n'y a pas encore de publi officielle sur les petites inversions à base d'inductifs partiels et je dois faire attention à ce qui se passe avec la thèse que je co-encadre avec Pierre sur ce sujet.

En fait ce PR est un exercice d'initiation commencé par @monniaux. Je ne sais pas si il a une autre vocation. En particulier, je n'envisage pas de merge avec main.

Je proposerais donc de juste mentionner qu'il y a une parenté avec ce que j'ai exposé en 2021 (et rappelé lapidairement à TYPES 2022), si tu es d'accord.

Tu peux me donner une réf. sur cet exposé? Je ne le trouve pas dans ta biblio.

[moninjf]

En 2021 il y a eu 3 exposés, 1 au CNAM en visio, 1 à Verimag (hybride) et 1 au groupe de travail Coq (visio). Dispo depuis ma page, lien direct
https://www-verimag.imag.fr/~monin/Talks/sir.pdf
(il y a dedans 2 sujets, Braga puis les petites inversions).

En 2022 aussi sur ma page, liens directs
article: https://www-verimag.imag.fr/~monin/Publis/Docs/types22-smallinv.pdf

diapos: https://www-verimag.imag.fr/~monin/Talks/sminv22.pdf

[moninjf]

J'ai mis une propal de commentaires et ai repéré une typo (?) au passage

[DmxLarchey]

En fait je suis très perturbé par le Dack qui oublie Gack dans ackermann_simple.v. Pour des raisons déjà évoquées (ce n'est pas Braga), mais aussi pour d'autres raisons:

• ce prédicat intègre déjà l'argument de terminaison: le produit lexicographique;
  • mais en même temps il masque cette notion derrière un prédicat qui semble ad-hoc;
• la preuve de la bonne fondation du produit lexico est justement basée sur l'induction imbriquée
  • exactement celle utilisée pour ack_termination;
  • mais c'est une instance d'un principe beaucoup plus général.

Donc en fait, je ne suis pas sûr que ce Dack explique grand chose:

• oui on n'a pas besoin de Gack;
• mais en fait on pourrait même écrire
  ack' (S m) (S n) = ack' m (f (ack' (S m) n))
  où f : nat -> nat est n'importe quelle fonction totale que ça marcherait aussi.

La raison pour laquelle ack est totale est bien plus générale que juste le domaine d'Ackermann.

Maintenant, comment expliquer simplement le produit lexicographique pour ne pas digresser trop fort:

• ma première approche avec ack_termination que tu as un peu désautomatisée, c'était:
  • tout le monde connait les produits lexico et pourquoi c'est bien fondé alors j'automatise (je réfute cependant le terme IA pour ça, l'automatisation produit un résultat fiable);
  • mais je suis d'accord, l'automatisation masque des détails qui peuvent être importants ou pas;
  • bien ou pas : ça dépend en fait de celui qui lit.
• donc méa culpa: j'exagère, en fait ce n'est pas évident pour tout le monde, alors je développe le produit lexico. dans ackermann_lex2.v mais en fait ça devient longuet si on veut tout expliciter
  • en particulier les projections avec inductifs spécialisés.
• il y a un petit bénéfice avec le domain définit par Dack := Acc ack_sub_calls puisque maintenant, on a une preuve directe que ack_sub_calls est incluse dans lex2
  • c'est normal, les appels récursifs respectent le produit lexico.
  • donc on a directement la preuve de totalité en utilisant simplement wf_incl et une belle abstraction.

A la réflexion, je ne sais pas trop comment faire de ce petit exercice une étude de cas instructive pour le lecteur:

• on veut mettre en avant Braga
• on veut expliciter un produit lexicographique
• on veut que ça reste court
• on veut cibler un programmeur ou un matheux ?
  • un programmeur ne sera pas motivé par Ackermann qui est trop académique
  • un matheux oui mais il n'aura pas de problème à comprendre la terminaison
• d'autres motivations ?

[moninjf]

Pour l'instant je vois cet exemple plutôt comme un terrain d'interrogations qu'autre chose, et il faut prendre le temps de le digérer.