coqmutual-recursiontotality

Coq best practice: mutual recursion, only one function is structurally decreasing


Consider the following toy representation for the untyped lambda calculus:

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.

Type-checking print fails with the following error:

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

What would be the most readable/ergonomic/efficient way of implementing this?


Solution

  • You can use nested recursive functions:

    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.
    

    This approach can be extended to handle pretty-printing -- the usual convention not to print parentheses in expressions like x y z (application associates to the left) or to print \x. \y. x y as \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.
    

    By the way, CPDT has some material on the mutual recursion vs. nested recursion, but in a different setting.