Movatterモバイル変換

Term (logic)

From Wikipedia, the free encyclopedia

Components of a mathematical or logical formula

Inmathematical logic, aterm is an arrangement of dependent/bound symbols that denotes amathematical object within an expression/formula. In particular, terms appear as components of a formula. This is analogous to natural language, where anoun phrase refers to an object and a wholesentence refers to a fact.

Afirst-order term isrecursively constructed from constant symbols,variable symbols, andfunction symbols.An expression formed by applying apredicate symbol to an appropriate number of terms is called anatomic formula, which evaluates totrue orfalse inbivalent logics, given aninterpretation.For example,⁠ $(x+1)*(x+1)$ ⁠ is a term built from the constant 1, the variablex, and the binary function symbols⁠ $+$ ⁠ and⁠ $*$ ⁠; it is part of the atomic formula⁠ $(x+1)*(x+1)\geq 0$ ⁠ which evaluates to true for eachreal-numbered value ofx.

Besides inlogic, terms play important roles inuniversal algebra, andrewriting systems.

Definition

[edit]

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

Given a setV of variable symbols, a setC of constant symbols and setsF_n ofn-ary function symbols, also called operator symbols, for each natural numbern ≥ 1, the set of (unsorted first-order) termsT isrecursively defined to be 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 everyn termst₁,...,t_n, and everyn-ary function symbolf ∈F_n, a larger termf(t₁, ...,t_n) can be built.

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

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

Thesignature of the term language describes which function symbol setsF_n are inhabited. Well-known examples are the unary function symbolssin,cos ∈F₁, and the binary function symbols +, −, ⋅, / ∈F₂.Ternary operations and higher-arity functions are possible but uncommon in practice. Many authors consider constant symbols as 0-ary function symbolsF₀, thus needing no special syntactic class for them.

A term denotes a mathematical object from thedomain of discourse. A constantc denotes a named object from that domain, a variablex ranges over the objects in that domain, and ann-ary functionf mapsn-tuples of objects to objects. For example, ifn ∈V is a variable symbol, 1 ∈C is a constant symbol, andadd ∈F₂ is a binary function symbol, thenn ∈T, 1 ∈T, and (hence)add(n, 1) ∈T by the first, second, and third term building rule, respectively. The latter term is usually written asn+1, usinginfix notation and the more common operator symbol + for convenience.

Term structure vs. representation

[edit]

Originally, logicians defined a term to be acharacter string adhering to certain building rules.^[2] However, since the concept oftree became popular in computer science, it turned out to be more convenient to think of a term as a tree. For example, several distinct character strings, like "(n⋅(n+1))/2", "((n⋅(n+1)))/2", and " ${\frac {n(n+1)}{2}}$ ", denote the same term and correspond to the same tree, viz. the left tree in the above picture.Separating the tree structure of a term from its graphical representation on paper, it is also easy to account for parentheses (being only representation, not structure) and invisible multiplication operators (existing only in structure, not in representation).

Structural equality

[edit]

Two terms are said to bestructurally,literally, orsyntactically equal if they correspond to the same tree. For example, the left and the right tree in the above picture are structurallyunequal terms, although they might be considered "semantically equal" as they always evaluate to the same value inrational arithmetic. While structural equality can be checked without any knowledge about the meaning of the symbols, semantic equality cannot. If the function / is e.g. interpreted not as rational but astruncating integer division, then atn=2 the left and right term evaluates to 3 and 2, respectively.Structurally equal terms need to agree in their variable names.

In contrast, a termt is called arenaming, or avariant, of a termu if the latter resulted from consistently renaming all variables of the former, i.e. ifu =tσ for somerenaming substitution σ. In that case,u is a renaming oft, too, since a renaming substitution σ has an inverse σ⁻¹, andt = uσ⁻¹. Both terms are then also said to beequal modulo renaming. In many contexts, the particular variable names in a term don't matter, e.g. the commutativity axiom for addition can be stated asx+y=y+x or asa+b=b+a; in such cases the whole formula may be renamed, while an arbitrary subterm usually may not, e.g.x+y=b+a is not a valid version of the commutativity axiom.^{[note 1]}^{[note 2]}

Ground and linear terms

[edit]

The set of variables of a termt is denoted byvars(t).A term that doesn't contain any variables is called aground term; a term that doesn't contain multiple occurrences of a variable is called alinear 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 in, for example,term rewriting.

Given asignature for the function symbols, the set of all terms forms thefree term algebra. The set of all ground terms forms theinitial term algebra.

Abbreviating the number of constants asf₀, and the number ofi-ary function symbols asf_i, the number θ_h of distinct ground terms of a height up toh can be computed by the following recursion formula:

θ₀ =f₀, since a ground term of height 0 can only be a constant,
$\theta _{h+1}=\sum _{i=0}^{\infty }f_{i}\cdot \theta _{h}^{i}$ , since a ground term of height up toh+1 can be obtained by composing anyi ground terms of height up toh, using ani-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.

