Term (logic)

자연 언어와 유사하게, 여기서 명사구(noun phrase)는 대상을 참조하고 전체 문장(sentence)은 사실을 지칭하며, 수학적 논리(mathematical logic)에서, 항(term)은 수학적 대상을 표시하고 공식(formula)은 수학적 사실을 표시합니다. 특히, 항은 공식의 구성요소로 나타납니다.

일-차(first-order) 항은 상수 기호, 변수(variables) 및 함수 기호(function symbols)로부터 재귀적으로 구성됩니다. 술어 기호(predicate symbol)를 항의 적절한 숫자에 적용함으로써 형성된 표현은 원자 수식(atomic formula)으로 불리며, 이것은 주어진 해석(interpretation)에서, 두-값의 논리(bivalent logics)에서 참(true) 또는 거짓(false)으로 평가됩니다. 예를 들어, $(x+1)*(x+1)$ 은 상수 1, 변수 $x$ , 및 이진 함수 기호 $+$ 와 $*$ 으로부터 만들어진 하나의 항입니다; 그것은 원자 수식 $(x+1)*(x+1)\geq 0$ 의 부분이며 $x$ 의 각 실수(real-number)의 값에 대해 참으로 평가됩니다.

논리(logic) 외에도, 항은 보편 대수학(universal algebra), 및 재-작성 시스템(rewriting system)에서 중요한 역할을 합니다.

Formal definition

변수 기호의 집합 V, 상수 기호의 집합 C 및 각각의 자연수 n ≥ 1에 대해, 역시 연산자 기호로 불리는, n-애리 함수 기호의 집합 F_n이 주어지면, (정렬되지 않은 일-차) 항 T의 집합은 다음 속성을 갖는 가장-작은 집합으로 재귀적으로 정의(recursively defined)됩니다: ^[1]

모든 각 변수 기호는 항입니다: V ⊆ T,
모든 각 상수 기호는 항입니다: C ⊆ T,
모든 각 n 항 t₁,...,t_n, 및 모든 각 n-애리 함수 기호 f ∈ F_n로부터, 더 큰 항 f(t₁, ..., t_n)이 세워질 수 있습니다.

직관적인, 유사-문법적(grammatical) 표기법을 사용하여, 이것은 때때로 다음처럼 쓰입니다: t ::= x | c | f(t₁, ..., t_n). 보통, 오직 처음 몇 개의 함수 기호 집합 F_n이 거주합니다. 잘-알려진 예제는 단항 함수 기호 sin, cos ∈ F₁, 및 이항 함수 기호 +, −, ⋅, / ∈ F₂이며, 반면에 삼항 연산(ternary operation)은 덜 알려져 있지만, 더 높은-애리티 함수는 물론입니다. 많은 저자들은 상수 기호를 0-애리 함수 기호 F₀로 고려하며, 따라서 그들에 대해 특별한 구문 클래스가 필요하지 않습니다.

항은 담론의 도메인(domain of discourse)의 수학적 대상을 나타냅니다. 상수 c는 해당 도메인에서 이름지은 대상을 나타내며, 변수 x는 해당 도메인에서 대상에 걸쳐 변화하고, n-애리 함수 f는 대상의 n-튜플(tuple)을 대상에 매핑합니다. 예를 들어, 만약 n ∈ V가 변수 기호, 1 ∈ C는 상수 기호이고, add ∈ F₂는 이항 함수 기호이면, 각각, 첫 번째, 두 번째, 및 세 번째 항 만드는 규칙에 의해, n ∈ T, 1 ∈ T, 및 (따라서) add(n, 1) ∈ T입니다. 후자 항은 보통 편의를 위해 중위 표기법 및 보다 공통적인 연산자 기호 +를 사용하여 n+1로 쓰입니다.

Term structure vs. representation

