Coq head normal formのヘッドとは何ですか？

Question

Coq/CICヘッドノーマルフォームの理解に問題があります。具体的には、私は頭が何かを理解していません。リファレンスマニュアル（8.5p1）は言うこと

任意の用語は、以下のように書くことができる

しかし、上記の定義は、否定的な意味である：それはではないt0が必要ですアプリケーションは、はt0ができることを言っていない。実際には、私が覚えている限り、t0 t1 t2 ...として書かれる唯一のものは、の関数またはコンストラクタのアプリケーションt0です。

誰かがここで首尾よく何ができるのかを綴ることができますか？

Answer 1

はい、t0 t1 ... tnはアプリケーションですが、マニュアルではt0のフォームについて話しています。手動で

、一部iためtまたはti通常用語を示し、そうt0は、任意の用語であることができ、それはアプリケーションではなく、例えばλ抽象化など - マニュアルのsect. 4.1.2と構文についてはsect. 1.2.1のリストを参照してください。

また、thisウィキペディアのページが役立つかもしれません。