Building formulas from terms

[edit]

Given a setR_n ofn-ary relation symbols for each natural numbern ≥ 1, an (unsorted first-order) atomic formula is obtained by applying ann-ary relation symbol ton terms. As for function symbols, a relation symbol setR_n is usually non-empty only for smalln. In mathematical logic, more complexformulas are built from atomic formulas usinglogical connectives andquantifiers. For example, letting $\mathbb {R}$ denote the set ofreal numbers, ∀x:x ∈ $\mathbb {R}$ ⇒ (x+1)⋅(x+1) ≥ 0 is a mathematical formula evaluating to true in the algebra ofcomplex numbers.An atomic formula is called ground if it is built entirely from ground terms; all ground atomic formulas composable from a given set of function and predicate symbols make up theHerbrand base for these symbol sets.

Operations with terms

[edit]

Tree structure of black example term ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$ , with blue redex⁠ $x*(y*z)$ ⁠

{\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}} — Tree structure of black example term ${\frac {a*((a+1)*(a+2))}{1*(2*3)}}$ , with blue redex⁠ $x*(y*z)$ ⁠

Since a term has the structure of a tree hierarchy, to each of its nodes aposition, orpath, can be assigned, that is, a string of natural numbers indicating the node's place in the hierarchy. The empty string, commonly denoted by ε, is assigned to the root node. Position strings within the black term are indicated in red in the picture.
At each positionp of a termt, a uniquesubterm starts, which is commonly denoted byt|_p. For example, at position 122 of the black term in the picture, the subterma+2 has its root. The relation"is a subterm of" is apartial order on the set of terms; it isreflexive since each term is trivially a subterm of itself.
The term obtained byreplacing in a termt the subterm at a positionp by a new termu is commonly denoted byt[u]_p. The termt[u]_p can also be viewed as resulting from a generalized concatenation of the termu with a term-like objectt[.]; the latter is called acontext, or aterm with a hole (indicated by "."; its position beingp), in whichu is said to beembedded. For example, ift is the black term in the picture, thent[b+1]₁₂ results in the term ${\frac {a*(b+1)}{1*(2*3)}}$ . The latter term also results from embedding the termb+1 into the context ${\frac {a*(\;.\;)}{1*(2*3)}}$ . In an informal sense, the operations ofinstantiating and embedding are converse to each other: while the former appends function symbols at the bottom of the term, the latter appends them at the top. Theencompassment ordering relates a term and any result of appends on both sides.
To each node of a term, itsdepth (calledheight by some authors) can be assigned, i.e. its distance (number of edges) from the root. In this setting, the depth of a node always equals the length of its position string. In the picture, depth levels in the black term are indicated in green.
Thesize of a term commonly refers to the number of its nodes, or, equivalently, to the length of the term's written representation, counting symbols without parentheses. The black and the blue term in the picture has the size 15 and 5, respectively.
A termumatches a termt, if a substitution instance ofu structurally equals a subterm oft, or formally, ifuσ =t|_p for some positionp int and some substitution σ. In this case,u,t, and σ are called thepattern term, thesubject term, and thematching substitution, respectively. In the picture, the blue pattern term⁠ $x*(y*z)$ ⁠ matches the black subject term at position 1, with the matching substitution {x ↦a,y ↦a+1, z ↦a+2 } indicated by blue variables immediately left to their black substitutes. Intuitively, the pattern, except for its variables, must be contained in the subject; if a variable occurs multiple times in the pattern, equal subterms are required at the respective positions of the subject.
unifying terms
term rewriting

Related concepts

[edit]

Sorted terms

[edit]

Main article:Many-sorted logic

When the domain of discourse contains elements of basically different kinds, it is useful to split the set of all terms accordingly. To this end, asort (sometimes also calledtype) is assigned to each variable and each constant symbol, and a declaration^{[note 3]} of domain sorts and range sort to each function symbol. Asorted termf(t₁,...,t_n) may be composed from sorted subtermst₁,...,t_n only if theith subterm's sort matches the declaredith domain sort off. Such a term is also calledwell-sorted; any other term (i.e. obeying theunsorted rules only) is calledill-sorted.

