감명 깊었던 programming language principles 2-기본기

2. 기본기 

프로그래밍 언어가 어떤 형태로 되어있는가 를 이야기 하기 위해서는 기본적으로 사용하는 어휘들과 말하는 방식이 있습니다. 그 어휘와 방식의 기본이 수학입니다.

이런 베이스적인 부분들을 언급할 필요성이 있고, 이해해야할 필요 역시 있습니다.

귀납법 ( inductive definition)

집합을 정의하는 방법에는 조건제시법, 원소 나열법, 귀납법이 있습니다.

원소나열법 :{0,1, 참새, 비둘기}

조건 제시법 : {x|x는 1,2 의 양의 정수}

귀납법은, 

참 매력적인 분야라고 합니다. 무한한 것을 유한한 것들로 정의 할 수 있기 때문입니다.

프로그래밍 언어에서는 이 귀납법에 대한 이해가 반드시 필요합니다.

한번 귀납법에 대해서 살펴 볼까요? ( 저처럼 수학에서 멀어진지 오래된 사람들은 기억이 가물가물 하답니다.^^)

자연수의 정의를 귀납적으로 표현 하는 방법은 아래 같습니다.

방법 1

A. 3단 논법이죠? 또는 B. B의 식은 사실 A를 살짝 수학스럽게(?) 표현한 것에 불과 합니다. 해석해보자면 "/은 자연수이다." 반드시 참인 식이어야겠죠. 분모의 정의("/#이 자연수이다.")를 만족하는 조건식 필요 조건은 "#은 자연수이다." 입니다.

방법 2

A. 음, 해석을 살짝 하자면,  "/ 가 자연수(N) 이다. /에 자연수(N)을 붙여도 자연수 이다." 정도로 이해하면 됩니다. 또는 B.

프로그래밍 언어에서는 다음과 같은 형식으로 표현됩니다.

그 예를 아래  나열 해 봤습니다.

자연수 집합

혹은 

 

스트링 집합

혹은

리스트

혹은 

정수 트리 

혹은

정수식 들의 집합

자연수 n은 정수 식이고, e가 정수식 이라면 그 앞에 음의 부호를 붙여도 정수식이고, 두개의 정수식 사이에 덧셈 부호나 곱셈 부호를 끼워넣어도 정수식이다.

간단한 프로그래밍 언어 표현

프로그래밍 언어에 대한 이야기 중인데 너무 귀납법이라는 것에 치우치게 되는것 같아서 나중에 나올 내용인데 미리 적어봤습니다. 

이 식을 처음 봤을때, 느낌이 강렬 했거든요. "아 이래서 프로그래밍 언어가 수학에서 나왔다라고 할 수있겠구나." 라는 생각을 했었으니까요.

정확한 표현은 아니지만, 이렇게 해석해보면 뭘 의도하는 표현식인지 이해가 쉬울 것입니다.

1. s -> x  syntax(또는 식) x  로 되어있다.

2. x는 e (expression : 식, 또는 명령어, 또는 상수 등등...) 이다.

3. x는 s;s 일 수도 있고, if e s s 일 수도 있고, print e 일 수도 있다.

4, s;s 는 각 식은 ; 으로 연결된다. (여러 언어들에서 문장의 맨 마지막에 ; 붙이는 것 말이죠)

5. if e s s  if 명령문은 e가 참이면 첫번째 s를 수행하고 두번째 s를 수행한다.

6. print e  e의 결과 값을 출력한다.

이렇게 해석해 보면, 프로그래밍 언어의 규칙을 표현한 것으로 보이죠?

형식논리

선언논리에서 생각하는 논리식 f는 다음의 귀납법칙으로 만들어 지는 집합의 원소이입니다.

논리식 이라고 하면, 전자공학에서 배우는 논리식을 생각 하실 수 있을 것입니다. 맞습니다. 바로 그것을 의미하는 것입니다.

그 논리식을 귀납법의 규칙에 따라 적으면 다음과 같습니다.

논리식을 다음과 같이 표현 방법을 바꿔봅시다.

implication :  ⊃ → ⇒

implication 은 '논리 승' 이라고 표현하기도 하는데 아래와 같은 참,것짓 테이블을 가집니다.

A	B	A⊃B
T	T	T
T	F	F
F	T	T
F	F	T

추론규칙

이제까지 참인지 거짓인지에 대한 표현 방법을 배웠다면, 논리식이 참인지 판별하는 방법에 대해서 고민해볼 차례인것 같습니다.

물론, 논리식의 의미를 정의한대로 따라가다보면 결과를 알수 있습니다. 음... 참, 혹은 거짓, 

논리식을 따라가면서 본다는 것이 결국, 프로그램을 돌려보고 그 프로그램이 참의 결과를 내는지 판별하는 것과 같습니다.

그런데, 혹시,,, 프로그램을 돌리지 않고 알아내는 방법은 없을까요? 논리식의 의미를 계산하지 않고 참인지 거짓인지 알수는 없을까?

논리식의 모양만을 보면서 참인지를 판별할 수는 없을까?

이런 규칙을 증명 규칙, 또는 추론 규칙이라고 합니다.

            

                       

                               

                          

                                

(감마, f) 쌍들의 집합을 만드는 규칙들이 위와 같습니다. 이는"감마에 있는 모든 논리식들이 참이면 f는 참" 이라는 의미를 갖습니다.

대개 형식논리에서는 "(감마, f)" 를 "감마 ㅏ f" 로 표기합니다.

이렇게 위의 식들을 다시 표시해보면,

(R1)     (R2)    (R3) (R4)

(R5)   (R6)

(R7)    (R8)

(R9)  (R10)

 

 

(R11) (R12)

  

의 증명을 위의 증명규칙으로 만들면 아래의 나무 구조가 됩니다. 

  

문법 구조와 의미 구조 

안전한 혹은 완전한

위의 규칙들이 만들어 내는  의 f는 모두 참인가? 반대로, 참인 식들은 모두 위의 증명규칙들을 통해서  꼴로 만들어지는가?

첫 질문에 예라고 답할 수 있다면, 우리의 규칙은 안전하다고 , 믿을만 하다고 한다.

둘째 질문에 예 라고 답할 수 있으면 유리의 규칙은 완전하다고, 빠뜨림이 없다고 한다.

증명 규칙들이 안전하기도 하고 완전하기도 하다면, 참인 식들만 빠짐없이 만들어 내는 규칙이 된다.

안전하냐 완벽하냐는 기계적인 증명규칙들의 성질에 대한 것이다.

그 기계적인 규칙들의 성질은 오직 우리가 생각하는 의미에 준해서 결정될 수 있다.

프로그램에서 그 겉모양(문법)과 속내용(의미)은 대개 다른 두개의 세계로 정의되고, 프로그램을 관찰하고 분석하는 모든 과정은 기계적으로 정의된다.

컴퓨터로 자동화하기 위해. 그 기계적인 과정들의 성질들(과연 맞는지, 무엇을 하는 것인지) 등에 대한 논의는 항상 그 과정의 의미나 결과물들의 의미를 참조하면서 확인된다.

다음 >> 모양과 뜻