분지 유형 이론

틀:위키데이터 속성 추적 논리학에서 분지 유형 이론(分枝類型理論, 틀:Llang, 약자 RTT) 또는 복잡 유형 이론(複雜類型理論)은 단순 유형 이론보다 더 세분된 유형을 사용하는 논리 체계이다.틀:Rp

정의

다음과 같은 데이터가 주어졌다고 하자. (여기서 $\mathbb{N}$은 음이 아닌 정수의 집합이다.)

• 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 $(𝒱,{\le }_{𝒱})$. 그 원소를 변수(變數, 틀:Llang)라고 한다.
• 집합 $𝒜$. 그 원소를 개체(個體, 틀:Llang)라고 한다.
• 집합 $ℛ$ 및 함수 ${\mathrm{arity}}_{ℛ}:ℛ\to \mathbb{N}$. 각 $n\in \mathbb{N}$에 대하여, ${\mathrm{arity}}_{ℛ}^{-1}(n)$의 원소를 $n$항 관계($n$項關係, 틀:Llang)라고 한다.

그렇다면, $(𝒱,{\le }_{𝒱},𝒜,ℛ,{\mathrm{arity}}_{ℛ})$에 대한 분지 유형 이론은 다음과 같다.

분지 유형

분지 유형 이론에서 사용되는 분지 유형(分枝類型, 틀:Llang)과 이들의 차수(次數, 틀:Llang)는 다음과 같다.

• ${\iota }^0$은 0차 분지 유형이다.
• $d_1,\dots ,d_n$차 분지 유형 ${\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}$ 및 자연수 $d>\max \{d_1,\dots ,d_n\}$에 대하여, $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$는 $d$차 분지 유형이다.

이들 가운데, 술어적 분지 유형(述語的分枝類型, 틀:Llang)은 다음과 같다.

• ${\iota }^0$은 술어적 분지 유형이다.
• $d_1,\dots ,d_n$차 술어적 분지 유형 ${\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}$에 대하여, $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^{\max \{d_1,\dots ,d_n\}+1}$는 술어적 분지 유형이다. ($n=0$일 경우, $({)}^0$은 술어적 분지 유형이다.)

술어적 분지 유형은 차수를 생략한 채 $\iota$와 $({\tau }_1,\dots ,{\tau }_n)$으로 쓸 수 있다.

분지 유형 이론의 문맥(文脈, 틀:Llang)은 유한 개의 변수의 집합과 분지 유형의 집합 사이의 함수이다. 문맥은 변수 $x$와 분지 유형 ${\tau }^d$의 순서쌍 $x:{\tau }^d$들의 유한 집합으로 여길 수 있다. 이 경우, 문맥 $\mathrm{\Gamma }$의 정의역(定義域, 틀:Llang)은 다음과 같이 나타낼 수 있다.

$\mathrm{dom}(\mathrm{\Gamma })=\{x|x:{\tau }^d\in \mathrm{\Gamma }\}$

논리식

분지 유형 이론의 유사 논리식(類似論理式, 틀:Llang)은 다음과 같다.

• $n$항 관계 $R$ 및 변수 또는 개체 $p_1,\dots ,p_n$에 대하여, $R(p_1,\dots ,p_n)$은 유사 논리식이다.
  • $n=0$일 경우 유사 논리식 $R()$은 0항 관계 $R$와 구분되어야 한다. 분지 유형 이론에서 $n$항 관계는 유사 논리식이 아니다.
• 변수 $x$ 및 유한 개의 변수 또는 개체 또는 유사 논리식 $p_1,\dots ,p_n$에 대하여, $x(p_1,\dots ,p_n)$는 유사 논리식이다.
  • $n=0$일 경우 유사 논리식 $x()$은 변수 $x$와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
• 유사 논리식 $\varphi ,\psi$에 대하여, $\varphi \vee \psi$와 $\mathrm{\neg }\varphi$는 유사 논리식이다.
• 유사 논리식 $\varphi$ 및 그 자유 변수 $x\in \mathrm{FVar}(\varphi )$ 및 분지 유형 ${\tau }^d$에 대하여, $\mathrm{\forall }x:{\tau }^d\varphi$는 유사 논리식이다.

