term

term An expression formed from symbols for functions, constants, and variables. An example is f(a,g(h(b),c,d))

Terms are defined recursively as follows: a term is either a variable symbol, a constant symbol, or else has the form φ(τ₁,…,τ_k), where φ is a function symbol and each of τ₁,…,τ_k is itself a term. The example above thus has the overall form f(τ₁,τ₂): in this case φ = f and k = 2. Another constraint is that different occurrences of the same symbol φ cannot occur with different values of k, i.e. each φ must have a fixed arity (number of arguments). Thus f(a,f(h(b),c,d))

would not be a term since the first f has arity 2 while the second has arity 3; neither would f(a,g(h(b),c,h)),

since the first h has arity 1 while the second has arity 0.

Terms are often built using signatures. A Σ-term is a term in which each constant and function symbol used is in a signature Σ, and has the arity associated with it by Σ and, if Σ is a many-sorted signature, all the sorts match properly. A Σ-term is also called a term over signature Σ. Often a Σ-term is allowed to contain variables (of arity 0) in addition to symbols in Σ. Terms containing variables are called open terms; terms containing only symbols of the signature are called closed or ground terms. Terms can also be viewed as trees (see tree language). Terms (whether as expressions or as trees) are important in the construction of virtually all syntactic concepts. Terms as defined here are sometimes called first-order terms, to distinguish them from the higher-order terms (such as those involved in lambda calculus). See also predicate calculus, initial algebra, equation.