Term — as an Expression of a Formal Language (System)

Term — an expression of a formal language (system) of a special kind. By analogy with natural language, where a noun phrase refers to an object and a whole sentence refers to a fact, in mathematical logic a term denotes a mathematical object, while a formula denotes a mathematical fact. In particular, terms appear as components of a formula.

A first-order term is recursively defined from constant, variable, and function symbols . An expression obtained by applying a predicate symbol to the corresponding number of terms is called a logical atom, whose value in two-valued logic based on a logical interpretation is evaluated as «true» or «false ». For example, — this is a term built from the constant 1, the variable x and the binary function symbols + and ∗ ; it is part of the atomic formula , which takes the value «true» for any real x.

Besides logic, terms play an important role in universal algebra and rewriting systems.

The set of terms of signature , where R — the set of predicates, F — the set of functions, and μ — the arity mapping for Σ , is defined inductively:

1. variables are terms of signature Σ
2. if is a term of signature Σ , f∈F and μ(f)=n, then — is a term of signature Σ .

The notation when n=0 denotes Θ. In particular, from item 2 we obtain that the symbol of a constant of signature Σ is a term of signature Σ.

Left to right: tree structure of the term ( n ⋅( n +1))/2 and n ⋅(( n +1)/2)

Given a set V of variable symbols, a set C of constant symbols, and sets F _n of n -ary functions, also called operator symbols, for each natural number n ≥ 1, the set (of unsorted first-order terms) T is recursively defined as the smallest set with the following properties: ^{[ 1 ]}

• every variable symbol is a term: V ⊆ T ,
• every constant symbol is a term: C ⊆ T ,
• from every n terms t ₁ ,..., t _n and every n -ary function symbol f ∈ F _n a larger term can be built f ( t ₁ , ..., t _{n ).}

Using an intuitive pseudo-grammar notation, this is sometimes written as:

t ::= x | c | f ( t ₁ , ..., t _n ).

The signature "language" of a term describes which sets of function symbols F n _{are used} . Well-known examples are the unary function symbols sin , cos ∈ F ₁ and the binary function symbols +, −, ⋅, / ∈ F ₂ . Ternary operations and functions of higher arity are possible, but are rarely encountered in practice. Many authors treat constant symbols as 0-ary function symbols F ₀ , so no special syntactic class is required for them.

A term denotes a mathematical object from the domain of discourse. The constant c denotes a named object from this domain, the variable x ranges over objects in this domain, and the n -ary function f maps n -tuples of objects to objects. For example, if n ∈ V is a variable symbol, 1 ∈ C is a constant symbol, and add ∈ F ₂ is a binary function symbol, then n ∈ T , 1 ∈ T , and (consequently) add ( n , 1) ∈ T by the first, second, and third term construction rules respectively. The last term is usually written as n + 1 , using infix notation and the more common operator symbol + for convenience.

Originally, logicians defined a term as a string of symbols, obeying certain rules of formation. ^{[ 2 ]} However, since the concept of a tree became popular in computer science, it turned out to be more convenient to represent a term as a tree. For example, several different strings of symbols, such as «, denote the same term and correspond to the same tree, namely the left tree in the figure above. By separating the tree structure of a term from its graphical representation on paper, it is easy to account for parentheses (which are only a matter of representation, not structure) and invisible multiplication operators (which exist only in the structure, not in the representation).

Two terms are considered structurally , literally or syntactically equal if they correspond to the same tree. For example, the left and right trees in the figure above are structurally unequal terms, although they can be considered « semantically equal », since they always give the same value in rational arithmetic. While structural equality can be checked without knowing the meaning of the symbols, semantic equality cannot. If the function / is interpreted, for example, not as rational division but as truncating integer division, then for n = 2 the left and right terms will have the values 3 and 2 respectively. Structurally equal terms must agree in their variable names.

