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のような式で括弧を印刷しない通常の規則をかへ

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を持っていますが、別の設定に：\x. \y. x y\xy. x yとして印刷します。あなたはまた、そうのようなprint_innerによって行われるケースの分析から、再帰呼び出し作るというアイデア切り離すことができ

Answer 2

：また

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. 

を、あなたが決めるためにコンストラクタの固定性のレベルに依存する別のアルゴリズムを使用することができますかっこを削除するかどうか。