원래, 논리학자들은 항을 특정 만드는 규칙을 준수하는 문자 열(character string)로 정의했습니다.^[2] 어쨌든, 트리(tree)의 개념은 컴퓨터 과학에서 대중화되었으므로, 항을 트리로 생각하는 것이 더 편리한 것으로 판명되었습니다. 예를 들어, " $(n \cdot(n +1))/2$ ", " $((n \cdot(n +1)))/2$ ", 및 " ${\frac {n(n+1)}{2}}$ "와 같은 여러 구별되는 문자열은 같은 항을 나타내고, 같은 트리, 즉 위의 그림에서 왼쪽 트리에 해당합니다. 종이 위의 그래픽 표시에서 항의 트리 구조를 분리하면, 괄호 (구조가 아닌 오직 표현인 것)와 보이지 않는 곱셈 연산자 (표시에서가 아닌, 오직 표현에서 존재함)를 역시 쉽게 설명할 수 있습니다.

Structural equality

두 항이 만약 그것들이 같은 트리에 해당하면, 구조적으로, 문자적으로, 또는 구문적으로 같은 것으로 말합니다. 예를 들어, 위 그림에서 왼쪽과 오른쪽 트리는 구조적으로 비-같은 항이지만, 그것들은 "의미론적으로 같은" 것으로 여길 수 있는데 왜냐하면 그것들은 유리적 산술(rational arithmetic)에서 항상 같은 값으로 평가되기 때문입니다. 구조적 상등이 기호의 의미에 대한 임의의 지식없이 확인될 수 있지만, 의미론적 상등은 불가능합니다. 만약 함수 /가 예를 들어 유리적이 아니라 정수 나눗셈(integer division) 자름으로 해석되면, n=2에서 왼쪽과 오른쪽 항은 각각 3과 2로 평가됩니다. 구조상의 같은 항은 그것들의 변수 이름에서 일치해야 합니다.

대조적으로, 항 t는 만약 u가 t의 모든 변수의 이름을 일관되게 변경한 결과이면, 즉, 만약 일부 이름-변경 치환(renaming substitution) σ에 대해 u = tσ이면, 항 u의 이름-변경(renaming), 또는 변체(variant)라고 불립니다. 해당 경우에서, u는 역시 t의 이름-변경인데, 왜냐하면 이름-변경 치환 σ는 역 σ⁻¹, t = uσ⁻¹을 가지기 때문입니다. 항 둘 다는 그런-다음 같은 모듈로 이름-변경(equal modulo renaming)이라고 말합니다. 많은 문맥에서, 항에서 특정 변수 이름은 중요하지 않습니다. 예를 들어, 덧셈에 대해 교환성 공리는 x+y=y+x로 또는 a+b=b+a로 말할 수 있습니다; 그러한 경우에서 전체 공식은 이름-변경될 수 있지만, 임의의 부분-항은 보통 그렇지 않을 수 있습니다. 예를 들어, x+y=b+a는 교환성 공리의 유효한 버전이 아닙니다.^{[note 1]} ^{[note 2]}

Ground and linear terms

항 t의 변수의 집합은 vars(t)로 표시됩니다. 임의의 변수를 포함하지 않는 항은 기초 항(ground term)이라고 불립니다; 변수의 여러 번 발생을 포함하지 않는 항은 선형 항(linear term)이라고 불립니다. 예를 들어, 2+2는 기초 항이고 따라서 역시 선형 항이며, x⋅(n+1)는 선형 항, n⋅(n+1)는 비-선형 항입니다. 이들 속성은 예를 들어 항 다시-쓰기(term rewriting)에서 중요합니다.

함수 기호에 대한 시그너츠(signature)가 주어지면, 모든 항의 집합은 자유(free) 항 대수(term algebra)를 형성합니다. 모든 기초 항의 집합은 초기(initial) 항 대수(term algebra)를 형성합니다.

상수의 숫자를 f₀로, i-항 함수 기호의 숫자를 f_i로 줄여-쓰면, h까지 높이의 구별되는 기초 항의 숫자 θ_h는 다음 재귀 공식에 의해 계산될 수 있습니다:

