0

Isabelle / HOLの優れたプログラミングと証明では、次のように書かれています

[...] 再帰関数とは対照的に、帰納的定義には終了要件はありません。(pdf p.40)

  1. これは、無限に深い派生ツリーを持つことが可能な帰納的定義があることを意味しますか?
  2. そのような非終了の派生 (できれば無限の高さを持つもの) の例は何ですか? これらをどのように「構築」しますか？
  3. これらの規則誘導の原則はどのようにまだ健全ですか?
4

2 に答える 2