분지 유형 이론

위키백과, 우리 모두의 백과사전.
둘러보기로 가기 검색하러 가기

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

정의[편집]

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

  • 최대 원소를 갖지 않는 가산 무한 정렬 전순서 집합 . 그 원소를 변수(變數, 영어: variable)라고 한다.
  • 집합 . 그 원소를 개체(個體, 영어: individual)라고 한다.
  • 집합 함수 . 각 에 대하여, 의 원소를 항 관계(項關係, 영어: -ary relation)라고 한다.

그렇다면, 에 대한 분지 유형 이론은 다음과 같다.

분지 유형[편집]

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

  • 은 0차 분지 유형이다.
  • 차 분지 유형 및 자연수 에 대하여, 차 분지 유형이다.

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

  • 은 술어적 분지 유형이다.
  • 차 술어적 분지 유형 에 대하여, 는 술어적 분지 유형이다.

술어적 분지 유형은 차수를 생략한 채 으로 쓸 수 있다.

분지 유형 이론의 문맥(文脈, 영어: context)은 정의역이 유한 집합인 변수의 집합과 분지 유형의 집합 사이의 부분 정의 함수이다. 변수 와 분지 유형 순서쌍로 표기하자. 그렇다면, 문맥을 이러한 순서쌍들의 집합으로 여길 수 있다. 이 경우, 문맥 정의역(定義域, 영어: domain)은 다음과 같이 나타낼 수 있다.

논리식[편집]

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

  • 항 관계 및 변수 또는 개체 에 대하여, 은 유사 논리식이다.
    • 일 경우 유사 논리식 은 0항 관계 와 구분되어야 한다. 분지 유형 이론에서 항 관계는 유사 논리식이 아니다.
  • 변수 및 유한 개의 변수 또는 개체 또는 유사 논리식 에 대하여, 는 유사 논리식이다.
    • 일 경우 유사 논리식 은 변수 와 구분되어야 한다. 분지 유형 이론에서 변수나 개체는 유사 논리식이 아니다.
  • 유사 논리식 에 대하여, 는 유사 논리식이다.
  • 유사 논리식 및 그 자유 변수 및 분지 유형 에 대하여, 는 유사 논리식이다.

유사 논리식의 집합을 라고 하자. 또한 각 유사 논리식 에 대하여, 속에 등장하는 모든 변수의 집합이라고 하고,

의 모든 자유 변수라고 하자.

문맥 에서 개체 또는 유사 논리식 가 분지 유형 를 갖는다는 것은 로 표기하며, 다음과 같이 재귀적으로 정의된다. (여기서 를 뜻한다.)

  • 개체 에 대하여, 이다.
  • 항 관계 및 개체 에 대하여, 이다.
  • (논리 연산) 문맥 및 유사 논리식 및 분지 유형 에 대하여, 만약 이며, 이며, 라면,

    이다.

  • (한정) 문맥 및 유사 논리식 및 분지 유형 에 대하여, 만약 라면,

    이다.

  • (매개 변수에 대한 추상화) 문맥 및 유사 논리식 및 그 개체이거나 유사 논리식인 매개 변수 및 분지 유형 및 술어적 분지 유형 및 변수 에 대하여, 만약 이며 이라면,

    이다. 여기서 에 등장하는 와 αΓ-동치인 각 매개 변수 로 대체하여 얻는 유사 논리식이다.

  • (논리식에 대한 추상화) 문맥 및 유사 논리식 및 술어적 분지 유형 및 변수 에 대하여, 만약 이라면,

    이다. (이 경우 반드시 임을 보일 수 있다.)

  • (치환) 문맥 및 자유 변수를 갖는 유사 논리식 및 개체 또는 유사 논리식 및 분지 유형 에 대하여, 만약 이며, 라면,

    이다. (이 경우 는 반드시 정의됨을 보일 수 있다.)

  • (약화) 문맥 및 유사 논리식 및 분지 유형 에 대하여, 만약 이며, 라면, 이다.
  • (순열) 문맥 및 유사 논리식 및 분지 유형 및 변수 에 대하여, 만약 라면,

    이다.

주어진 문맥 속에서, 유사 논리식의 분지 유형은 존재하지 않을 수 있으나, 만약 존재한다면 이는 유일하다. 주어진 유사 논리식은 서로 다른 문맥 속에서 서로 다른 분지 유형을 가질 수 있다. 유사 논리식 에 대하여, 인 문맥 가 존재한다면, 논리식(論理式, 영어: formula)이라고 한다.

연산[편집]

자유 변수, 매개 변수, 재귀 매개 변수[편집]

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

  • 항 관계 및 변수 또는 개체 에 대하여,

  • 변수 및 유한 개의 변수 또는 개체 또는 유사 논리식 에 대하여,

  • 유사 논리식 에 대하여,

  • 유사 논리식 및 그 자유 변수 에 대하여,

치환[편집]

변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여,

이라고 하자.

유사 논리식 및 변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여, 치환 실례(置換實例, 영어: substitutional instance) 는 다음과 같이 재귀적으로 정의된다.

  • 항 관계 및 변수 또는 개체 및 서로 다른 변수 에 대하여,

  • 변수 및 및 변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여,

  • 유사 논리식 및 변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여,

  • 유사 논리식 및 그 자유 변수 및 분지 유형 및 변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여,

위 경우에 속하지 않는 치환 실례는 정의되지 않는다. 예를 들어, 변수 또는 개체 또는 유사 논리식 및 서로 다른 변수 에 대하여, 만약 이거나, 이며 의 자유 변수가 정확히 개가 아닐 경우, 는 정의되지 않는다.

α-동치[편집]

두 유사 논리식 에 대하여, 다음 조건을 만족시키는 전단사 함수 가 존재한다면, 가 서로 α-순열 동치(α-順列同値, 영어: α-equivalent modulo permutation)라고 한다.

  • 에 등장하는 각 변수 로 대체하여 얻는다. (특히, 이다.)

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

  • 에 등장하는 각 변수 로 대체하여 얻는다. (특히, 이다.)
  • 증가 함수이다. 즉, 임의의 에 대하여,

두 유사 논리식 및 문맥 에 대하여, 다음 세 조건을 만족시키는 전단사 함수 가 존재한다면, 가 서로 αΓ-동치Γ-同値, 영어: αΓ-equivalent)라고 한다.

  • 에 등장하는 각 변수 로 대체하여 얻는다. (특히, 이다.)
  • 는 증가 함수이다. 즉, 임의의 에 대하여,
  • 임의의 및 분지 유형 에 대하여,

역사[편집]

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

각주[편집]

  1. Laan, Twan; Nederpelt, Rob (1996년 10월). “A modern elaboration of the ramified theory of types”. 《Studia Logica》 (영어) 57 (2–3): 243–278. doi:10.1007/BF00370835. ISSN 0039-3215. JSTOR 20015876. 
  2. Kamareddine, Fairouz; Laan, Twan; Nederpelt, Rob (2005). 《A Modern Perspective on Type Theory》. Applied Logic Series (영어) 29. Dordrecht: Springer. doi:10.1007/1-4020-2335-9. ISBN 978-1-4020-2334-7.