For example, avector space comes with an associatedfield of scalar numbers. LetW andN denote the sort of vectors and numbers, respectively, letV_W andV_N be the set of vector and number variables, respectively, andC_W andC_N the set of vector and number constants, respectively. Then e.g. ${\vec {0}}\in C_{W}$ and0 ∈C_N, and the vector addition, the scalar multiplication, and the inner product is declared as⁠ $+:W\times W\to W,*:W\times N\to W$ ⁠, and⁠ $\langle .,.\rangle :W\times W\to N$ ⁠, respectively. Assuming variable symbols ${\vec {v}},{\vec {w}}\in V_{W}$ anda,b ∈V_N, the term $\langle ({\vec {v}}+{\vec {0}})*a,{\vec {w}}*b\rangle$ is well-sorted, while ${\vec {v}}+a$ is not (since + doesn't accept a term of sortN as 2nd argument). In order to make $a*{\vec {v}}$ a well-sorted term, an additional declaration⁠ $*:N\times W\to W$ ⁠ is required. Function symbols having several declarations are calledoverloaded.

Seemany-sorted logic for more information, including extensions of themany-sorted framework described here.

Lambda terms

[edit]

Terms with bound variables
Notation example	Bound variables	Free variables	Written as lambda-term
limn→∞x/n	n	x	limit(λn.div(x,n))
$\sum _{i=1}^{n}i^{2}$	i	n	sum(1,n,λi.power(i,2))
$\int _{a}^{b}\sin(k\cdot t)dt$	t	a,b,k	integral(a,b,λt.sin(k⋅t))

Main article:Lambda term

Motivation

[edit]

Mathematical notations as shown in the table do not fit into the scheme of a first-order term as definedabove, as they all introduce an ownlocal, orbound, variable that may not appear outside the notation's scope, e.g. $t\cdot \int _{a}^{b}\sin(k\cdot t)\;dt$ doesn't make sense. In contrast, the other variables, referred to asfree, behave like ordinary first-order term variables, e.g. $k\cdot \int _{a}^{b}\sin(k\cdot t)\;dt$ does make sense.

All these operators can be viewed as taking a function rather than a value term as one of their arguments. For example, thelim operator is applied to a sequence, i.e. to a mapping from positive integer to e.g. real numbers. As another example, aC function to implement the second example from the table, Σ, would have a function pointer argument (see box below).

Lambda terms can be used to denoteanonymous functions to be supplied as arguments tolim, Σ, ∫, etc.

For example, the functionsquare from the C program below can be written anonymously as a lambda term λi.i². The general sum operator Σ can then be considered as a ternary function symbol taking a lower bound value, an upper bound value and a function to be summed-up. Due to its latter argument, the Σ operator is called asecond-order function symbol.As another example, the lambda term λn.x/n denotes a function that maps 1, 2, 3, ... tox/1,x/2,x/3, ..., respectively, that is, it denotes thesequence (x/1,x/2,x/3, ...). Thelim operator takes such a sequence and returns its limit (if defined).

The rightmost column of the table indicates how each mathematical notation example can be represented by a lambda term, also converting commoninfix operators intoprefix form.

intsum(intlwb,intupb,intfct(int)){// implements general sum operatorintres=0;for(inti=lwb;i<=upb;++i)res+=fct(i);returnres;}intsquare(inti){returni*i;}// implements anonymous function (lambda i. i*i); however, C requires a name for it#include<stdio.h>intmain(void){intn;scanf(" %d",&n);printf("%d\n",sum(1,n,square));// applies sum operator to sum up squaresreturn0;}

Definition

[edit]

This sectionneeds expansion. You can help byadding missing information.(April 2021)

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

every variable symbolx∈V is a lambda term;
ifx∈V is a variable symbol andt is a lambda term, then λx.t is also a lambda term (abstraction);
ift₁ andt₂ are lambda terms, then (t₁t₂ ) is also a lambda term (application).

The above motivating examples also used some constants likediv,power, etc. which are, however, not admitted in pure lambda calculus.

Intuitively, the abstraction λx.t denotes a unary function that returnst when givenx, while the application (t₁t₂ ) denotes the result of calling the functiont₁ with the inputt₂. For example, the abstraction λx.x denotes the identity function, while λx.y denotes the constant function always returningy. The lambda term λx.(xx) takes a functionx and returns the result of applyingx to itself.

Notes

[edit]

^Since atomic formulas can be viewed as trees, too, and renaming is essentially a concept on trees, atomic (and, more generally,quantifier-free) formulas can be renamed in a similar way as terms. In fact, some authors consider a quantifier-free formula as a term (of typebool rather than e.g.int, cf.#Sorted terms below).
^Renaming of the commutativity axiom can be viewed asalpha-conversion on theuniversal closure of the axiom: "x+y=y+x" actually means "∀x,y:x+y=y+x", which is synonymous to "∀a,b:a+b=b+a"; see also#Lambda terms below.
^I.e., "symbol type" in theMany-sorted signatures section of the Signature (logic) article.

References

[edit]

Franz Baader;Tobias Nipkow (1999).Term Rewriting and All That. Cambridge University Press. pp. 1–2 and 34–35.ISBN 978-0-521-77920-3.

^C.C. Chang;H. Jerome Keisler (1977).Model Theory. Studies in Logic and the Foundation of Mathematics. Vol. 73. North Holland.; here: Sect.1.3
^Hermes, Hans (1973).Introduction to Mathematical Logic. Springer London.ISBN 3540058192.ISSN 1431-4657.; here: Sect.II.1.3

Mathematical logic

General

Theorems
(list),
paradoxes

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types ofsets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps, cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive