Was ist ein Kopf in Coq Kopf Normalform?

Question

Ich habe Probleme, Coq/CIC Kopf Normalform zu verstehen. Genauer verstehe ich nicht, was ein Kopf ist. Das Referenzhandbuch (8.5p1) sagt, dass

Jeder Begriff kann geschrieben werden:

Aber die obige Definition ist im negativen Sinne: es erfordert t0 nicht zu sein Anwendung, aber nicht gesagt, was kannt0 sein. Soweit ich mich erinnern kann, ist das einzige, was als t0 t1 t2 ...geschrieben werden kann, eine Anwendung einer Funktion oder Konstruktor t0.

Kann jemand mithelfen, was genau kann der Kopf hier sein?

Answer 1

Ja, t0 t1 ... tn ist eine Anwendung, aber das Handbuch spricht über die Form von t0 allein stehend.

Im Handbuch t oder ti für einige i gewöhnlich eine, Begriff bezeichnet so t0 beliebigen Begriff sein kann, ist, dass nicht eine Anwendung, z.B. eine λ-Abstraktion usw. - siehe die Liste in sect. 4.1.2 des Handbuchs und die sect. 1.2.1 Syntax.

Auch this Wikipedia-Seite könnte eine Hilfe sein.