In contrast, a term t is called a renaming or variant of a term u , if the latter resulted from the consistent renaming of all the variables of the former, i.e. if u = tσ for some renaming substitution σ. In this case u is also a renaming of t , since the renaming substitution σ has an inverse σ ⁻¹ , and t = uσ ⁻¹ . Both terms are then also called equal modulo renaming . In many contexts, the specific variable names in a term have no significance; for example, the commutativity axiom for addition can be formulated as x + y = y + x or as a + b = b + a ; in such cases the entire formula can be renamed, whereas an arbitrary subterm generally cannot, for example, x + y = b + a is not a valid version of the commutativity axiom.

The set of variables of a term t is denoted as vars ( t ). A term containing no variables is called a ground term ; a term containing no multiple occurrences of a single variable is called a linear term . For example, 2+2 is a ground term and hence also a linear term, x ⋅( n +1) — is a linear term, n ⋅( n +1) — is a non-linear term. These properties are important, for example, in term rewriting.

Given a signature for function symbols, the set of all terms forms the algebra of free terms . The set of all ground terms forms the initial term algebra .

Abbreviating the number of constants as f ₀ , and the number of i- -ary function symbols as f _i , the number θ _h of distinct ground terms of height up to h can be computed using the following recursive formula:

• θ ₀ = f ₀ , since a ground term of height 0 can only be a constant,
• , since a ground term of height up to h + 1 can be obtained by combining any i ground terms of height up to h using an i- -ary root function symbol. The sum has a finite value if there is only a finite number of constants and function symbols, which is usually the case.

Given a set of R _n -ary relation symbols for each natural number n ≥ 1, then a (unsorted) first-order atomic formula is obtained by applying an n -ary relation symbol to n terms. As with function symbols, the set of relation symbols R _n is usually non-empty only for small n . In mathematical logic, more complex formulas are built from atomic formulas using logical connectives and quantifiers. For example, let denote the set of real numbers, ∀ x : x ∈ ⇒ ( x +1)⋅( x +1) ≥ 0 — is a mathematical formula that takes the value «true» in the algebra of complex numbers. An atomic formula is called ground if it is built entirely from ground terms; all ground atomic formulas that can be formed from a given set of function and predicate symbols make up the Herbrand base for those sets of symbols.

Tree structure of the example black term , with the blue redex ⁠

• Since a term has the structure of a tree hierarchy, each of its nodes can be assigned a position (a path), that is, a string of natural numbers indicating the node's place in the hierarchy. The empty string, usually denoted ε, is assigned to the root node. The position strings inside the term highlighted in black are shown in red in the figure.
• At each position p of the term t there begins a unique subterm , which is usually denoted as t | _p . For example, at position 122 of the black term in the figure the root of the term is a + 2. The relation «is a subterm of» is a partial order on the set of terms; it is reflexive, since every term is trivially a subterm of itself.
• A term obtained by replacing in the term t the subterm at position p with a new term u, is usually denoted as t [ u ] _p . The term t [ u ] _p can also be viewed as the result of a generalized concatenation of the term u with the term-like object t [.] ; the latter is called a context or term with a hole (denoted "."; its position is p ), into which is said to be embedded u . For example, if t — is the black term in the figure, then t [ b +1] ₁₂ gives the term . The latter term is also obtained as the result of embedding the term b +1 into the context. Informally, the operations of instantiation and embedding are inverse to each other: the former adds function symbols at the end of a term, while the latter adds them at the beginning. The subsumption order relates a term and any result of additions on both sides.
• Each node of a term can be assigned its depth (some authors call it height ), that is, the distance (number of edges) from the root. In this case, the depth of a node is always equal to the length of its position string. In the figure, the depth levels in the black term are shown in green.
• The size of a term is usually defined by the number of its nodes, or, equivalently, the length of its written representation, not counting parentheses. The black and blue terms in the figure have sizes 15 and 5, respectively .
• A term u matches a term t , if a substitution instance of u is structurally equal to a subterm of t , or formally, if u · σ = t | _p for some position p in t and some substitution σ. In this case u , t and σ are called the pattern term , subject term and the matching substitution respectively. In the figure, the blue pattern term ⁠ ⁠ matches the black subject term at position 1 with the corresponding substitution { x ↦ a , y ↦ a +1, z ↦ a +2}, shown by the blue variables placed to the left of their black replacements. Intuitively, the pattern, apart from its variables, must be contained in the subject; if a variable occurs multiple times in the pattern, the corresponding positions in the subject must contain identical subterms.
• unifying terms
• rewriting terms

