분지 유형 이론

분지 유형 이론(分枝類型理論, 영어: ramified type theory, 약자 RTT) 또는 복잡 유형 이론(複雜類型理論)은 단순 유형 이론보다 더 세분된 유형을 다루는 유형 이론이다.^{:Chapter 2}

정의

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

• 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 $({\mathcal {V}},\leq _{\mathcal {V}})$. 그 원소를 변수(變數, 영어: variable)라고 한다.
• 집합 ${\mathcal {A}}$. 그 원소를 개체(個體, 영어: individual)라고 한다.
• 집합 ${\mathcal {R}}$ 및 함수 $\operatorname {arity} _{\mathcal {R}}\colon {\mathcal {R}}\to \mathbb {N}$. 각 $n\in \mathbb {N}$에 대하여, $\operatorname {arity} _{\mathcal {R}}^{-1}(n)$의 원소를 $n$항 관계($n$項關係, 영어: $n$-ary relation)라고 한다.

그렇다면, $({\mathcal {V}},\leq _{\mathcal {V}},{\mathcal {A}},{\mathcal {R}},\operatorname {arity} _{\mathcal {R}})$에 대한 분지 유형 이론은 다음과 같다.

분지 유형

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

• $\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$차 분지 유형이다.

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

• $\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}$는 술어적 분지 유형이다.

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

변수 $x$와 분지 유형 $\tau ^{d}$의 순서쌍을 $x{:}\tau ^{d}$로 표기하자. 이러한 순서쌍들의 집합을 분지 유형 이론의 문맥(文脈, 영어: context)이라고 한다. 문맥 $\Gamma$의 정의역(定義域, 영어: domain)은 다음과 같다.

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

논리식

분지 유형 이론의 유사 논리식(類似論理式, 영어: pseudoformula)는 다음과 같다.

• $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$와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
• 유사 논리식 $\phi ,\psi$에 대하여, $\phi \lor \psi$와 $\lnot \phi$는 유사 논리식이다.
• 유사 논리식 $\phi$ 및 그 자유 변수 $x\in \operatorname {FVar} (\phi )$ 및 분지 유형 $\tau ^{d}$에 대하여, $\forall x{:}\tau ^{d}\phi$는 유사 논리식이다.

유사 논리식의 집합을 ${\mathcal {P}}$라고 하자.

연산

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

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