θ₀ = f₀인데, 왜냐하면 높이 0의 기초 항은 오직 상수일 수 있기 때문입니다,
$\theta _{h+1}=\sum _{i=0}^{\infty }f_{i}\cdot \theta _{h}^{i}$ 인데, 왜냐하면 h+1까지 높이의 기초 항은 h까지 높이의 임의의 i 기초 항을 합성함으로써 얻어질 수 있으며, i-항 근 함수 기호를 사용합니다. 그 합은 만약 보통 경우인, 오직 유한 숫자의 상수와 함수 기호가 있으면 유한 값을 가집니다.

Building formulas from terms

각 자연수 n ≥ 1에 대해 n-항 관계 기호의 집합 R_n이 주어지면, (비-정렬된 일-차) 원자 공식은 n-항 관계 기호를 n 항에 적용함으로써 얻습니다. 함수 기호에 대해, 관계 기호 집합 R_n은 보통 오직 작은 n에 대해 비-빈 것입니다. 수학적 논리에서, 보다 복잡한 공식(formulas)은 논리적 연결(logical connective) 및 한정어(quantifiers)를 사용하여 원자 공식에서 작성됩니다. 예를 들어, ℝ이 실수(real number)의 집합을 나타내는 것으로 놓으면, ∀x: x ∈ ℝ ⇒ (x+1)⋅(x+1) ≥ 0은 복소수(complex number)의 대수에서 참으로 평가되는 수학적 공식입니다. 원자 공식은 만약 그것이 기초 항으로부터 완전히 구축되면 기초라고 불립니다; 주어진 함수와 술어 기호의 집합에서 합성-가능 모든 기초 원자 공식은 이들 기호 집합에 대해 에르브랑 기저(Herbrand base)을 구성합니다.

Operations with terms

항은 트리 계층의 구조를 갖기 때문에, 그것의 각 노드에 위치, 또는 경로가 할당될 수 있으며, 즉 계층에서 노드의 위치를 나타내는 자연수의 문자열가 할당될 수 있습니다. 공통적으로 ε으로 표시되는, 빈 문자열은 루트 노드에 할당됩니다. 검은색 항 내의 위치 문자열은 그림에서 빨간색으로 표시됩니다.
항 t의 각 위치 p에서, 고유한 부분-항(subterm)으로 시작하며, 공통적으로 $t | p$ 에 의해 표시됩니다. 예를 들어, 그림에서 검은색 항의 위치 122에서, 부분항 a+2는 자체의 루트를 가집니다. 관계 "의 부분항입니다"는 항의 집합에 대한 부분 순서(partial order)입니다; 그것은 반사적(reflexive)인데 왜냐하면 각 항은 자명하게 자체의 부분항입니다.
항 t에서 위치 p에서 부분항을 새로운 항 u로 대체함으로써 얻어진 항은 공통적으로 $t [u] p$ 로 표시됩니다. 항 $t [u] p$ 는 역시 용어 u를 항-같은 대상 $t [.]$ 의 일반화된 연쇄로부터 결과로 보일 수 있습니다; 후자는 컨텍스트(context), 또는 구멍을 가진 항(term with a hole) ("."로 표시됨; 그것의 위치는 p임)이라고 불리며, 이것에서 u는 삽입된(embedded) 것으로 말합니다. 예를 들어, 만약 t가 그림에서 검은색 항이면, $t [b +1] 12$ 는 항 ${\frac {a*(b+1)}{1*(2*3)}}$ 의 결과입니다. 후자 항은 역시 항 $b +1$ 를 컨텍스트 ${\frac {a*(\;.\;)}{1*(2*3)}}$ 로의 삽입의 결과입니다. 비공식적 의미에서, 인스턴트화(instantiating) 및 삽입의 연산은 서로 전환입니다: 전자는 항의 맨 아래에서 함수 기호를 첨부하지만, 후자는 맨 위에 그것들을 첨부합니다. 포괄 순서화(encompassment ordering)는 항과 양쪽 변에 첨부된 임의의 결과를 관련시킵니다.
용어의 각 노드에, 그것의 깊이(depth) (일부 저자에 의해 높이(height)라고 불림)는 할당될 수 있습니다. 즉, 루트로부터의 그것의 거리 (가장자리의 숫자)를 할당할 수 있습니다. 이 설정에서, 노드의 깊이는 항상 그것의 위치 문자열의 길이와 같습니다. 그림에서, 검은색 항에서 깊이 수준은 녹색으로 표시됩니다.
항의 크기(size)는 공통적으로 그것의 노드의 숫자를 참조하거나, 동등하게, 괄호없이 기호를 세는, 항의 쓰인 표현의 길이를 참조합니다. 그림에서 검은색과 파란색 항은, 각각, 크기 15와 5를 가집니다.
항 u는, 만약 u의 대체 예제가 t의 부분항과 구조적으로 같으면, 또는 공식적으로, 만약 t에서 일부 위치 p와 일부 대체 σ에 대해 $u σ = t | p$ 이면, 항 t와 짝맞춥니다(match). 이 경우에서, u, t, 및 σ는, 각각, 패턴 항(pattern term), 주어 항(subject term), 및 짝맞추는 대체(matching substitution)이라고 불립니다. 그림에서, 파란색 패턴 항 $x*(y*z)$ 는 위치 1에서 검은색 주어 항과 짝맞추며, 짝맞추는 대체 ${x \mapsto a, y \mapsto a +1, z \mapsto a +2 }$ 는 그것들의 검은색 대체에 바로 왼쪽에 있는 파란색 변수로 표시됩니다. 직관적으로, 패턴은, 그것의 변수를 제외하고, 주어에서 포함되어야 합니다; 만약 변수가 패턴에서 여러 번 발생하면, 같은 부분항은 주어의 각 위치에서 요구됩니다.
항을 통합하는 것(unifying terms)
항 다시-쓰기(term rewriting)

