Лучшая практика Coq: взаимная рекурсия, структурно уменьшается только одна функция

Question

Рассмотрим следующее игрушечное представление для нетипизированного лямбда-исчисления:

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.

Тип проверка print завершается со следующей ошибкой:

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

Что было бы наиболее читаемым / эргономичным / эффективным способом реализации этого?

Answer 1

Вы можете использовать вложенные рекурсивные функции:

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.

Этот подход может быть расширен для обработки симпатичной печати - обычное соглашение не печатать скобки в таких выражениях, как x y z (приложение ассоциируется слева) или распечатать \x. \y. x y как \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.

Кстати, у CPDT есть некоторый материал о взаимной рекурсии и вложенной рекурсии, но в другой среде.

Answer 2

Вы также можете отделить идею создания рекурсивного вызова от анализа случая, выполненного print_inner вот так:

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.

В качестве альтернативы, вы можете использовать другой алгоритм, основанный на уровне фиксированности конструктора, чтобы решить, следует ли исключить скобки.