유사 논리식의 집합을 $𝒫$라고 하자. 또한 각 유사 논리식 $\varphi$에 대하여, $\mathrm{Var}(\varphi )$가 $\varphi$ 속에 등장하는 모든 변수의 집합이라고 하고,

$x_1^{\varphi }{<}_{𝒱}\cdots {<}_{𝒱}{x}_{|\mathrm{FVar}(\varphi )|}^{\varphi }$

가 $\varphi$의 모든 자유 변수라고 하자.

문맥 $\mathrm{\Gamma }$에서 개체 또는 유사 논리식 $\varphi$가 분지 유형 ${\tau }^d$를 갖는다는 것은 $\mathrm{\Gamma }⊢\varphi :{\tau }^d$로 표기하며, 다음과 같이 재귀적으로 정의된다. (여기서 $⊢\varphi :{\tau }^d$는 $\varnothing ⊢\varphi :{\tau }^d$를 뜻한다.)

• 개체 $a$에 대하여, $⊢a:{\iota }^0$이다.
• $n$항 관계 $R$ 및 개체 $a_1,\dots ,a_n$에 대하여, $⊢R(a_1,\dots ,a_n):({)}^1$이다.
• (논리 연산) 문맥 $\mathrm{\Gamma },\mathrm{\Delta }$ 및 유사 논리식 $\varphi ,\psi$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_m}{)}^d,({{{\tau }_1}^{\prime }}^{{d_1}^{\prime }},\dots ,{{{\tau }_n}^{\prime }}^{{d_n}^{\prime }}{)}^{d^{\prime }}$에 대하여, 만약 $\mathrm{\Gamma }⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_m}{)}^d$이며, $\mathrm{\Delta }⊢\psi :({{{\tau }_1}^{\prime }}^{{d_1}^{\prime }},\dots ,{{{\tau }_n}^{\prime }}^{{d_n}^{\prime }}{)}^{d^{\prime }}$이며, $\max \mathrm{dom}(\mathrm{\Gamma })<\min \mathrm{dom}(\mathrm{\Delta })$라면,틀:Mindent틀:Mindent이다.
• (한정) 문맥 $\mathrm{\Gamma }$ 및 유사 논리식 $\varphi$ 및 $i\in \{1,\dots ,|\mathrm{FVar}(\varphi )|\}$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$에 대하여, 만약 $\mathrm{\Gamma }\cup \{x_i^{\varphi }:{\tau }_i^{d_i}\}⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$라면,틀:Mindent이다.
• (매개 변수에 대한 추상화) 문맥 $\mathrm{\Gamma }$ 및 유사 논리식 $\varphi$ 및 그 개체이거나 유사 논리식인 매개 변수 $\psi \in \mathrm{Par}(\varphi )\cap (𝒜\cup 𝒫)$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d,{\tau }_{n+1}^{d_{n+1}}$ 및 변수 $y>\max \mathrm{dom}(\mathrm{\Gamma })$에 대하여, 만약 $\mathrm{\Gamma }⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$이며 $\mathrm{\Gamma }⊢\psi :{\tau }_{n+1}^{d_{n+1}}$이라면,틀:Mindent이다. 여기서 $(\varphi {)}_{\mathrm{\Gamma },\psi ,y}$는 $\varphi$에 등장하는 $\psi$와 α_Γ-동치인 각 매개 변수 ${\psi }^{\prime }$를 $y$로 대체하여 얻는 유사 논리식이다. (《수학 원리》에서 이는 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$가 술어적 분지 유형인 경우로 제한된다.)
• (논리식에 대한 추상화) 문맥 $\mathrm{\Gamma }$ 및 유사 논리식 $\varphi$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$ 및 변수 $y>\max \mathrm{dom}(\mathrm{\Gamma })$에 대하여, 만약 $\mathrm{\Gamma }⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$이라면,틀:Mindent이다. (이 경우 반드시 $|\mathrm{FVar}(\varphi )|=n$임을 보일 수 있다.) (《수학 원리》에서 이는 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$가 술어적 분지 유형인 경우로 제한된다.)
• (치환) 문맥 $\mathrm{\Gamma }$ 및 자유 변수를 갖는 유사 논리식 $\varphi$ 및 개체 또는 유사 논리식 $\psi$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$에 대하여, 만약 $\mathrm{\Gamma }\cup \{x_1^{\varphi }:{\tau }_1^{d_1}\}⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$이며, $\mathrm{\Gamma }⊢\psi :{\tau }_1^{d_1}$라면,틀:Mindent이다. (이 경우 $\varphi [\psi /x_1^{\varphi }]$는 반드시 정의됨을 보일 수 있다.)
• (약화) 문맥 $\mathrm{\Gamma },\mathrm{\Delta }$ 및 유사 논리식 $\varphi$ 및 분지 유형 ${\tau }^d$에 대하여, 만약 $\mathrm{\Gamma }⊢\varphi :{\tau }^d$이며, $\mathrm{\Gamma }\subseteq \mathrm{\Delta }$라면, $\mathrm{\Delta }⊢\varphi :{\tau }^d$이다.
• (순열) 문맥 $\mathrm{\Gamma }$ 및 유사 논리식 $\varphi$ 및 $i\in \{1,\dots ,|\mathrm{FVar}(\varphi )|\}$ 및 분지 유형 $({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$ 및 변수 $y>\max \mathrm{dom}(\mathrm{\Gamma })$에 대하여, 만약 $\mathrm{\Gamma }\cup \{x_i^{\varphi }:{\tau }_i^{d_i}\}⊢\varphi :({\tau }_1^{d_1},\dots ,{\tau }_n^{d_n}{)}^d$라면,틀:Mindent이다.

주어진 문맥 속에서, 유사 논리식의 분지 유형은 존재하지 않을 수 있으나, 만약 존재한다면 이는 유일하다. 주어진 유사 논리식은 서로 다른 문맥 속에서 서로 다른 분지 유형을 가질 수 있다. 유사 논리식 $\varphi$에 대하여, $\mathrm{\Gamma }⊢\varphi :{\tau }^d$인 문맥 $\mathrm{\Gamma }$과 ${\tau }^d$가 존재한다면, $\varphi$를 논리식(論理式, 틀:Llang)이라고 한다.

연산

자유 변수, 매개 변수, 재귀 매개 변수

분지 유형 이론의 각 유사 논리식 $\varphi$의 자유 변수(自由變數, 틀:Llang)의 집합 $\mathrm{FVar}(\varphi )$, 매개 변수(媒介變數, 틀:Llang)의 집합 $\mathrm{Par}(\varphi )$, 재귀 매개 변수(再歸媒介變數, 틀:Llang)의 집합 $\mathrm{RPar}(\varphi )$은 다음과 같이 재귀적으로 정의된다. (매개 변수와 재귀 매개 변수는 이름과 달리 변수가 아닐 수 있다.)

• $n$항 관계 $R$ 및 변수 또는 개체 $p_1,\dots ,p_n$에 대하여,틀:Mindent틀:Mindent틀:Mindent
• 변수 $x$ 및 유한 개의 변수 또는 개체 또는 유사 논리식 $p_1,\dots ,p_n$에 대하여,틀:Mindent틀:Mindent틀:Mindent
• 유사 논리식 $\varphi ,\psi$에 대하여,틀:Mindent틀:Mindent틀:Mindent틀:Mindent틀:Mindent틀:Mindent
• 유사 논리식 $\varphi$ 및 그 자유 변수 $x\in \mathrm{FVar}(\varphi )$에 대하여,틀:Mindent틀:Mindent틀:Mindent

치환

변수 또는 개체 또는 유사 논리식 $p,q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여,

$p⟨q_1/x_1,\dots ,q_k/x_k⟩=\{\begin{array}{cc}p& p\in ̸\{x_1,\dots ,x_k\}\\ q_j& p=x_j\end{array}$

이라고 하자.

유사 논리식 $\varphi$ 및 변수 또는 개체 또는 유사 논리식 $q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여, 치환 실례(置換實例, 틀:Llang) $\varphi [q_1/x_1,\dots ,q_k/x_k]$는 다음과 같이 재귀적으로 정의된다.

• $n$항 관계 $R$ 및 변수 또는 개체 $p_1,\dots ,p_n,q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여,틀:Mindent
• 변수 $x$ 및 및 변수 또는 개체 또는 유사 논리식 $p_1,\dots ,p_n,q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여,틀:Mindent
• 유사 논리식 $\varphi ,\psi$ 및 변수 또는 개체 또는 유사 논리식 $q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여,틀:Mindent틀:Mindent
• 유사 논리식 $\varphi$ 및 그 자유 변수 $x\in \mathrm{FVar}(\varphi )$ 및 분지 유형 ${\tau }^d$ 및 변수 또는 개체 또는 유사 논리식 $q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여,틀:Mindent

위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 $p_1,\dots ,p_n,q_1,\dots ,q_k$ 및 서로 다른 변수 $x_1,\dots ,x_k$에 대하여, 만약 $q_i\in 𝒜$이거나, $q_i\in 𝒫$이며 $q_i$의 자유 변수가 정확히 $n$개가 아닐 경우, $x_i(p_1,\dots ,p_n)[q_1/x_1,\dots ,q_k/x_k]$는 정의되지 않는다.

α-동치

두 유사 논리식 $\varphi ,\psi$에 대하여, 다음 조건을 만족시키는 전단사 함수 $f:𝒱\to 𝒱$가 존재한다면, $\varphi ,\psi$가 서로 α-순열 동치(α-順列同値, 틀:Llang)라고 한다.

• $\psi$는 $\varphi$에 등장하는 각 변수 $x$를 $f(x)$로 대체하여 얻는다. (특히, $f(\mathrm{Var}(\varphi ))=\mathrm{Var}(\psi )$이다.)

두 유사 논리식 $\varphi ,\psi$에 대하여, 다음 두 조건을 만족시키는 전단사 함수 $f:𝒱\to 𝒱$가 존재한다면, $\varphi ,\psi$가 서로 α-동치(α-同値, 틀:Llang)라고 한다.

• $\psi$는 $\varphi$에 등장하는 각 변수 $x$를 $f(x)$로 대체하여 얻는다. (특히, $f(\mathrm{Var}(\varphi ))=\mathrm{Var}(\psi )$이다.)
• $f{|}_{\mathrm{Var}(\varphi )}$는 증가 함수이다. 즉, 임의의 $x,y\in \mathrm{Var}(\varphi )$에 대하여, $x{<}_{𝒱}y⟺f(x){<}_{𝒱}f(y)$

두 유사 논리식 $\varphi ,\psi$ 및 문맥 $\mathrm{\Gamma }$에 대하여, 다음 세 조건을 만족시키는 전단사 함수 $f:𝒱\to 𝒱$가 존재한다면, $\varphi ,\psi$가 서로 α_Γ-동치(α_Γ-同値, 틀:Llang)라고 한다.

• $\psi$는 $\varphi$에 등장하는 각 변수 $x$를 $f(x)$로 대체하여 얻는다. (특히, $f(\mathrm{Var}(\varphi ))=\mathrm{Var}(\psi )$이다.)
• $f{|}_{\mathrm{Var}(\varphi )}$는 증가 함수이다. 즉, 임의의 $x,y\in \mathrm{Var}(\varphi )$에 대하여, $x{<}_{𝒱}y⟺f(x){<}_{𝒱}f(y)$
• 임의의 $x\in 𝒱$ 및 분지 유형 ${\tau }^d$에 대하여, $x:{\tau }^d\in \mathrm{\Gamma }⟺f(x):{\tau }^d\in \mathrm{\Gamma }$

역사

버트런드 러셀이 《수학 원리》에서 제시하였다.

각주

• 틀:저널 인용
• 틀:저널 인용
• 틀:저널 인용틀:깨진 링크