145 Denotation Terms

A term is a syntactic value-expression represented as a string of symbols, built from logic variables and function symbols.

The set of terms is defined inductively:

• Any logic variable symbol is a term.
• If f is an n-ary function symbol and t₁,… ,tₙ are terms, then f(t₁,…,tₙ) is a term.

Only expressions obtained by finitely many applications of these rules are terms.

Function symbols include:

• constants (as 0-ary function symbols)
• arithmetic operators like +, -, *, /.
• user-defined functions
• program variables

A 0-ary function symbol can denote a program variable in the environment of an imperative Predica program, perhaps associated with a database. For example a variable named s of type ShipmentsSystem. Within a term in a formula in logic, a program variable represents a function symbol not a logic variable. Note therefore that program variables are treated like constants and can never be captured (i.e. become bound using quantifiers ∃ and ∀ or in a set comprehension or a fold).