Term (Type Theory)

Definition

A term is a formal expression belonging to a type. In the judgment $a:A$, $a$ is the term and $A$ is its type. Under the Curry-Howard correspondence, a term represents a program or a proof of the proposition encoded by its type.

Formation

Terms are constructed according to the introduction rules and elimination rules of their respective types. In lambda calculus, terms include variables, lambda abstraction, and function application.

• Introduction: $\lambda x.M$ constructs a term of type $A\to B$.
• Elimination: $MN$ extracts a value by applying a function term.