Related concepts

Sorted terms

담화의 도메인이 기본적으로 다른 종류의 원소를 포함하면, 그에 따라 모든 항의 집합을 쪼개는 것이 유용합니다. 이 끝을 위해, 종류 (때때로 역시 유형이라고 불림)는 각 변수와 각 상수 기호, 및 각 함수 기호에 도메인 종류와 치역 종류의 선언에 할당됩니다.^{[note 3]} 정렬된 항(sorted term) f(t₁,...,t_n)은 만약 $i$ 번째 부분항의 종류가 선언된 $i$ 번째 도메인 종류 f와 일치하면 오직 정렬된 부분항 t₁,...,t_n에서 구성될 수 있습니다. 그러한 항은 역시 바른-정렬된(well-sorted) 것이라고 불립니다; 다른 항 (즉, 오직 비-정렬된 규칙(unsorted rules)을 따름)은 잘못-정렬된(ill-sorted) 것이라고 불립니다.

예를 들어, 벡터 공간(vector space)이 스칼라 숫자의 결합된 필드(field)와 함께 옵니다. W와 N이, 각각, 벡터와 숫자의 종류를 표시한다고 놓고, V_W와 V_N를 각각 벡터와 숫자 변수의 집합으로 놓고, C_W와 C_N를 각각 벡터와 숫자 상수의 집합으로 놓습니다. 그런-다음 예를 들어 ${\vec {0}}\in C_{W}$ 와 $0 \in C N$ , 및 벡터 덧셈, 스칼라 곱셈, 및 안의 곱은 각각 $+:W\times W\to W,*:W\times N\to W$ , 및 $\langle .,.\rangle :W\times W\to N$ 으로 선언됩니다. 변수 기호 ${\vec {v}},{\vec {w}}\in V_{W}$ 와 $a, b \in V N$ 를 가정하면, 항 $\langle ({\vec {v}}+{\vec {0}})*a,{\vec {w}}*b\rangle$ 은 잘-정렬된 것이지만, ${\vec {v}}+a$ 는 그렇지 않습니다 (왜냐하면 +는 두 번째 인수로 종류 N의 항을 받아들이기 않기 때문입니다). $a*{\vec {v}}$ 를 잘-정렬된 항으로 만들기 위해, 추가적인 선언 $*:N\times W\to W$ 이 요구됩니다. 여러 선을 가지는 함수 기호는 오버로딩된(overloaded) 것이라고 불립니다.

