Formal System

개요

이번 글에서는 Formal System에 대해서 말씀드리겠습니다. 허허; 분명 lambda calculus를 본격적으로 말씀드린다고 했는데, 막상 공부해보니 이 개념을 대충 넘어가면 안되겠더군요.

lambda caclulus를 한 번 쭉 보고나서 느낀 점은 "도대체 내가 뭘 배운거지?"라는 생각이 들었습니다.

기호를 정의하고, 규칙을 정의하고, 정리를 도출하고.. 이게 lambda caclulus와 어떤 관련이 있는가? 궁금했었죠.

하하; 결론을 말씀드리자면 lambda calculus는 Formal System이기 때문에, 위 자체가 람다에 대한 Formal System을 배우는 거였습니다.

따라서 이번 글에서는 Formal System이 무엇인가?에 대해서 알아보도록 하겠습니다.

본문

정의

eng wiki

A formal system is used for inferring theorems from axioms according to a set of rules

ko wiki

형식 체계는 공리들로부터 추론 규칙들을 통해 정리를 이끌어낼 수 있는 논리적 체계를 가리킨다. 또한 이를 표기하기 위한 기호들과 그로부터 문장을 구성하기 위한 문법을 필요로 한다.

정의를 한 세 번 정도 읽고 음미해보세요.

제가 느낀 것은 다음과 같습니다. "맞아잉~ 체계적으로 어떤 지식을 쌓은 것을 의미하네~"로 감이 왔죠.

이 감을 좀 더 자세히 알아보겠습니다

핵심 키워드

1. 공리(axiom)

공리란 증명없이 자명하게 사실이라 간주되는 가정을 뜻합니다.

예를 들어서 유클리드 기하학 논리 체계에선 두 점 사이엔 하나의 직선을 이을 수 있다는 것을 말하죠.

공리는 논리적으로, 다시 말해서 근거를 들어 말할 때 근본이 되는 명제라고도 볼 수 있습니다.

왜? 왜? 왜?라는 질문을 계속 던져보세요. 한 명제를 뒷 받침하는 가장 밑에 있는 근거는 무엇일까요? 질문을 던질 필요도 없이 자명하다고 판단되어 체계의 근간을 이루고 있는 지식이라고 보시면 될 것 같습니다.

2. 추론 규칙(set of rules)

논리식에서 다른 논리식을 이끌어 내는 규칙.

또는 함수들로 이루어진 logical form이라고 하죠. 전제들을 받고, syntax를 분석하여 결론을 내세우는 것. 이라고 합니다.

아무래도 논리학과 연결된 뜻이라 다소 어려워 보이네요. 하지만, 어디서 봤던 글이 떠오르네요... 이걸 떠올리면 좀 더 와닿을 수 있겠습니다.

이론은 단순히 지식 덩어리가 아니라 체계적으로 쌓아올린 지식이다.

맞습니다... 지식을 어떤 규칙으로 엮은 것. 그게 이론이겠지요. 그 짜임새 역할을 해주는 것이 추로 규칙이라고 볼 수 있겠습니다.

또 다른 예시로 삼단논법 아시죠? P->Q이고, Q->R이다면 P->R이다.

이것도 추론 규칙이라고 보시면 돼요.

3. 정리(theorems)

자명한 명제들이 아니며, 공리와 추론 규칙으로 인해 증명된 명제들이라고 보시면 됩니다.

새로운 발견이라고도 생각할 수 있을 것 같아요 ㅎㅎ

표현

그래서 위와 같은 내용들을 어떻게 "표현"해야 할까요? 수학에서, 컴퓨터 언어에서 배우는 것과 똑같습니다 ㅎㅎ

기호로 관심있는 대상을 표현하고, 이 대상들을 문법을 통해 문장을 만드는 것이지요.

Lambda caculus와 연결

그래서 lambda calculus는 위와 같은 formal system을 배우는 것입니다! 그렇다면, 어떤 formal system을 배우는 것일까요? 화학, 물리, 수학처럼 뭔가 관심있는 대상들을 체계적으로 쌓아 올리잖아요?

정의를 다시 한 번 읽어볼게요.

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.

람다 칼큘러스는 function abstraction과 function application을 계산을 표현하기 위한 수학 논리에서의 formal system이라고 합니다. 그리고 그 계산을 하기 위해 variable binding과 substitution을 사용하지요.

function abstraction이니, function application이니, variable binding이니 variable substitution이니하는 것은 아직 잘 모르니까 대충 함수에서 특정 부분의 연산에 관한 것이라고 뭉그뜨려서 표현합시다.

그래서 요약하자면, 함수 특정 부분의 연산에 대한 formal system이란 것이죠 ㅎㅎ

그래서 함수 특정 부분 연산을 위한 기호에 대해 알아보고, 규칙을 알고, 정리들을 알아가는 내용이라고 보시면 될 것 같습니다.

그리고 위와 같은 체계들을 javacsript, go, pascal등 각자 나름대로 구현하고 있다고 보시면 됩니다.

앞으로 우리가 알 것에 대해 좀 더 명쾌한 글이 되었으면 좋겠네요.