勒柯克最佳實踐：相互遞歸，只有一個功能，在結構上減少

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對相互遞歸與嵌套遞歸some material，但在不同的設置。

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. 

或者，你可以使用不同的算法依賴於構造的固定性水平來決定是否捨去括號。