When the domain of discourse contains elements of fundamentally different kinds, it is useful to partition the set of all terms accordingly. To do this, each variable and each constant symbol is assigned a sort (sometimes also called a type), and each function symbol is assigned a declaration of domain sorts and a range sort. A sorted term f ( t 1 ,..., t n ) can be composed of sorted subterms t ₁ ,..., t _{n ,} only if the sort of the i -th subterm matches the declared sort of the i-th domain f . Such a term is also called well-sorted ; any other term (i.e. obeying only the unsorted rules) is called ill-sorted .

For example, a vector space has an associated field of scalar numbers. Let W and N denote the type of vectors and numbers respectively, V _W and V _N — the sets of vector and numeric variables respectively, and C _W and C _{N —} the sets of vector and numeric constants respectively. Then, for example, and 0 ∈ C _N , and vector addition, scalar multiplication, and the dot product are declared as ⁠ ⁠ , and ⁠ , respectively. Assuming the variable symbols and a , b ∈ V _N , the term is well-sorted, whereasv→+ais not (since + does not accept a term of type N as its second argument). To make a well-sorted term, an additional declaration ⁠ is required. Function symbols having several declarations are called overloaded .

For more information, see the section «Many-sorted logic» , including extensions of the many-sorted framework, described there.

Terms with Bound Variables

Example notation	Bound variables	Free variables	Written as lambda term
lim n →∞ x / n	n	x	limit (λ n . div ( x , n ))
	i	n	sum (1, n ,λ i . power ( i ,2))
	t	a , b , k	integral ( a , b ,λ t . sin ( k ⋅ t ))

The mathematical notations shown in the table do not fit into the first-order term scheme defined above, since they all introduce their own local or bound variable, which cannot appear outside the scope of the notation, for example does not make sense. In contrast, other variables, called free , behave like ordinary first-order variables, for example, makes sense.

All these operators can be viewed as taking a function as an argument, rather than a value. For example, the operator lim is applied to a sequence, that is, to a mapping from a positive integer to a real number. Another example: the C function implementing the second example from the table, Σ, will have a function-pointer argument (see the box below).

Lambda terms can be used to denote anonymous functions that will be supplied as arguments to lim , Σ, ∫ etc.

For example, the square function from the C program below can be written anonymously as the lambda term λ i . i ² . Then the general sum operator Σ can be regarded as a ternary function symbol, taking the lower bound value, the upper bound value, and the function to be summed. Because of its last argument, the Σ operator is called a second-order function symbol . As another example, the lambda term λ n . x / n denotes a function that maps 1, 2, 3, ... to x / 1, x / 2, x / 3, ..., respectively, that is, it denotes the sequence ( x / 1, x / 2, x / 3, ...). The operator lim takes such a sequence and returns its limit (if defined).

The rightmost column of the table shows how each example of mathematical notation can be represented by a lambda term, and how common infix operators are converted to prefix form.

Given a set of V variable symbols, the set of lambda terms is recursively defined as follows:

• every variable symbol x ∈ V is a lambda term;
• if x ∈ V — is a variable symbol, and t — is a lambda term, then λ x . t is also a lambda term (abstraction);
• if t ₁ and t ₂ are lambda terms, then ( t ₁ t ₂ ) is also a lambda term (application).

The motivating examples above also used some constants, such as div, power, etc., which, however, are not allowed in pure lambda calculus.

Intuitively, the abstraction λ x . t denotes a unary function that returns t given x , whereas the application ( t 1 t 2 ) denotes the result of calling the function t 1 with the input t 2 . For example, the abstraction λ x . x denotes the identity function, and λ x . y denotes a constant function that always returns y . The lambda term λ x .( x x ) takes a function x and returns the result of applying x to itself.

• Equation
• Expression (mathematics)
• Many-sorted logic
• [[b6933]]