• $n$항 관계 $R$ 및 변수 또는 개체 $p_{1},\dots ,p_{n}$에 대하여,
  $$\operatorname {FVar} (R(p_{1},\dots ,p_{n}))={\mathcal {V}}\cap \{p_{1},\dots ,p_{n}\}$$
  $$\operatorname {Par} (R(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}$$
  $$\operatorname {RPar} (R(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}$$
• 변수 $x$ 및 유한 개의 변수 또는 개체 또는 유사 논리식 $p_{1},\dots ,p_{n}$에 대하여,
  $$\operatorname {FVar} (x(p_{1},\dots ,p_{n}))={\mathcal {V}}\cap \{x,p_{1},\dots ,p_{n}\}$$
  $$\operatorname {Par} (x(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}$$
  $$\operatorname {RPar} (x(p_{1},\dots ,p_{n}))=\{p_{1},\dots ,p_{n}\}\cup \bigcup _{\phi \in {\mathcal {P}}\cap \{p_{1},\dots ,p_{n}\}}\operatorname {RPar} (\phi )$$
• 유사 논리식 $\phi ,\psi$에 대하여,
  $$\operatorname {FVar} (\phi \lor \psi )=\operatorname {FVar} (\phi )\cup \operatorname {FVar} (\psi )$$
  $$\operatorname {Par} (\phi \lor \psi )=\operatorname {Par} (\phi )\cup \operatorname {Par} (\psi )$$
  $$\operatorname {RPar} (\phi \lor \psi )=\operatorname {RPar} (\phi )\cup \operatorname {RPar} (\psi )$$
  $$\operatorname {FVar} (\lnot \phi )=\operatorname {FVar} (\phi )$$
  $$\operatorname {Par} (\lnot \phi )=\operatorname {Par} (\phi )$$
  $$\operatorname {RPar} (\lnot \phi )=\operatorname {RPar} (\phi )$$
• 유사 논리식 $\phi$ 및 그 자유 변수 $x\in \operatorname {FVar} (\phi )$에 대하여,
  $$\operatorname {FVar} (\forall x\phi )=\operatorname {FVar} (\phi )\setminus \{x\}$$
  $$\operatorname {Par} (\forall x\phi )=\operatorname {Par} (\phi )$$
  $$\operatorname {RPar} (\forall x\phi )=\operatorname {RPar} (\phi )$$

치환

변수 또는 개체 또는 유사 논리식 $p,q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여,

$p\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle ={\begin{cases}q_{j}&p=x_{j}\\p&p\not \in \{x_{1},\dots ,x_{k}\}\end{cases}}$

이라고 하자.

유사 논리식 $\phi$ 및 변수 또는 개체 또는 유사 논리식 $q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여, 치환 실례(置換實例, 영어: substitutional instance) $\phi [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}$에 대하여,
  $$R(p_{1},\dots ,p_{n})[q_{1}/x_{1},\dots ,q_{k}/x_{k}]=R(p_{1}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle ,\dots ,p_{n}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle )$$
• 변수 $x$ 및 및 변수 또는 개체 또는 유사 논리식 $p_{1},\dots ,p_{n},q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여,
  $$x(p_{1},\dots ,p_{n})[q_{1}/x_{1},\dots ,q_{k}/x_{k}]={\begin{cases}q_{i}[p_{1}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle /y_{1},\dots ,p_{n}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle /y_{n}]&x=x_{i},\;q_{i}\in {\mathcal {P}},\;\operatorname {FVar} (q_{i})=\{y_{1}<\cdots <y_{n}\}\\x(p_{1}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle ,\dots ,p_{n}\langle q_{1}/x_{1},\dots ,q_{k}/x_{k}\rangle )&x\not \in \{x_{1},\dots ,x_{k}\}\end{cases}}$$
• 유사 논리식 $\phi ,\psi$ 및 변수 또는 개체 또는 유사 논리식 $q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여,
  $$(\phi \lor \psi )[q_{1}/x_{1},\dots ,q_{k}/x_{k}]=\phi [q_{1}/x_{1},\dots ,q_{k}/x_{k}]\lor \psi [q_{1}/x_{1},\dots ,q_{k}/x_{k}]$$
  $$(\lnot \phi )[q_{1}/x_{1},\dots ,q_{k}/x_{k}]=\lnot (\phi [q_{1}/x_{1},\dots ,q_{k}/x_{k}])$$
• 유사 논리식 $\phi$ 및 그 자유 변수 $x\in \operatorname {FVar} (\phi )$ 및 분지 유형 $\tau ^{d}$ 및 변수 또는 개체 또는 유사 논리식 $q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여,
  $$(\forall x{:}\tau ^{d}\phi )[q_{1}/x_{1},\dots ,q_{k}/x_{k}]={\begin{cases}\forall x{:}\tau ^{d}(\phi [q_{1}/x_{1},\dots ,q_{k}/x_{k}])&x\not \in \{x_{1},\dots ,x_{n}\}\\\forall x{:}\tau ^{d}(\phi [q_{1}/x_{1},\dots ,q_{i-1}/x_{i-1},q_{i+1}/x_{i+1},\dots ,q_{k}/x_{k}])&x=x_{i}\end{cases}}$$

위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 $p_{1},\dots ,p_{n},q_{1},\dots ,q_{k}$ 및 서로 다른 변수 $x_{1},\dots ,x_{k}$에 대하여, 만약 $q_{i}\in {\mathcal {P}}$이며 $q_{i}$의 자유 변수가 정확히 $n$개가 아닐 경우, $x_{i}(p_{1},\dots ,p_{n})[q_{1}/x_{1},\dots ,q_{k}/x_{k}]$는 정의되지 않는다.

α-동치

두 유사 논리식 $\phi ,\psi$에 대하여, 다음 조건을 만족시키는 전단사 함수 $f\colon {\mathcal {V}}\to {\mathcal {V}}$가 존재한다면, $\phi ,\psi$가 서로 α-동치(α-同値, 영어: α-equivalent)라고 한다.

• $\psi$는 $\phi$에 등장하는 각 변수 $x$를 $f(x)$로 대체하여 얻는다.

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

• $\psi$는 $\phi$에 등장하는 각 변수 $x$를 $f(x)$로 대체하여 얻는다.
• 임의의 $x,y\in {\mathcal {V}}$ 및 분지 유형 $\tau ^{d}$에 대하여, $x{:}\tau ^{d}\in \Gamma \iff f(x){:}\tau ^{d}\in \Gamma$
• 임의의 $x,y\in {\mathcal {V}}$에 대하여, $x<_{\mathcal {V}}y\iff f(x)<_{\mathcal {V}}f(y)$

역사

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