계산 삼위일체론 computational trinitarianism

웹서핑을 하다가 흥미로운 개념을 알게 되었는데, 제대로 이해한 건 아니지만 일단 개소리를 써 본다. 사실 이 블로그의 대부분의 내용이 다 헛소리다. ㅋ

삼위일체론은 나도 잘 모르지만-_- 이렇게 이해했다: 신이라고 추정되는 어떤 가상적 존재성과, 인간의 형태로 등장한 예수라는 인물과, 신성한 영혼이라는 개념은 형태가 모두 다르지만 본질이 동일하다는 주장이다.

무신론자인 본인도 과거 피치못할 사정으로 교회에 간 경험이 있는데, (물론 군대-_-) 아마 거기서는 내가 설교를 제일 열심히 들었을 것이다-_- 목사님이 나름 은근히 동방정교회를 디스하는 듯한 발언을 하시던데-_- 나는 여태까지 동방정교회가 삼위일체를 부정하는 줄 알았더니만, 지금 위키피디아를 보니 동방정교회도 삼위일체를 인정하고 있었네??? 아, 설교를 들은지 너무 오래돼서 여호와의 증인이랑 헷갈렸던 것 같다-_- 지금 찾아보니 여호와의 증인은 삼위일체를 부정하는 듯[1]. 개인적으로 중앙아시아사에 관심이 좀 있는데, 네스토리우스파도 삼위일체를 부정한다고 들었다. 중앙아시아사에 대한 저작물을 몇 개[2,3]보면 은근 네스토리우스파 이야기가 꽤 등장한다. 몽케 칸이 각종 종교지도자들을 불러 모아 놓고, 종교 토론 배틀-_-을 시켰다는 이야기[2]를 들은 적이 있는데, 거기서도 네스토리우스파도 당당한 일원으로 등장한다.

뭐 여하간 카네기 멜론 대학의 Robert Harper 선생의 블로그에 computational trinitarianism에 대한 설명[4]이 잘 돼 있다. nLab의 설명[5]도 참고하시기 바란다. 대충 검색해보니 ‘computational trinitarianism’을 번역한 사이트가 없길래 내 맘대로 ‘계산 삼위일체론’이라 번역했다-_- 이거 뭘로 번역해야 되지-_-

여하간 명제의 증명(proofs of propositions), 자료형의 프로그램(programs of a type), 구조의 사상(mappings between structure)이 모두 동일한 개념의 다른 표현이라는 이야기라고 한다. 세 가지는 각각 논리학, (프로그래밍) 언어론, 범주론에서 중요하게 다루는 부분이다. 논리학에서 어떤 명제가 존재하고 무엇이 증명을 이루는가를 다루고, 언어론에서 어떤 자료 유형(type)이 존재하고 어떻게 프로그램을 구성하는가를 다루며, 범주론에서 어떤 수학적 구조가 존재하고 무엇이 그들 사이의 map을 이루는가를 다룬다.

이후로 Harper 선생이 axiom으로부터 명제의 증명, 프로그램에서 변수로부터의 유형판단, 범주론에서 mapping의 유사성에 대한 설명을 하는데, 뭐 본인은 잘 모르지만 뭔가 좀 신박하다. 논리학, 프로그래밍, 수학이 모두 대통일 된다는 이야기 아닌가. 모든 증명은 프로그램이고, 모든 프로그램은 mapping이고 모든 mapping은 증명이 된다. 궁극적으로 수학적 추론과 프로그램의 실행이 합치하게 된다!!! 일전에 본 DeepHOL[6]은 아무것도 아니구만-_-

경제학에서는 고정환율제도, 자본 이동의 자유화, 통화정책의 독립성이 동시에 달성될 수 없다는 Unholy Trinity가 있는데, 수학/컴퓨터공학에서는 holy trinity가 될 듯하다. 증명, 실행, 사상(mapping)이 한 몸임을 믿습니까?? ㅋㅋㅋㅋㅋ

.


2019.10.7
Curry–Howard correspondence라는 게 이미 있었구만. 젠장 오늘 알았네-_- 근데 왜 Robert Harper 선생은 이 용어의 언급을 안 한 건지는 의문이다.

.


[1] NEWSM 궁금한데 물어볼 수 없었던 ‘삼위일체 교리’ 2010.07.23 14:16
[2] 내 백과사전 [서평] 몽골 제국 기행 – 마르코 폴로의 선구자들 2018년 3월 1일
[3] 내 백과사전 [서평] 신장의 역사 : 유라시아의 교차로 2013년 5월 30일
[4] The Holy Trinity (existentialtype.wordpress.com)
[5] computational trinitarianism (nLab)
[6] 내 백과사전 DeepHOL : 딥러닝을 이용한 수학 명제 자동증명 시스템 2019년 4월 29일