Coq meilleures pratiques: récursion mutuelle, une seule fonction est décroissante structurellement

Question

Considérons la représentation du jouet suivant pour le calcul typées lambda:

Require Import String. 
Open Scope string_scope. 

Inductive term : Set := 
| Var : string -> term 
| Abs : string -> term -> term 
| App : term -> term -> term. 

Fixpoint print (term : term) := 
    match term return string with 
    | Var id => id 
    | Abs id term => "\" ++ id ++ " " ++ print term 
    | App term1 term2 => print_inner term1 ++ " " ++ print_inner term2 
    end 
with print_inner (term : term) := 
    match term return string with 
    | Var id => id 
    | term => "(" ++ print term ++ ")" 
    end. 

vérification de type print échoue avec l'erreur suivante:

Recursive definition of print_inner is ill-formed. 
[...] 
Recursive call to print has principal argument equal to "term" instead of "t". 

Quelle serait la manière la plus lisible/ergonomique/efficace de mettre en œuvre ceci?

Answer 1

Vous pouvez utiliser les fonctions récursives imbriquées:

Fixpoint print (tm : term) : string := 
    match tm return string with 
    | Var id => id 
    | Abs id body => "\" ++ id ++ ". " ++ print body 
    | App tm1 tm2 => 
    let fix print_inner (tm : term) : string := 
     match tm return string with 
     | Var id => id 
     | _ => "(" ++ print tm ++ ")" 
     end 
    in 
    print_inner tm1 ++ " " ++ print_inner tm2 
    end. 

Cette approche peut être étendue à gérer assez d'impression - la convention habituelle de ne pas imprimer entre parenthèses dans des expressions comme x y z (associés d'application à gauche) ou à imprimer \x. \y. x y comme \xy. x y:

Definition in_parens (stm : string) : string := "(" ++ stm ++ ")". 

Fixpoint pprint (tm : term) : string := 
    match tm with 
    | Var id => id 
    | Abs id tm1 => 
    let fix pprint_nested_abs (tm : term) : string := 
     match tm with 
     | Abs id tm1 => id ++ pprint_nested_abs tm1 
     | _ => ". " ++ pprint tm 
     end 
    in 
    "\" ++ id ++ pprint_nested_abs tm1 

    (* e.g. (\x. x x) (\x. x x) *) 
    | App ((Abs _ _) as tm1) ((Abs _ _) as tm2) =>  
     in_parens (pprint tm1) ++ " " ++ in_parens (pprint tm2) 

    (* variable scopes *) 
    | App ((Abs _ _) as tm1) tm2 => in_parens (pprint tm1) ++ " " ++ pprint tm2 

    (* `x \x. x` looks ugly, `x (\x. x)` is better; also handle `x (y z)` *) 
    | App tm1 ((Abs _ _) as tm2) | App tm1 (App _ _ as tm2) => 
     pprint tm1 ++ " " ++ in_parens (pprint tm2) 

    | App tm1 tm2 => pprint tm1 ++ " " ++ pprint tm2 
    end. 

Par ailleurs, CPDT a some material sur la récursion mutuelle contre récursion imbriquées, mais dans un contexte différent.

Answer 2

Vous pouvez également découpler l'idée de faire un appel récursif de l'analyse de cas réalisée par print_inner comme ceci:

Definition print_inner (term : term) (sterm : string) : string := 
match term with 
| Var id => id 
| _  => "(" ++ sterm ++ ")" 
end. 

Fixpoint print (term : term) := 
    match term return string with 
    | Var id => id 
    | Abs id term => "\" ++ id ++ " " ++ print term 
    | App term1 term2 => print_inner term1 (print term1) 
        ++ " " ++ print_inner term2 (print term2) 
    end. 

Alternativement, vous pouvez utiliser un algorithme différent reposant sur le niveau de fixité du constructeur de décider s'il faut ou non mettre les parenthèses entre parenthèses.