여기에 설명된 많은-정렬된 프레임워크(many-sorted framework)의 확장을 포함하여, 자세한 정보에 대해 많은-정렬된 논리(many-sorted logic)를 참조하십시오.

Lambda terms

Terms with bound variables
Notation example	Bound variables	Free variables	Written as lambda-term
$lim n \to\infty 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))

Motivation

테이블에서 표시된 수학적 표기법은 위에(above) 정의된 것으로 일-차 항의 개요에 적합하지 않는데, 왜냐하면 그것들 모두는 자체 지역, 또는 경계, 표기법의 범위 밖에 나타날 수 없는 변수를 도입하며, 예를 들어, $t\cdot \int _{a}^{b}\sin(k\cdot t)\;dt$ 는 의미가 없습니다. 반면에, 다른 변수는, 자유로 참조되며, 보통의 일-차 항 변수로 작용하며, 예를 들어, $k\cdot \int _{a}^{b}\sin(k\cdot t)\;dt$ 는 의미가 있습니다.

모든 이들 연산자는 그들 인수 중 하나로 값 항이 아닌 함수를 취하는 것으로 보일 수 있습니다. 예를 들어, lim 연산자는 수열, 즉, 양의 정수에서, 예를 들어, 실수로의 매핑으로 적용됩니다. 또 다른 예제로, 테이블의 두 번째 예제, ∑를 구현하는 C 함수는 함수 포인터 인수를 갖습니다 (아래 코드를 참조하십시오).

람다 항(Lambda term)은 lim, ∑, ∫, 등에 대한 인수로 제공되는 익명 함수(anonymous function)를 표시하기 위해 사용될 수 있습니다.

예를 들어, 아래 C 프로그램에서 함수 square는 람다 항 λi. i²로 익명적으로 쓸 수 있습니다. 일반적인 합 연산자 ∑는 그런-다음 아래쪽 경계 값, 위쪽 경계 값과 합산해야 할 함수를 취하는 삼항 함수 기호로 여길 수 있습니다. 그것의 후자 인수로 인해, ∑ 연산자는 이-차 함수 기호라고 불립니다. 또 다른 예제로, 람다 항 λn. x/n은 각각 1, 2, 3, ...을 x/1, x/2, x/3, ...로 매핑하는 함수를 표시하며, 즉, 그것은 수열(sequence) (x/1, x/2, x/3, ...)을 표시합니다. lim 연산자는 그러한 수열을 취하고 (만약 정의되면) 그것의 극한을 반환합니다.

테이블의 가장-오른쪽 열은 각 수학적 표기법 예제가 람다 항으로 표현될 수 있는 방법을 나타내며, 역시 공통적인 중위(infix) 연산자를 접두(prefix) 형식으로 변환합니다.

int sum(int lwb, int upb, int fct(int)) {    // implements general sum operator
    int res = 0;
    for (int i=lwb; i<=upb; ++i)
        res += fct(i);
    return res;
}

int square(int i) { return i*i; }            // implements anonymous function (lambda i. i*i); however, C requires a name for it

#include <stdio.h>
int main(void) {
    int n;
    scanf(" %d",&n);
    printf("%d\n", sum(1, n, square));        // applies sum operator to sum up squares
    return 0;
}

Notes

^ 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 type bool rather than e.g. int, cf. #Sorted terms below).
^ Renaming of the commutativity axiom can be viewed as alpha-conversion on the universal 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 the Many-sorted signatures section of the Signature (logic) article.

References

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

[3] 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 type bool rather than e.g. int, cf. #Sorted terms below).

[4] Renaming of the commutativity axiom can be viewed as alpha-conversion on the universal 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.

[5] I.e., "symbol type" in the Many-sorted signatures section of the Signature (logic) article.

[1] 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

[2] Hermes, Hans (1973). Introduction to Mathematical Logic. Springer London. ISBN 3540058192. ISSN 1431-4657.; here: Sect.II.1.3

[1]

[2]

[note 1]

[note 2]

[note 3]