미카 프로젝트

오류 검증 문제

M3는 유용하지만 실행되서는 안되는 프로그램들이 있습니다. 실행중에 타입이 맞이 않아서 실행을 멈추게 되는 경우를 가진 프로그램들입니다.

타입

 - 프로그램을 기획하는 한 방법

 - 프로그래밍 언어가 그러한 기획을 물샐틈 없이 할 수 있도록 구성되어야 

  "너무 빡빡하지 않게" (PASCAL, PL/1, Algol68, Ada)

 

프로그램이 기획한 대로 실행된다는 것을 보장해야

 

프로그램 기획이 제대로 됬는지를 실행전에 검증 될 수 있어야 

검증이 자동으로 된다면...

M3 프로그램은 다섯종류의 값들이 있고 각각 분별력있게 흘러다녀야 합니다. 함수, 정수, 참/거짓, 쌍, 메모리 주소 입니다.

1. 함수 적용식  E1 E2  에서 식 E1은 함수여야 합니다. 

2. 덧셈식 E1 + E2 의 부품식들의 결과는 정수여야 합니다.

3. 조건식 if E1 E2 E3 에서 E1의 결과값은 참/거짓 이어야 합니다.

4. 쌍에서 첫번째 값을 뜻하는 식 E.1 에서 E의 결가값은 쌍이어야 합니다.

5. 메모리에 쓰는 식 E1:=E2 에서 E1의 결과 값은 메모리 주소여야 합니다.

M3 프로그램이 위와 같은 타입의 조건을 실행중에 항상 만족하는지를 미리 자동으로 검증하는 것이 가능했으면 하는 것입니다.

미리 static 안전하게 sound 검증하는 그러한 타입 시스템이 M3에 대해서는 가능합니다.

정적 타입 시스템 static type system

정적 타입 시스템은 말이 되는 프로그램인지를 프로그램 텍스트만으로 판단하는 한 방법입니다. 실행전에 말이죠.

이는 정적 의미 구조 static semantics 라고 부르기도 합니다. 이전까지의 의미구조들은 모두 동적 의미구조 dynamic semantics 였습니다.

일차적으로 문법 검증이 수행되는데, 

대부분 문법 구문은 아주 간단하기 때문에 문법 자체를 검증 하는 것은 쉽습니다.

그러나 프로그램은 문법 검증만으로 안전하다는 보장은 할 수 없습니다.

예를 들면,아래와 같은 간략한 문법규칙이 있다고 합시다.

문법 규칙이 간단하다는 것은 문맥을 생각하지 않는 규칙들이기 때문입니다.

+ 식은 두개의 부품식들이 정수식이어야 한다는 이런 문맥에 대한 조건은 "문법 규칙"에 표현하지 않습니다.

그래서  1+'a'는 문법상으로 정상이 되는 것입니다.

만약 이런 문맥에 대한 조건들을 표현한다면, 문법 규칙에서 "정적 타입 시스템"으로 은근 슬적 넘어가는 것입니다.

정적 타입 시스템 은 결국 일종의 정적 프로그램 분석(static program analysis)입니다.

대부분의 프로그램 분석이 그렇듯 정적 타입 시스템 역시 완전하지 못합니다.(incomplete)

그러나 안전하기는 합니다.(sound) 안전하도록 타입 시스템을 고안 해야 합니다.(우리 언어인 M3안에...)

정적타입 시스템은 형식 논리 시스템(formal logic)입니다. 논리식의 생김새, 논리식의 의미, 참인 논리식을 기계적으로 추론하는 규칙들 proof rules 또는 inference rules라고 불리는 것들 을 이용하여, 안전성과 완전성을 증명하는 논리 식들로 구성하는 것입니다.

구현되는 알고리즘이 디자인 한 타입 시스템을 제대로구현한 것이라는 사실도 확인하게 됩니다. 디자인에서 구현까지 단단한 과정을 밟는 것입니다.

형식 논리 시스템(formal logic) 리뷰

형식 논리 시스템은 논리식 집합의 정의, 논리식 의미의 정의,  참논리식 집합의 정의, 참논리식 추론의 방법, 추론방법 평가하기

로 구성됩니다.

선언 논리 (propositional logic) 시스템을 보자. 논리식 집합은 다음과 같은 귀납 규칙으로 정의됩니다.

논리식의 정의는 다음과 같고,

참인 논리식들의 집합을 정의합니다 

: 즉, 쌍 ({f1,...,fn},f)    (표기 : 

)들의 집합입니다.

참인식 

들의 집합들.

이 규칙들은 참인 식을 만드는 규칙이고, 이것을 논리 시스템에서는 추론규칙 inference rules 혹은 증명규칙 proof rules 라고 합니다.

여기서 살짝 다른 관점에서 보자면, 참인 논리식 집합을 만드는 과정은 곧 참 논리식을 유추한 증명을 만드는 과정이기도 합니다. 증명들의 집합을 만드는 귀납규칙으로보는 것입니다. 

증명규칙으로 만들어지는 증명을 증명 나무 (proof tree)라고 합니다.

이제 이렇게 "기계적인" 증명규칙 혹은 추론 규칙이 정말 좋은가를 따져봐야 합니다.

추론 규칙의 안전성 soundness

추론 규칙의 완전성 completeness

단순 타입 시스템 simple type system

M0 로 모든 것을 프로그래밍 할수 있겠으나, 값은 오직 함수 밖에 없었습니다. 값의 타입으로 함수와 정수만 있는 M1 코어만 생각합시다.

위의 의미 규칙

를 사용할 수도 있으나, 타입 시스템의 안정성 증명에서 편리한 방식을 위해서 프로그램 텍스트를 다시 써가는 방식의 의미에서, 

의미는 같지만, 실행 문맥 evaluation context을 이용하여 다음과 같이 정의 합니다.

실행 문맥은 적극적 실행 Eager evaluation 순서에 준해서 다음에 실행해야 할 부분을 결정됩니다.

프로그램 실행 규칙은 다음과 같습니다.

프로그램 E의 의미는 위의 규칙에 따라

단순 타입 추론 규칙

타입시스템을 정의합시다.

다시 한번 강조 하지만, 프로그램 텍스트만을 가지고 타입 오류 없이 실행되는 프로그램인지를 검증하는 논리 시스템입니다.

-프로그램 텍스트에 타입이 명시된것은 없습니다.

 하지만 논리시스템은 프로그램 구석구석의 타입이 어떻게 기계적으로 유추될 수 있는지를 정의합니다.

논리식의 생김새는 

입니다.

Γ(gamma)는 타입 환경 type environment 으로 변수들의 알려진 타입을 가지고 있습니다.

타입환경 Γ에 대해서 Γ{x⟼τ} 대신 Γ+x:τ로도 씁니다.

x⟼τ ∈ Γ 대신에 x:τ ∈ Γ 로도 쓸 것입니다.

논리식의 의미는

                  [[ Γ⊢E:τ]]= true

                              iff

                 : ∀σ ⊨ Γ.E 이 영원히 돌든가, 값을 계산 E→*υ 하면 ⊢υ:τ

입니다.

이제 참인 논리식을 유추하는 규칙을 정의합니다.

타입 추론 규칙 type inference rules

이 식을 이용해서 실제 타입들에 대해서 증명과정에 대해서는 생략...

1. 식 E의 생김새마다 오직 하나의 규칙이 있다.

 이 사실은 증명규칙의 성질을 증명할 때 우리를 편하게 합니다.

예를 들어

이런 식이 유추 되었다면, 반드시 한 경우밖에 없습니다. : 

의 타입 유추 규칙이 하나 밖에 없으므로, 그 규칙에 있는 조건이 만족한 경우 밖에 없습니다.

즉, 

이면   

 이면 

                                             :

2. 어떤 식 E에 대해서, Γ⊢E:τ 인 τ값이 여럿 가능하다.

3. 문제 없이 실행되는 프로그램이 타입 유추가 불가능한 경우가 있다. 완전 complete 하지는 못한 것이다.

추론 규칙의 안전성

우리는 추론 규칙의 안전성 soundness은 증명할 수 있습니다.

즉, 타입 추론이 성공하면 그 프로그램은 타입 오류 없이 실행된다는 것이 보장됩니다.

즉, 프로그램(자유변수가 없는 식) E에 대해서

이 추론될 수 있다면, 프로그램 E는 문제 없이 실행되고 , 끝난다면 결과값 τ 타입이라는 것입니다.

두가지 증명법

1. 안정성을 증명하는 한가지 방법.

- Progress Lemma: 값이 나올 때 까지 문제 없이 진행한다.

               ⊢e:τ 이고 e가 값이 아니면 반드시 e → e'

- Subject Reduction Lemma : 진행은 타입을 보존한다.

               ⊢e:τ 이고  e → e' 이면  ⊢e':τ

2. 안정성 증명하는 두번째 방법.

- E → error 를 정의합니다.

- Subject Reduction Lemma : "진행은 타입을 유지한다", 를 증명합니다.

      ⊢E:τ 이고 E→ E' 이면 ⊢E':r 이다.

- 안정성이란, 값이 아닌 식 E가 타입이 있으면, E는 문제없이 진행하며 끝난다면 그 타입은 값이어야 한다.

- 값이 아닌 식 E가 타입이었다고 하자. 잘 진행하는가?

   그렇다, E

→error로 진행할 수 없다. 왜냐하면, 그렇게 진행한다면 "Subject Reduction Lemma"에 의해서 모순이기 때문이다. error가 타입이 있어야 하는데 error의 타입을 결정하는 규칙은 없기 때문이다.- 그리고 진행이 타입을 항상 보존하므로, 값으로 진행이 끝나게 되면 그 값도 같은 타입을 가진다.

이 단순 타입 시스템은 논리시스템으로 우리가 바라는 바를 가지고 있음을 증명할 수 있었습니다. 

다음 단계는 구현입니다. 하지만 간단해 보이지 않습니다. 다음 규칙을 보면 말이죠.

함수 몸통 E를 타입 유추하려면 인자의 타입 τ1을 알고 있어야 합니다. 그러나, τ1은 우리가 최종적으로 유추해야 할 함수 타입의 일부입니다.

어디서 본듯한 패턴입니다. 유추해야 할것을 미리 알고 있어야 한다.!!! 유추를 포기한다? 프로그래머에게 함수마다 타입을 기입하라고 해야 할까?

이번에는 놀라운 방식이 있습니다. 타입에 대한 연립방정식을 세우고 풀어가는 과정입니다.

그 과정이 놀라운 이유는 ,우선 타입을 자동으로 유추해 주는 알고리즘 때문입니다. 프로그램 텍스트에 타입에 대해서 프로그래머가 아무것도 명시할 필요가 없습니다. 자동으로 유추되기 때문입니다.

또다른 이유는, 타입 시스템을 충실히 구현한 알고리즘이기 때문입니다. 충실히?? 타입 시스템이 유추할 수 있는 것을 그 알고리즘은 똑 같이 유추해줍니다. 그 반대도 성립합니다. 알고리즘이 유추해 내었으면 타입 시스템도 같은 것을 유추해 낼 수 있습니다. 서로 iff관계로 논리시스템과 구현 시스템이 물려 있습니다.

예를 들면,

   1+(λx.x 1)0

이런 식이 있다고 합시다.

 각 부품(파트) 별로 번호를 붙여봅시다.

부품식 i 가 가져야 하는 타입 αi 와 변수 x가 가져야 하는 타입 αx에 대한 방정식 "lhs ≐ rhs" 는 다음과 같습니다.

위의 방정식의 해는 없다.  αx 는 ι(iota 요타)이기도 해야 하고 ( α≐ αx 로부터) ι →ι이기도 해야 하므로 ( α6≐ αx 로부터)

타입 연립 방적식 u는 다음과 같은 모습입니다.

타입 방정식

연립

타입변수

타입 연립 방정식의 해 S를 치환으로 표현하면 편합니다. TyVar을 Type으로 바꾸는 것입니다.

:A->fin B  = A에서 B로 가는 치환들의 집합입니다. 

따라서 TyVar에서 Type으로 가는 집합을 의미합니다.

온라인 알고리즘들

타입 방정식을 도출하면서 그때 그때 풀어가는 알고리즘도 가능합니다.

안전한 그러나 경직된

단순 타입 시스템은 안전하긴 하지만 아쉬움이 많습니다.

완전하지 못하다. 타입 오류 없이 잘 실행될 수 있는 모든 프로그램이 단순 타입시스템을 통과 할 수는 없습니다.

인자 타입에 상관없이 실행되는 함수들이 많이 있습니다.

안전하지만 빠뜨리는 프로그램들이 있는 것입니다.

재귀 함수

재귀 함수는  Y 컴비네이터  (Y combinator)를 통해서 표현할 수 있습니다.

  :Y 컴비네이터

이 핵심 부분은 자신을 인자로 받는 함수의 적용  "x x"입니다.

단순 타입 시스템에서는 함수가 자신을 인자로 받는 식은 타입 유추가 될 수 없습니다.

각 부품식 i가 가져야 하는 타입 αi를 따져보면,

이 되는데, 결국 α→β≐α를 만족하는 타입을 Type에서는 찾을 수 없습니다.

unification  알고리즘은 위의 양변을 같게 만드는 α와 β를 찾는 것에 실패한다.

단순 타입시스템이 갖추어진 언어에서는 재귀함수를 Y 컴비네이터로 표현해서는 타입 시스템을 통과할 수 없습니다.

때문에 재귀함수인

은 필수가 됩니다. (더이상 설탕이 아닙니다.)

메모리 주소 값

메모리 주소를 값으로 사용하는 경우는 타입 시스템을 어떻게 확장할 수 있을까?

우선 타입의 종류가 하나 늘어납니다.

1. 타입 τ loc 는 메모리 주소타입인데, 그 주소에는 τ 타입의 값이 저장되는 타입입니다.

그리고, 타입 규칙들은 자연스럽게 확장됩니다.

다형 타입 시스템

단순 타입시스템을 정교하게 확장하자.. 안정성을 유지하면서 "잘 모르겠다"고 하는 경우를 줄입니다.

안전하면서 유연한 타입시스템이 필요합니다.

다형 타입 시스템(polymorphic  type system)이 바로 그러한 타입시스템입니다.

타입 유추가 가능하고 실제 언어에 실용적으로 구현될 수 있는 다형 타입 시스템이 let-다형 타입 시스템입니다.

타입 시스템에서 

"잘 모르겠다" = "타입방정식의 해가 없다" 즉,

이런경우 ⊢p 는 ⊢를 포섭하면서 확장한 경우라고 합니다.

다형 타입 시스템에서 "잘 모르겠다"고 하는 경우가 단순 타입 시스템 보다는 적습니다.

프로그래밍 언어의 편의성 측면에서는 여러가지 설탕 구조물들이 첨가 되어야 합니다. 

이는 프로그래머에게 편의를 제공해주고, 코드의 이해를 돕는데 좋은 장치가 됩니다.

컴퓨터 메모리를 사용하는 명령형 언어의 모습(imperative features)가 그 대표적인 예입니다.

추가합니다.  

언어키우기 : M3

1. 새로운 메모리 주소를 할당받는다.

2. 메모리 주소에 저장된 값을 읽고 쓴다.

3. 프로그램 실행 순서에 따라서 다른 결과를 계산하게 될 수 있다. (주소에서 읽고 나서 쓰느냐 쓰고나서 읽느냐)

이제 값의 공간에는 메모리 주소가 포함되었습니다.

메모리 주소가 값이 되면서, 프로그램 식의 의미 판단에는 메모리가 필요합니다.

메모리에는 프로그램의 식들이 계산되면서 일어난 반응들이 계속 쌓여갑니다.

  : 식 E가 환경 σ(sigma) 와 메모리 M에서 υ를 계산하고 그 결과는 M'이다.

메모리는 주소에서 값으로 가는 유한 함수입니다.

의미 규칙은 다음과 같습니다.

다른 모든 식들의 의미 규칙에도 메모리 반응이 쌓여가는 것이 표현되야 할 것입니다. 예로

이렇게 해서 M3의 문법을 다시 정리하면.

while E do E 역시 설탕구조입니다.

우선 M3로 녹일 수 있습니다.(표현 가능합니다.)

다음 >> 정적 타입 시스템 (static type system)

지금까지 프로그래밍 언어가 어디서 시작되어 어떻게 만들어 졌는지에 대해서 언급했습니다.

현재 프로그래밍 언어가 나아가는 방향은 시스템(기계) 을 다루는 단계에서 점점 본연의 목적을 향해 가고 있습니다.

그 본연의 방향이라는 것은 적어도 "기계를 편하게 다루는 것"은 아닙니다. 

"기계의 편리한 사용" 이라는 슬로건으로는 달성할 수 없었던 결과를 향하는 것입니다.

다시한번 처음에 언급했던, 프로그래밍 언어가 컴퓨터를 구동시키기 위해 만들어 졌는가?에 대해서 되세겨봅시다.

프로그래밍 언어는 컴퓨터를 동작시키기 위해서 만들어진 것이 아닙니다. 프로그래밍 언어가 있었고(수학적 증명을 위해서 만들어진), 이것을 동작시키기 위해서 컴퓨터가 탄생했습니다. 

1930-40 년대에 이미 논리학자와 수학자들은 기계적으로 계산가능한 것이 무엇인지 고민하기 시작했습니다.

괴델은 부분 재귀 함수(Partial Recursive Function)꼴로 정의 되는 함수들을 기계적으로 계산 가능한 것들이라고 정의했습니다.

처치는 람다 계산법(Lambda Calculus)으로 계산될 수 있는 것들이가고 정의 했고,

튜링은 튜링 기계(Turing Machine)가 실행할 수있는 것들이라고 정의 했습니다.

그런데, 세 가지가 모두 같은 정의였습니다. 부분 재귀 함수는 람다 계산법으로 계산될 수 있고, 람다 함수는 튜링 기계로 실행할 수 있고, 튜링 기계가 실행하는 함수는 부분 재귀 함수 꼴로 정의 할 수 있습니다.

그러고 나니 사람들은 기계적으로 계산 가능한 함수가 그게 다가 아닐까 믿고 있습니다. 세사람이 독자적으로 정의한 것들이 결국 다르지 않은 것으로 미루어 , 이것을 "Turing-Church Thesis"라고 부릅니다.

이 셋중에 람다 계산법( Lambda Calculus)이 문법과 의미정의를 가춘 언어의 모습을 하고 있습니다.

람다 계산법 Lambda Calculus

이 람다 계산법이라는 언어를 기초로 프로그래밍 언어를 디자인해가면 , 이 언어의 표현력이 완전하기 때문에 , 기계적으로 계산 가능한 모든 것이 이 언어로 작성할 수 있기에, 든든해집니다.

기계적으로 계산 가능한 모든 것을 표현할 수 있는 언어 "Turing-Complete"이라 합니다.

언어의 이름을 람다(Lambda)라고 합시다.

람다의 문법구조 Syntax 다음과 같습니다.(매우 간단하죠)

1. x는 이름입니다.

2. 는 함수를 뜻합니다. x는 함수의 인자 이고, E는 함수의 몸통입니다. x의 유효범위는 E입니다. E에 나타난 "x를 묶어준다고(binding)" 표현합니다.

3.E E를 다시 적어보면, E1 E2 로 표현된  함수를 적용하는 식입니다.  

      E1은 계산하면 함수 가 되어야 하고 E2는 그함수의 인자 x의 실체가 됩니다.

     (이 과정을 Beta-reduction이라고 합니다.)

풀이 과정은 주로 Beta-reduction으로 정리 되는데, 즉 람다 함수의 인자인 x에 대입하는 과정이라고 이해하면 되겠습니다.

문맥구조( context) C 는 빈칸[]을 딱 하나 품고있는 람다식입니다.

아래의 간단한 수식(?) 들을 이용하여 표현해 개념을 이해하고 넘어가겠습니다.

처치의 2와 3 같은 숫자는 두번 ,세번 과 같은 의미를 갖습니다.

그래서 

2 =  λfx.f(fx)

3 =  λfx.f(f(fx))

1 =  λfx.fx

0 =  λfx.x

와 같습니다. 

즉 f를 몇번 반복했는가가 의미가 있는 것입니다. 마치 숫자를 연산자나 함수처럼 다루는 것이죠.

예제로 3에 2승 을 계산 해봅시다. 

(P2)3 = ((λfg.fg)2)3

           = (λg.2g)3                         ----------  2g = (λfx.f(fx))g 2g는 g를 2번 수행하는 것 

           = (λg.(λfx.f(fx))g)3   = λfx.f(fx)3

           = λx.3(3x)  ------ (3x) 를 y로 치환하면, 3(3x) = 3y , 즉 y를 3번 수행하는 식이 필요함. (λfy.f(f(fy)))(3x)

           = λx.(λfy.f(f(fy))(3x))

           = λx.(λy.(3x)( (3x)( (3x)y) ) )

           = λxy. (3x)( (3x)( (3x)y) )

           = λxy. (3x)( (3x)( (x(x(xy)) ) )

           = λxy. (3x)( (x(x(x (x(x(xy))))) ) )

           = λxy. (x(x(x(x(x(x (x(x(xy))))))))) = 9 = 3^2

(3x)y  =  (&fz.f( f( fz ) ) x )y= (&z.x(x(xz)))y = x(x(xy)))

이런 Beta-reduction 과정에서   (λx.E)E1 과 같이 연산( 대입) 이 가능 한 부분을 레덱스 (redex)라고합니다.( reducible expression)

이 Beta-reduction 은 어떤 식에 따라서 영원히 계속될 수도 있습니다.

더이상 레덱스가 없을때 연산은 끝납니다. 이런 람다식을 정상식(normal term)이라고 부릅니다.

이 Beta-reduction 과정도 어떤 순서로 하는가에 따라, (즉, 어떤 레덱스 부터 바꾸는가에 따라) 결과가 달라집니다.

그래서 순서가 중요합니다.

정상순서로 계산하는 것은 normal-order reduction 이라고 하고, 제일 왼쪽 제일 위의 레덱스를 계산해가는 것입니다.

이 순서로 진행하면, normal term이 있는 람다식은 항상 그 정상식에 도달합니다.

여기서 의문점이 있을것인데요.

람다로 과연 프로그램 다운 프로그램을 짤 수 있을까요?

이 의문은 지금까지 다룬 식들이 대부분 산술 연산이었기 때문에 나오는 질문일 것입니다.

우리가 흔히 프로그래밍 이라고 하는것은,

1. 어떤 조건에 따라 분기를 해야 하고, 조건에 따라 다른 기능이 수행 되는 것을 의미할 것입니다.

다시 예기 하면, 논리 식에 따라 코드 분기가 가능한가? 라는 질문으로 단순화 시켜볼 수 있을것입니다.

그 식을 if e1 e2 e3  라고 하고, e1이 true이면 e2를 아니면 e3를 처리하면 되겠군요.

그전에 람다 언어에서 true 와 false에 대해서 정의가 필요합니다.

true = λx.λy.x

false = λx.λy.y

입니다.

하는김에 몇개 더 가져와 보겠습니다.

not = λb.λx.λy.byz

and = λb.λb'.λx.λy.b(cxy)y

iszero = λn.λx.λy.n(λz.y)x  or  λn.n (λx.FALSE) TRUE

succ = λn.λf.λx.f(nfx)

자 이제 준비가 되었습니다.

if e1 e2 e3  -> (e1 e2) e3

                  -> e1' e2 e3

                          1)  -> true e2 e3

                          2)  -> false e2 e3

1) true e2 e3  = (λx.λy.x)e2 e3

                  = (λy.e2) e3  ----> beta reduction 수행을 위해서 e3를 y에 집어넣으려 하지만 몸체에는 y가 없기 때문에 사라짐.

                  = e2

2) false e2 e3 = ( λx.λy.y) e2 e3  ------------> e2를 x에 대입. 그러나 x가 없음 e2는 사라짐

                  = (λy.y)e3

                  = e3

if e1 e2 e3 --> iszero e1 e2 e3

이렇게 해보니 그럴듯 하죠 . 언어같죠.. 람다 문법은 굉장히 단순하면서 프로그래밍 언어가 가지는 요소들을 다 품고 있습니다.

loop 을 구현하기 위해서는 기본적으로 재귀호출이 되어야 합니다.

아래와 같은 형식으로 람다에서 구현이 가능합니다.

In ML, C, Java & etc.

fun fac(n) = 

          if n=0 then 1

          else n*fac(n-1)

In λ-Calculus

      fac = Y(λf.λn. if n=0 1 n*f(n-1) )

      Y = λf.(λx.f(x x))(λx.f(x x))

Then 

     fac  n -> n!

언어 키우기.. M0

람다를 프로그래밍 언어로 바라봅시다. (이글 초반에 이미 그러자고 예기 했었죠? ^^)

λx.E 는 함수 정의로 봅시다. 그런데 함수 이름은 없습니다. 인자가 x이고 몸통이 E인 함수입니다. E1 E2는 함수를 적용하는 식입니다.

람다에서 계산과 프로그램에서의 실행은 조금 다릅니다. 람다에서 계산의 끝은 식의 모든 구석구석에 레덱스가 없는 경우입니다. 

함수식 λx.E 의 몸통 식 E에도 레덱스가 있다면 몸통식은 계산이 됩니다.

프로그램 에서는 λx.E 가 최종 값입니다. 몸통 E의 실행은 그 함수가 호출될때 비로소 시작됩니다.

이 최종값인  λx.E를 기준식 (canonical term)이라고 부릅니다.

기준식이 값이기 때문에 종종 υ("value" : upsilon)로 표기 합니다. 

소극적 실행 Lazy evaluation 과 적극적 실행 Eager evaluation

앞에서 β- reduction 과정에서 순서가 중요하다는 예기를 했었는데, 그것과 관련 있는 예기입니다.

프로그램이 실행되면서 함수는 자체로 값이 됩니다.  함수의 몸통은 그 함수가 호출될때 비로소 실행될 뿐입니다.

여기서 함수가 호출될때 E1 E2 ,  인자식 E2를 언제 실행해주기로 해야 할까요?

두가지 선택이 있을 것입니다. 몸통을 실행하면서 인자 값이 필요할 때에 인자 식을 실행하거나, 몸통을 실행하기 전에 인자 식을 실행해서 인자 값을 구한 후에 몸통을 실행하거나. 이 두가지 선택을 할 수 있을 것입니다.

첫번째 경우를 소극적 실행 Lazy evaluation, normal-order evaluation , 또는 식 전달 호출 방식 call-by-name, call-by-need 라고 합니다.

두번째 방식을 적극적 실행 Eager evaluation 혹은 값 전달 방식 call-by-value 라고 합니다.

람다 언어(우리가 람다 계산식을 바탕으로 키워가고 있는 언어) 에서 실행 방식을 정의하는 규칙은 다음과 같습니다.

각각의 장단점이 있습니다.

소극적인 실행으로 적극적인 실행 보다 빨리 계산 되는 경우가 있고, 반대의 경우도 있습니다.

소극적으로 실행하면

   (λx.7)((λx.x x)(λx.x x)) =>N 7

이지만 적극적으로 실행하면

(λx.7)((λx.x x)(λx.x x)) =>E (λx.7)((λx.x x)(λx.x x))

                                   =>E :

영원히 돌게 됩니다.(무한 루프)

반면,

아래를 소극적으로 실행하면,

   ((λx.(x..x))E =>N (E..E) =>N .....

E를 두번 실행해야 하지만,적극적으로 실행하면, 한번만 실행됩니다.

((λx.(x..x))E =>E (λx.(x..x)) υ =>E ( υ.. υ) =>E ...

람다언어의 문법을 시작합시다.

1. 이 언어에서 이름 지을 수 있는 것은 값 뿐입니다. 이것을 변수라고 합니다.

2. 변수 x 의 유효범위는 그 이름을 묶은 함수 λx.E 의 몸통 E입니다.

3. 각 변수가 무슨값을 뜻하는지는 그 변수를 묶은 함수가 호출될 때 전달되는 인자 값이 그 변수가 뜻하는 값이 됩니다.

의미 정의는 프로그램 텍스트를 변화시키지 않으면서 정의합시다.

"환경 σ(sigma) 에서 식 E는 값 υ를 계산한다" 는 뜻힙니다.

의미정의에서 환경을 따로 가지는 이유는 프로그램 식을 변경하지 않기 때문입니다.

변수는 그대로 프로그램에 남아 있는 것이죠. 예전처럼 프로그램 이름이 텍스트에서 해당 값으로 바꿔써지는 방식이 아닙니다.

값은 정수와 함수 뿐입니다. 

함수 값을 클로져(closure)라고 하는데, 함수  λx.E 텍스트 자체와 그 함수가 정의될 때 (static scope)의 환경입니다.

환경의 역할은  λx.E에서 자유로운 변수들의 값을 결정해주는 것입니다.

의미 규칙들은  적극적인 실행 규칙(Eager evaluation)을 같습니다.

언어키우기 M1

M0 를 가지고 모든 프로그램을 짤 수 있지만 불편합니다.

프로그래밍의 편의를 위해서 설탕을 좀 첨가할 필요가 있습니다. 설탕구조(syntactic sugar)

정수, 참/거짓

추가하고 싶은것들은 정수, 참/거짓, 재귀함수 rec f λx.E, 조건식 if E E E, 그리고 덧셈식 E+E

동치식  E=E. 등입니다.

가령 let x=E1 in E2  의 경우  (λx.E2)E1 이지만 사용하기 편리하게 그 자체로 그대로 둡시다.

이제 값들은 세종류가 되었습니다. 함수값과 정수 그리고 참/거짓

 구조가 있는 값 : 쌍 pair

구조를 가진 데이타를 프로그래밍하기 쉽게 하자.

쌍을 만들고 사용하는 방식을 제공합니다.

이제 값들은 세가지 종류가 있습니다. 함수값, 정수, 참/거짓,혹은 두값의 쌍

쌍을 M0로 표현하면

(E1,E2) =  λm.(mE1)E2

E.1 = E( λx. λy.x)

E.2 = E( λx. λy.y)

로 풀어서 쓸수 있습니다.

이 쌍을 이용해서 리스트, 나무구조(tree), 그래프도 표현할 수 있고 함수나 테이블도 표현할 수 있습니다.

리스트를 구현해보면 다음과 같습니다.

     λx.λlst.(x,lst)

"link 1 nil" 은 1 하나있는 리스트[1]

"link 1 (link 2 nil)" 은 [1,2]인 리스트를 만듭니다.

isNil?                              head                   tail           

λlst.(lst=nil)                    λlst.(lst.1)          λlst.(lst.2)

두갈래 나무구조 binary tree 를 구성해봅시다.

empty                     leaf              node

0                              λx.x                λlt. λrt.(link lt rt)

isEmpty?                 left                right

 λt.(t=empty)         λt.(t.1)          λt.(t.2)

다음 >> 값 중심의 언어- 메모리 주소 값 : 명령형 언어의 모습

타입 시스템.

실행되서는 안되는 프로그램들

프로그램을 만드는 방법을 충실히 따라서 제대로 생긴 프로그램을 만드는 것은 쉽습니다. 그런데, 그 중에는 실행될 수 없는 프로그램들이 많습니다.

(프로그램이라고 표현했지만, 좀 규모를 축소하면 코드라고 표현 하는게 프로그래머에게 더 와닫겠군요.)

실행되서 어떤 루틴에서 동작하지 않는 프로그램, 메모리를 과도하게 사용하여 시스템을 멈추게 하는 프로그램, 무한 루프에 빠진 프로그램.... 등등.

예를 들지 않아도 아마 대충은 감이 올것입니다.

실행되서는 안되는 이라고 했지만, 좀더 평범하게 표현하자면, 실행되지만 잘 돌지 않는 프로그램이라고 표현하는 것이 좋겠네요.

프로그램을 만드는 방법( 문법) 적으로는 문제가 없지만, 실제로 동작했을때 제대로 실행되지 않는 프로그램들이 있습니다.

사용자들은 제대로 동작하는 프로그램들을 동작시키길 원하고, 이런 프로그램들을 미리 확인하고 싶어합니다.

컴퓨터 사이언스에서는 이런 프로그램들을 찾고 검증하는 기술들이 점점 발전하고 있습니다.( 물론 완전한 프로그램은 없습니다... Halt problem ...)

다른 분야들에서는(기계설계, 건축 등) 인공물들이 자연세계에서 문제 없이 동작할 지를 미리 분석하는 수학적 기술들이 잘 발달해 있습니다.

뉴튼 역학, 미적분 방정식, 통계 역학 등등.

소프트웨어 분야에서는 아직 완전한 기술들은 없지만, 최종 목표는 소프트웨어가 오류없이 작동할 지를 실행전에 자동으로 검증하는 기술을 이룩하는 것입니다.

이 축을 따라 프로그래밍 언어에서 , 프로그래밍 언어가 어떻게 디자인 되면 이문제가 어디까지 해결될 수 있을까? 프로그래밍 언어 분야에서는 이 시급한 문제에 어떤 답을 내 놓고 있는가?

현재 어느 정도 수준인가?

프로그래밍 언어 분야를 돌이켜 보면, 다음과 같은 단계를 거치면서 한발짝을 나아가고 있습니다.

1.  우리가 확인 할 수 있는 오류의 한계를 정확하게 정의한다.

2.  정의한 오류의 존재를 찾는 방법을 고안한다.

3.  컴퓨터가 자동으로 실행할 수 있도록 소프트웨어를 만든다.

각 단계별로 애매하고 허술한 구석이 없을때에만 비로소 한 발짝의 전진이 있게 됩니다. 이 단계들이 반복되면서 소프트웨어의 오류의 정의는 점점 정교해집니다.

현재 이렇게 해서 발전된 단계는 겨우 두발자국 이라고 합니다.

1세대 기술 : 문법 검증 기술

1970년대에 달성된 첫 발짝은 ,생긴게 잘못된 프로그램을 찾아내는 기술입니다.

이 기술은 안전하고 빠뜨림 없이 문법이 오류인 것을 찾아주는 것을 의미합니다.( 새로운 것이 아니라 이미 우리는 이렇게 코딩하면서 컴파일러를 통해서 오류들을 찾아내고 있습니다.)

그러나, 여전히 제대로 동작하지 않는 프로그램을 찾아 내지는 못합니다.

2세대 기술 : 타입 검증 기술

1990년대에 빛을 보기시작한 기술입니다.

이때의 오류의 정의튼 겉모양이 틀린 프로그램 외에 속 내용이 잘못되어있을 수 있는 경우를 포함합니다.

프로그램 실행은 일종의 계산인데, 계산중에는 분별있는 일들이 일어납니다. 

더하기에 숫자만 들어와야 한다. 수력발전하기 에는 물이 들어와야 한다. 햄버거 만들기에는 퍼티와 빵이 들어와야 한다...

등등의 분별력있는 계산식과 그에 맞는 데이타가 필요한데, 그렇지 않는 경우들이 발생되면, 프로그램은 생각대로 동작하지 않습니다.

타입이 맞지 않는 계산이 실행중에 발생할지를 미리 검증하는 방법이 타입검증입니다. 프로그램의 안전한 타입검증은 그 프로그래밍 언어가 제대로 디자인된 경우에만 가능합니다.(ML, OCaml, Haskell)

프로그램 E의 문법 규칙을 다음과 같다고 하자.

이 때 2+"a" 는 문법 규칙에는 맞습니다. 하지만 프로그램의 흐름상 잘 동작하리라는 보장은 못합니다.

우리는 + 식에 대해서 두개의 부품식은 모두 정수여야 한다는 규칙이 필요합니다.

하지만, 문법 규칙에는 대개 표현하지 않습니다.

이런 문법을 표현하게 되면, 우리는 "문법규칙" 의 영역에서 "타입 시스템"의 영역으로 은근 슬쩍 넘어가게 됩니다.

"x+1"이 말이 되려면, x는 정수여야 합니다. 텍스트가 가지는 속 내용을 문맥으로 고려해야 합니다. 

우선 이를 해결하기 위해서 타입시스템을 만들어봅시다.( 실제로 이미 만들어진 시스템을 학습하는 차원에서 한발 한발 나아가는 것입니다.)

우선 실행중에 위에서 x가 정수인지 아닌지 판단하는 것을 실행기(interpreter)에서 구현했다면, 이를 동적 타입 검증 (dynamic type checking)이라고합니다.

덧셈 "E1+E2"의 두식이 "+" 연산을 하는 시점에 E1이나 E2가 정수가 아닌지 판별하려면, E1식의 결과가 정수이어야 하고, E2의 결과가 정수이어야 합니다.

"+" 연산 시점에서 비로소 판단 할 수 있는 것입니다.

쉽게 만들어지겠죠.? 

그러나 우리에게 필요한 것은 정적 타입 검증(static type checking) 입니다. 프로그램 실행전에 타입을 검증하기

즉, 문제를 미리 찾아내고 무결점임을 확인한 후에 실행을 시작하는 것이 필요합니다.

여러번 언급했던것 처럼 오류를 완전하게 찾아내는 시스템은 만들 수 없습니다. 그렇기 때문에 믿을만한, 안전한, Sound한 시스템 이었으면 합니다.

타입 검증 시스템이 문제 없을 것이라고 했는데 실행중에 문제가 발생하는 경우가 없었으면 좋겠다는 것입니다.

Type

우리가 정의한 언어에는 계산하는 값들의 종류가 5가지입니다.

다음 과정을 통해 type을 정의해봅니다.

1. 기본 값(primitive value)의 종류마다 이름을 붙입니다.

2. 레코드 는 복합 값입니다. 레코드의 부품들로 만들어진 복합타입을 갖습니다. (compound value,compound type)

3. 메모리 주소는 값을 보관하고 있고, 메모리주소의 타입은 보환하고 있는 값의 타입에 따라 분류한 복합 타입입니다.

4. 프로시져는 값은 아니지만 그 타입을 가지고 호출식들이 제대로 쓰이는 지 확인할 필요가 있습니다.

타입검증 규칙

                                              "식 E가 제대로 실행되고 만일 끝난다면 타입 r(tau)의 값을 계산한다" 

을 증명하는 논리 규칙들은 다음과 같습니다.

T(Gamma)는 프로그램에 나타나는 이름들의 타입을 가진 테이블입니다.

   :

   :

재미있는 사실은 이 타입 시스템은 프로그래머가 타입에 대해서 프로그램 텍스트 안에 써 넣은 것이 전혀 없습니다.

(우리는 실제로 이런 언어가 있다는 것도 알고 있습니다.)

이 타입 시스템을 보면, 프로그램의 구석구석이 어떤 타입을 갖는다고 판단 될 수 있는지 순수하게 논리 시스템으로 바라보자.

이 시스템은 그럴듯 하지만 아쉬운 면이 있습니다.  안전(sound)하지도 완전(complete)하지도 않습니다. 이 두가지 문제를 자세히 다루겠습니다.

안전하지 않다.

타입시스템이 문제없다고 판단한 프로그램이 실행중에 타입 오류로 멈출 수 있습니다.

type 리스트 = {int x, 리스트 next }

let 

   리스트 node = {x:=1, next:={}}

in 

   node.next.x

end

위와 같은 프로그래밍은 C나 C++에서 흔히 보는 경우입니다.

"상식 수준에서 " 키워온 우리 언어에서는 해결할 수 없습니다. 언어를 다지아니 할 때 부터, 이 문제를 염두에 두고 잘 디자인 해 가야 해결 할 수 있는 문제입니다.

(C나 C++등 초창기에 만들어진 언어들에서는 알려지지 않은 오류들이었을 것입니다. 그래서 그 당시에는 이런 문제가 있을 것이라는 예상이 불가능 했을 것이고 말이죠. )

안전하게 되기 위해서 지금까지 설명했던 우리의 언어는 제 정의될 필요가 있습니다. 더이상 이전의 언어는 아닐 것입니다.

안전한 타입 시스템을 고안하고 구현할 수 있게 된다면, 그 타입 시스템을 통과하는 프로그램은 매우 소수가 될 것입니다.

그런 프로그램은 제한된 기능만 가지고 작성된 프로그램들이 도리것입니다.

또, 안전하게 되기 위해서 매우 정교한 타입 시스템을 고안하게 될것이고, 그 정교함이 극에 달해서 아마도 지금의 기계로는 구현할 수 없는 것이 될것입니다.

어떻게 실용적인 범용의 언어가 이 문제를 해결한 편리한 타입시스템을 갖추게 되었는지 는 값 중심의 언어에서 다루게 될것입니다.

그 전에 좀더 타입에 대해서 다뤄볼 필요가 있습니다.(두번째 문제점을 다룰 차례죠)

완전하지 않다.

제대로 도는 프로그램중에서 위의 타입 시스템을 통과하는 것은 일부분 입니다.

제대로 잘 도는 프로그램도 타입이 없다고 판단할 수 있습니다. 

1. 메모리 주소의 타입이 변할 수 가없다.

    메모리 주소에 처음으로 보관되는 초기값의 타입이 그 주소가 저장할 수 있는 값들의 타입으로 고정됩니다.

2. 어떤 프로시져는 인자값의 타입에 상관없이 실행될 수 있는 프로시져 들이 있다. 

    이러한 프로시져는 다양한 타입의 인자를 받으면서 아무 문제 없이 실행될 수 있습니다.

    그러나 이 타입 시스템은 통과 할 수 없습니다.

3. 레코드 타입 관련해서도 타입 검증이 너무 까다롭다.

   복합적인 데이타를 표현하는 데 쓰이는 레코드의 타입이 유연하지 않습니다.

   리스트를 예로 들어보면,

lst의 next 는 빈 레코드 타입으로 고정될 수 없습니다.초기에는 빈 레코드이지만 다음 라인에서 다른 레코드로 변경되어 버렸습니다.

즉, static하게 next의 타입을 판단 할 수 없다는 의미가 됩니다.

이 문제는 타입의 안정성을 개의치 않는다면 쉽게 해결 방법이 나옵니다. (대부분의 현재 언어들이 취하고 있는 방법입니다.)

프로그래머가 타입을 정의하고 이름을 지을 수 있도록 합니다.

그리고 그 이름이 타입 정의에서 재귀적으로 사용될 수 있도록 합니다.

                         type list = {int val, list next}

이렇게 정수를 가지는 val 필드와 재귀적으로 list를 품을 수 있는 next 필드로 표현하고, 리스트의 깊이는 표현할 필요가 없습니다.

1. 타입 이름들의 유효범위는 프로그램전체가 되도록 하였습니다. 

2. 타입 이름들이 정의 되는 곳은 프로그램의 처음 부분 뿐입니다.

빈 레코드의 식은 임의의 타입으로 결정될 수 있다고 타입 규칙으로 정의합니다.

대신 

로, 빈 레코드를 초기에 가지게 되는 리스트 레코드의 next 필드는 list타입이 되는 것으로 판단 되는 것이다.

  lst :={val:=0,next:={}};

  lst.next:= {val:=100,next:={}};

lst의 타입은 list loc으로 판단할 수 있고, 두번째 줄의 지정문도 타입 검증을 통과합니다. lst.next 도 list loc 이기 때문입니다.

여기서 중요한 아이디어는 이름을 사용한다는 것입니다. 타입에 이름을 붙이고 그 이름으로 속 내용을 감춥니다.

재귀적인 구조를 구현하는 레코드는 재귀 고리 역할을 하는 필드가 있습니다.

임의의 깊이로 레코드를 품을 수 있는 필드의 타입을 사용해야 하지만 이를 표현하지 않기 위해서 이름을 사용하는 것입니다. 

이 해결책 역시 어설픈 이유는, 타입 시스템이 안전하지 않은 문제가 해결되지 않았기 때문입니다. 

안전성을 포기하고 이렇게 고안된 방법들이 현재 대부분의 프로그래밍 언어에 적용되었습니다.

자! 다시 좀더 깐깐하게 짚어보면, 위의 타입시스템으로 작성된 프로그램의 구석 구석 타입이 제대로 되었는지 증명해 낼 수 있을까?

타입 규칙들은 의미규칙과 다른 양상이 있습니다. 타입 검증기 구현은 의미규칙을 보고 실행기를 구현할 때와 같이 간단하지 않습니다.

이 구현의 문제를 간단히 넘어가는 방법(선택의 여지가 없었는지도 모른다)은 프로그래머가 타입 검증을 돕는 코맨트를 프로그램 택스트에 포함시키도록 강제하는 것입니다.

C,C++,Pascal, Java 등의 언어가 이런 방식으로 구성되어있습니다.

의 증명을 구현하는 타입 검증 함수의 입력은 두가지가 될것입니다. 프로그램 식 E와 T(Gamma).

주어진 두개의 입력에 대해서 타입 검증 함수는 위의 타입 판단에 해당하는 r(tau)가 있는지를 찾게 됩니다.

타입 환경 T는  프로그램에 나타나는 이름들의 타입들에 대해서 알려진(가정) 내용입니다.

이것을 가지고 프로그램 텍스트 E가 타입 r를 가질 수 있는지 타입 규칙에 준해서 알아보는 것입니다.

프로그램 전체에 대해서는 시작 T는 물론 비어있을 것입니다. 타입 검증 함수가 프로그램의 부분들에 대해서 재귀적으로 호출되면서 T에 정보가 쌓이게 됩니다.

우리의 타입시스템에서 구현이 어려운 이유는 다음 규칙에서 드러납니다.

타입 검증에서 함수에 입력으로 줄 타입환경

은 이미 우리가 알아내야할 r1과 r2가 사용되고 있습니다. 그 두 타입들이 프로시져의 타입을 구성하기 때문입니다.

출력으로 알아내야 할 것을 입력으로 넣어 주어야 하는 것입니다.

이렇게 x의 E1의 타입을 프로시져에서 명시적으로 주면 간편해 집니다.

지금까지의 내용을 종합해서 프로그래머가 타입을 프로그램 코드( 택스트) 에 포함시키도록하자. 

프로시저와 변수의 타입을 프로그래머가 명시하도록 하는 것입니다.

이 문법으로 프로그래밍을 하면 다음과 같습니다. 그리고 타입 검증이 통과 할 것입니다.

타입 환경(type environment)이 이전에는 프로그램에 나타나는 이름들 (변수, 프로시져 이름, 레코드 필드)의 타입에 관한 것이었으나, 이제부터는 타입 이름들의 속 내용(타입)에 대한 환경도 필요해 집니다.

타입에 대해서 다른 두가지 이슈가 더있는데 이부분에 대해서 간단히 언급하겠습니다.

우선 이름 공간(namespace)와 같은 타입 (type equivalence)에 대한 내용입니다.

우리 언어에서는 많은 것에 이름을 지을 수 있습니다. 메모리 주소(변수), 레코드의 필드, 플그램코드(프로시져), 타입에 이름을 정할 수 있었습니다.

타입 이름은 프로그램 전체가 유효범위 였고, 변수 이름과 프로시져 이름은 유효범위를 한정할 수 있었습니다.

같은 이름으로 타입 이름이나 변수 이름으로 사용해도 프로그램 텍스트에서 문제 없이 구분 할 수 있었습니다.

타입 이름과 메모리 주서의 이름은 다른 이름 공간을 가지고 있다고 예기 할 수 있고, 프로시저 이름 과 변수 이름은 같은 이름 공간을 공유합니다.

같은 타입이란 무엇인가?

type a= {int x; int y}

type b= {int y; int x}

내용이 같더라도 위와 같이 이름이 다르면 다른 타입인 것으로 정의(name equivence) 할 수도 있고, 내용만 같다면 같은 타입으로 정의(structural equivalence)할 수 도 있습니다.

우리의 언어에서는 타입 이름이 같아야 같은 타입인 것으로 정의한 셈입니다.

여기까지 해서 기계중심의 언어, 즉 상식선에서 프로그래밍 언어를 디자인 했던 과정을 따라가 보았습니다. 현재 널리 쓰이고 있는 명령형 프로그래밍 언어들이 만들어진 과정이기도합니다.

그 대표적인 언어가 C 언어 입니다. 어떻게 프로그래밍 언어를 디자인해야 하는지, 무엇이 문제일지가 드러나지 않은 상태에서 , 주어진 디지털 컴퓨터를 편하게 사용하기 위한 도구로서 프로그래밍 언어를 디자인 했던 과거죠.

현재 시점에서 바라보면 아쉬움이 많습니다.

다음 >> 값 중심의 언어

메모리 관리

컴퓨터가 프로그램을 실행할 때 소모하는 자원은 시간과 메모리입니다. 시간은 무한하지만, 메모리는 유한합니다. 프로그램이 한없이 메모리를 소모할 수는 없습니다.

메모리가 어디에서 소모되는지 볼 필요가 있습니다.

프로그램 실행중에 메모리는 let- 식과 프로시져 호출식의 실행을 위해 하나씩 소모됩니다.

let 식으로 선언된 이름과 프로시져의 인자 이름을 위해 매번 새로운 메모리가 소모됩니다. 그리고 소모되기만 합니다.

이렇게 메모리만 소모시키면 언젠가는 프로그램을 더이상 수행 못하게 되겠죠.

따라서 메모리를 재활용 해야 합니다. 그러면 어떤 메모리를 재활용 해야 하는가?

프로그램 실행중 사용한 메모리중에서 더이상 사용하지 않을 메모리를 재활용 해야 합니다.

그럼  어떻게 더이상 사용하지 않을 메모리인지를 알아 낼 것인가?

앞에서 우리가 디자인한 언어의 경우에는 쉽습니다. 메모리 주소의 사용기간이 곧 그 주소의 이름의 유효범위 이기 때문입니다.

메모리 주소는 하나의 이름만 붙고 그 이름을 통해야만 그 메모리 주소를 사용 할 수 있기 때문입니다.

우리의 언어에서는 let 식의 마지막이나, 프로시져의 마지막입니다. 

언어가 복잡해지면, 이렇게 간단하게 메모리 재활용이 안되죠..(garbage collection)

메모리 주소가 따로 프로그램 식의 결과값으로 프로그램 여기저기로 흘러다니면, 메모리 주소의 사용기간은 그 주소에 붙은 이름의 유효범위와 일치하지 않게 됩니다.

이런 언어의 경우 메모리관리는 어떻게 해야 할까요... 

이 문제는 좀 미뤄 둬야 할것 같습니다. 아직 이 문제를 다룰 단계가 아니기 때문이죠. 우리 언어는 아직 이런 기능이 없죠.

현재 우리가 설계한(사실은 과거의 언어를 따라서 규칙을 하나하나 추가한것이죠) ,이름을 붙일 수 있는 메모리 주소와 프로그램 코드, 이름의 유효범위, 재귀호출 , 값전달과 주소전달 호출이 가능하고,

while, for 식으로 반복이 가능합니다.

리스트나 나무구조를 만들고 사용하는 프로그램을 짤수 있을까요? 집합을 만들고 사용하는 프로그램을 작성할 수 있을까요? 할수는 있습니다.

그러나 , 손쉽게 다룰 수 있도록 프로그래밍 언어에서 지원이 되면 좋겠습니다.

기초적인 값 이외에 구조가 있는 값을 프로그램에서 손쉽게 다룰 수 있도록 하려면, 구조가 필요합니다.

기초적인 값은 메모리 주소 하나면 됩니다. 구조를 갖춘다는 것은 여러개의 기초적인 값들을 모아서 하나의 새로운 형태를 만든다는 것입니다.

즉, 여러개의 메모리 주소가 필요하게 됩니다. 메모리 뭉치가 됩니다. 이를 레코드(record)라고 합시다. C에서는 struct이라고 하죠.

이렇게 뭉쳐진 메모리 안에 각각의 메모리 주소들도 이름이 있습니다. 레코드 필드라고 합시다.  배열도 메모리 뭉치입니다. 각각의 메모리 주소들의 이름이 자연수로 되어있죠.

로 표현 할수 있습니다.

값들은 레코드 까지 포함하게 되었습니다. 

프로그래밍 언어에서 레코드를 만들고 사용하는 문법이 아래와 같이 제공 됩니다.

레코드에 이름을 붙이고, 레코드의 필드가 아래와 같이 사용됩니다.

let

   item:= {id:=200012, age:=20}

in 

   item.id + item.age

이제 나무를 작성하는 것이 쉬워졌습니다.

let

    tree := {left:={},v:=0, right:={}}

in

   tree.right := {left:={}, v:=2,:right:=3};

   shake(tree)

이렇게 레코드가 메모리 뭉치를 뜻하면서, 그리고 레코드가 값이 되면서, 메모리 주소의 사용기간을 간단히 알 수 없게 되었습니다.

...

f( let tree:={left:={}, v:=0, right={}}  in tree })

...

포인터 : 메모리 주소를 데이타로

지금까지의 값들은 자유자제로 사용되었습니다. 변수에 저장되기도 하고 프로시저에 전달되기도 하고 프로시져의 결과값이기도 하였습니다.

값들로 자유롭게 움직 일 수 있다는 것은 이름이 붙어 있을 필요가 없이 계산 될 수 있음을 의미 하기도 합니다.

정수마다 이름을 붙여 사용한다거나, 레코드마다 이름이 있어야 하고, 정수를 더할때 마다 그 결과에 이름을 붙여야만 한다면,

불편할 것입니다. 그리고 불평은 당연한 것입니다.

지금까지 항상 이름을 붙여야만 사용할 수 있는 값들이 있었습니다. 메모리 주소와 프로시져 였죠.

메모리의 주소를 이름 없이 쓸 수 있게 하려면, 값들 중에 메모리 주소 역시 값이 되게 하면 됩니다.

프로그램에서 메모리 주소를 값으로 다룰 수 있으려면,문법을 제공해야 합니다.

malloc E와  &- 식은 메모리 주소값을 만드는 식입니다.

레코드는 메모리 주소 뭉치이고, 레코드는 값이므로, 레코드를 이용해서 메모리 주소가 값으로 여겨지는 프로그램을 할 수 는 있습니다. 

어떻게 ?

1. *E는 그 자체가 식인 경우와 메모리 지정문의 왼쪽에 있을 경우, 의미가 다르다.

  *E가 지정문의 왼쪽에 있는 경우 E가 뜻하는 메모리의  주소값을 뜻한다.

  *E가 지정문의 오른쪽에 있을 경우 E가 뜻하는 메모리 주소에 보관되어있는 값을 뜻한다. 

(C 언어가 이렇게 되어있지요.)

그래서 다음 프로그램을 실행 시키면,

let 

   x:= malloc(2)

in

   *x := 1;

   *(x+1) := *x+2

x의 주소의 위치에 1을 담고, 다음 위치에 3을 담습니다.

메모리관리

메모리 블럭을 설정하는 방법이나, 레코드 등에 대해서 정의하는 법이 만들어졌으니, 이제 재활용에 대해서 본격적으로 고민해볼 차례입니다.

초기에 작성했던 언어의 경우에는 메모리와 메모리 주소의 이름의 사용기간이 일치했기 때문에 메모리 재활용이 쉬웠습니다.

그러나,  지금은 쉽지 않습니다.

어떻게 해야 할까요?

수동 메모리 재활용

해결을 미루는 쉬운 방법이 있습니다. 메모리 재활용을 프로그래머에게 맡기는 것입니다. 메모리 재활용이 안되는 문제는 프로그래머의 책임으로 ...

그래서 프로그램 언어에 메모리 재활용 명령문을 제공하는 것입니다. (C가 이렇습니다.)

free E 식의 의미를 정의 해봅시다. 식 E는 메모리 주소를 계산합니다. 그 주소는 반드시 할당받은 메모리 주소이어야 합니다. 메모리 뭉치를 재활용하려면 메모리 뭉치 에 포함된 모든 주소를 재활용 해야 합니다.

\frac { \sigma,M\vdash E \Rightarrow \ell,M' }{ \sigma, M\vdash free\quad E \Rightarrow \cdot ,M' } \quad \ell \in Dom \quad M

좀이상합니다. 메모리 재활용 효과가 표현되지 않았습니다.메모리 재활용 효과가 표현되지 않아도 충분한가???  

메모리 재활용은 이제 프로그래밍 언어 밖의 일이 되어버렸습니다.

언어의 의미정의 목적은 우리가 필요로하는 디테일의 정도에서 혼동이 없게 정의하는 것입니다. 메모리 재활용에 대해서 명시 할 필요는 없습니다.

이 언어의 의미정의로 메모리 관리에 대해 알 수 있는 사실들은.

1. 새 메모리가 필요할 때, let-식이나, 프로시져 호출, 레코드 식, malloc 식, 새로운 메모리는 항상 있어야 한다.

2. 메모리 주소에 저장된 데이타가 없을 때, 그 주소를 접근 하는 식은 의미가 없다.

    let x:= malloc(1) in *x

3. 할당된 메모리들은 서로에게서 서로에게로 도달할 수 있는 방법이 없다. 할당 받은 주소로 부터 몇 발자국을 움직여서 별도로 할당받은 다른 메모리에 도달할 수 있는 방법은 없다.

  ( 이 부분은 C와 다른 점이기도 합니다. C에서는 임의의 주소로 접근이 가능하기 때문이죠)

자.. 오랜 기간동안 문제가 되어왔던 "메모리 재활용을 프로그래머에게 미루는 것은 바람직한 것인가?".

어쩔 수 없는 선택이라고 봐야 할 것입니다.

언어가 복잡해 질 대로 복잡해졌고, 메모리 재활용 방안은 없고.... 

프로그래머가 신경 써야 할 것은 많아졌습니다. 프로그램의 논리적인 흐름만이 아니라, 유한한 메모리를 가진 컴퓨터가 자신의 프로그램을 실행하게 된다는 조건을 염두해 두어야 하고, 적절한 시점에 메모리를 해재 해줘야 합니다. 사용한 메모리 주소 마다 말이죠.

다른 질문, 과연 프로그래머가 자신의 프로그램이 소모하는 메모리의 사용기간을 가장 잘 알 수 있는가? 정말로 그런가?

C 프로그래밍의 경험이 지난 20년 넘게 쌓이면서, 그 대답은 "아니다" 라고 결론이 났습니다. 현재 프로그래머가 가장 많이 하는 실수가 메모리 재활용 오류입니다.

메모리 관리를 프로그래머에게 맡기면서 C 프로그램의 가장 골치아픈 오류가 메모리 재활용이 되었습니다.

그 오류는 두가지 인데,  재활용 지점을 너무 늦게 잡는 오류와 너무 늦게 잡는 오류입니다.

너무 늦게 잡으면 메모리 자원이 고갈되고, 너무 빠르게 잡으면, 사용중인 메모리가 용도변경이 되어버리는 것입니다.

memory leak 과 dangling pointer 죠.

자동 메모리 재활용

메모리 재활용은 사실 프로그래머가 제대로 완벽하게( 안전하게 말구요) 처리하는 것은 어렵습니다. 제 경험도 그렇고, 여러사람들의 경험을 들어봐도 그렇죠..

자동 메모리 재활욜의 개념은 ... 

1. 프로그램 실행은 계속 메모리를 소모한다.

2. 메모리 소모량이 어느 수위에 오르면, 실행을 잠시 멈춘다.

3. 메모리를 재활용한다.

4. 이제 컴퓨터의 메모리 자원이 풍부해졌다.

5. 멈춘 프로그램의 실행을 재개한다.

가능할까? 

프로그램이 멈추고, 앞으로 사용하지 않을 메모리를 찾아서 재활용해야 합니다. 그런데 과연 앞으로 사용하지 않을 메모리를 찾아서 재활용한다는 것이 가능한것인가요?

어떻게 앞으로 사용하지 않을 것을 알까요?  어렵습니다. 사실은 모든 사용하지 않을 메모리를 찾는 것은 불가능합니다. 빠.짐. 없. 이.찾는 것...

확신을 어떻게 할 수 있을까요? 모든 재활용 할수 있는 메모리를 찾을 수 있다는 것은, 이미 불가능하다고 증명된, Halting problem 을 푸는 프로그램을 작성할 수 있다는 것이 되기 때문입니다.

Halting problem program역시 메모리를 사용할  것이고, 이 프로그램의 재활용 가능한 메모리를 빠짐없이 재활용 할 수 있다는 의미가 되기 때문입니다.

이것이 디지탈 컴퓨터의 한계라고 합니다.  

여기서 조건을 조금만 완화하여 그럴듯한(?: 완전하지 않지만, 쓸만한)  재활용 이라고 하면, 우리에게 가능성이 생깁니다.

- 몇개는 빠뜨릴 수 있지만, 꽤 많은 부분은 재활용 해주는 프로그램을 만들수 있다.

원칙 : 프로그램의 진행을 멈추고 나서, 지금까지 할당된 메모리중에서 미래에 사용할 수 있는 메모리를 제외하고 나머지는 모두 재활용해야 한다.

사실: 재활용을 완전하게 할 수 있는 방법은 없다. 

양보: 재활용을 안전하게 할 수 있는 방법은 있다.

- 앞으로 실행할 식인 E만 있다고 하자, 식 E의 현재 환경 environment 으로 부터 현재의 메모리를 통해 다다를 수 있는 모든 주소들은 앞으로 E를 실행중에 다시 사용될 수 있다. 

이것들만 빼고 재활용하자. 즉, 그렇게 해서 다다를 수 없는 메모리 주소들은, 과거에 할당되어 사용되었으나 앞으로의 E를 실행하는데 사용되지 않을 것이 분명하므로,

재활용 해도 된다.

현대 언어들의 메모리 재활용기 (GC: garbage collector)는 위의 방식으로 구현되어있습니다.(Java, ML, Scheme, Haskell, C#, Prolog, etc)

메모리 재활용기(Garbage collector) 구현 알고리즘은 대표적으로 두가지가 있습니다.

프로그램 실행중에 메모리에 만들어진 구조물들을 모두 따라가면서 앞으로 사용될 수 있는 메모리 주소들을 모으게 됩니다. 

메모리가 없어서 메모리 재활용기를 돌리는 것인데, 메모리를 필요로 하게 되죠.

위의 방법으로 메모리 주소들을 모으기 위해서는, 그래프를 누비고 다니는 알고리즘(depth-first-, breath-first-traversal  algorithms )들은 메모리를 소모합니다.

그래프의 가장 긴 경로만큼의 스택을 갖게 되죠.

그러면, 메모리를 소모하지 않고 그래프를 누비는 방법이 있을까요? 스택없이 가능한 알고리즘이 있습니다.

1. 헨델과 그레텔 알고리즘 -Mark & Sweep

2. Stop & copy 

- 메모리 영역을 2개로 나누고, garbage collection이 발생할때, 다른 메모리 영역으로 copy함.

- fragmentation 발생이 거의 없음.

- 메모리를 반밖에 사용할 수 없음.

- copy overhead가 있음.

3. generational 

-  모든 메모리를 탐색하는 것보다, 일부만 탐색하도록 하여 속도를 높이는 방법.

   - 생성된 시기별로 세대를 나눈다.

   - Heap을 두개 이상의 sub heap으로 나눔.

   - 객체가 처음 생성되면, 0 번 세대의 heap에 할당.

   - 0세대의 Garbage collection이 수행될때, (대부분 객체는 수명이 짧기 때문에 사라짐,) 살아남은 메모리들은 다음 세대로 넘어감

다음 >> 타입 시스템

기계 중심의 언어

초기에 컴퓨터 사이언스는 튜링 머신이나 람다 컬큐러스를 기반으로 컴퓨터와 프로그래밍 언어를 만드는 것에 의의가 있었고, 그러다 보니 자연스럽게 기계 자체를 동작시키는데 가장 큰 목적이 있었습니다.

그 당시는 이제 시작 단계라서 어떻게 프로그래밍 언어를 디자인해야 하는지 무엇이 문제일지가 드러나지 않은 상태 였습니다.

 처음에 기대했던, 기계중심의 언어는 이런것이다.!! 라고 간단하게 정의 되어있을 것이라 기대하고 읽기 시작 하실 것입니다.

그러나, 내용은 사실 그렇게 명쾌하게 나오지 않습니다. 언어가 어떤 수학적 정의를 바탕으로 설계가 되었고, 

그 한계가 무엇인지는 프로그래밍 언어의 요소들을 하나 하나 살펴보면서  짚어갈 수 밖에 없습니다.

예를 들면 변수란 무엇인가? 함수는 무엇인가? 재귀 호출이 무엇인가?  하는 것들이죠. 이미 프로그램 개발 경험이 많고, 여러가지 프로그래밍 언어 교제들을 통해서, 다들 알고 있는 개념들입니다.

하지만 그것들이 무엇인지 정확하게 수학적으로 어떤 의미가 있고, 그래서 어떤것이 미흡한지에 대한 이해와는 다를 것입니다.

언어의 요소들에 대해서 깊이있게 이해하고 새로운 시각을 갖기 위한 과정이 이 programming language principles  입니다. 

"옆에 컴퓨터가 있다, 사용해야 한다, 컴퓨터에게 시킬 일을 편하게 정의할 수 있는 방법을 고안하자." 이렇게 해서 C언어를 만들었던 과정은 .....

아.주. 상식적인 과정(현재에서 바라봤을때)을 밟았습니다.

이 과정들에는 현재 불합리한 부분들도 있고, 이런 과정을 바탕으로 프로그래밍 언어의 발전에서 살아남은 것들도 있습니다. 

우리는 이 살아남은 것들은 앞으로도 살아남을 가능성이 매우큰 것들이고, 우리는 이런 것들을 확인하고 이해해둔다면,  프로그래밍 언어와 컴퓨터 사이언스 부분에 대한 이해의 폭이 넓고 깊어질 것이라 보입니다.

어쩌면 현재의 바람직한 프로그래밍 기술 및 기법들은 미래에 보면 어설픈 모습으로 보일 가능성이 있습니다.

주어진 기계 - 메모리, 중앙처리장치, 입출력이 가능하다.

중앙 처리장치는 기초적인 기계어 명령들을 처리하는 실행기 입니다. 실행할 수 있는 기계어 명령의 갯수는 유한하고 고정되어 있습니다. 

(매우 작은 전기줄로 구성되어있고...)

그 기계는 폰 노이만 머신(Von Neuman machine) 입니다.        

"기계가 실행할 명령문들이 메모리에 보관될 수 있다. 그 기계는 명령문 하나 하나를 메모리에서 읽어와서 실행한다. 명령문 들에 따라 그 기계는 다른 일을 한다" 그 명령문들이 프로그램이죠.

이렇게 기계를 구동시키는 명령어들을 다루는 방식을 좀더 편리하게 사용해보자... 언어입니다. 기계어 보다 좀더 상위의 언어를 고안해봅시다. (사실은 이미 있는 것을 밟아나가갔던 과정을 지나가봅시다.)

1. 변수 : 메모리 주소에 이름 붙이기

 "명령문 여러개가 순서대로 실행된다. 반복이 있다. 입출력이 있다. 조건에 따라 명령이 구분되어 실행된다."

이런 기초적인 조건들을 갖는 기초적인 문법의 언어가 있습니다.

명령문

Command\quad C\quad \rightarrow \quad skip \\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad x:=E\\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad C;C \\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad if \quad E \quad then \quad C \quad else \quad C \\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad while\quad E \quad do \quad C\\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad for  \quad x:=E\quad to \quad E \quad do \quad C\\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad read \quad x \\

\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad|\quad write \quad E

식

프로그램

각 명령문과 식의 의미를 정확히 정의할 필요가 있습니다.

우선 의미를 정의해갈 때 사용할 원소 semantic object들이 어느 집합(의미공간) semantic domain 의 원소들인지를 정해야 합니다. 

1. 값은 정수거나 참/거짓이다.- 값의 집합은 정수집합이거나 참 거짓의 집합이다.

2. 메모리는 기계적으로는 전기줄에 매달린 트랜지스터 이겠지만, 좀더 추상화 시키면, 논리 게이트, 더 추상화 시키면 주소에서 값으로 가는 테이블 입니다.

3. 테이블은 수학적으로는 하나의 함수입니다. - 정의 구역은 메모리 주소, 공변역은 값.

4. 정의 구역은 메모리 주소 집합중에서 유한한 집합이다.

5. 주소는 프로그래머가 사용하는 이름들의 집합으로 정의한다.

의미공간( semantic domain) 들은 아래와 같습니다.

프로그램의 의미는 논리 시스템의 증명 규칙들로 정의 된됩니다.

MㅏC=>M' 와 MㅏE=>v 를 증명하는 규칙들이 될것 입니다. 이러한 증명이 불가능 한 C와 E는 의미 없는 것이 됩니다.

이름은 메모리 주소가 됩니다.

이름이 하는 역할에 대해서 대해서 살펴보자. 이름은 2가지 의미를 가집니다.

1. 메모리 주소

2. 때로는 메모리 주소에 있는 값

이렇게 이름이 뜻하는 두개의 값을 L-value 와 R-value라고 부릅니다.  

x:=E의 왼쪽과 오른쪽에 대한 정의가 다름을 의미합니다. 왼쪽은 메모리 주소, 오른쪽은 메모리 주소에 보관된 값 입니다.

깊이있게 들어와서 변수가 뜻하는 의미가 모호해 지는 것이 싫다면, 두가지를 다르게 표현 하는 방법도 있습니다.

메모리 주소의 값을  뜻할때 이름 앞에 !를 표시 하는 것으로 합시다. 그러면 다음과 같아집니다.

x:=x+1 은 x:=!x+1 과 같이 사용되게 됩니다. x+y+1 대신 !x+!y+1 로 사용해야 합니다.

이름은 기계중심의 언어에서는 변수(variable)이라고 부릅니다.

프로그래머가 메모리 주소에 이름을 짓기 시작하면서 문제가 생깁니다. 

같은 이름을 다른 용도로 사용 하고 싶을때, 같은 이름을 다른 메모리 주소를 위해 재사용 하고 싶을때 , 프로그램이 커지다 보면 이런 경우들이 발생하게 됩니다.

항상 다른 이름을 사용해야 한다면, 프로그래머의 불편은 클 것입니다.

우리가 서두에서 정의한 언어는 같은 이름을 다른 메모리 주소로 사용할 수 없습니다. 때문에 매번 다른 이름을 사용해야 합니다.

이를 해결하기 위한 방안은 이미 있습니다. 수학이나 모든 엄밀한 논술에서 사용하는 방안입니다. 이름의 유효범위를 정하는 것입니다.

유효범위가 겹치지 않는다면, 같은 이름을 다른 메모리 주소로 사용할 수 있습니다. 

그 유효범위는 어떻게 표시 할것인가? 수학에서 사용하는 방식을 빌려옵니다.(이 방식은 수학에서 이미 지난 2000년간 사용해온 믿을만한 방식입니다.)

프로그램의 텍스트의 범위로 이름의 유효 범위를 결정하는 것입니다.

x라는 이름은 새로운 메모리 주소이고 이는 명령문 C 안에서만 유효합니다. let 구문에 의한 유효범위가 일부만 겹치는 경우는 없습니다.  포함되거나 별개이거나...

같은 이름으로 다른 것을 지칭 할 수 있도록 하기 위해서는 위와 같은 규칙을 정확히 드러내야 합니다. 

환경(Environment)

환경이라는 것을 가지고 의미구조를 정확히 정의 할 수 있습니다.

환경은 이름의 실체를 정의한 함수입니다. 

- 환경(시그마)은 이름들에서 주소들로 가는 유한한 함수 입니다.

- 메모리는 주소들에 값들을 대응시키는 유한한 함수입니다.

- 주소는 더이상 프로그램에 나타나는 이름이 될 수 없습니다. (주소는 다른 집합이 될것입니다.)

설탕 구조 - 패스

프로시져(Procedure)

메모리 주소 뿐아니라 명령문에도 이름을 붙일 수 있도록 하자.!!!! 명령문을 반복적으로 사용하지 않고 이름 만으로 그 명령문을 수행 할 수 있도록,...

  let f(x) = C in C'

1. 프로시져 이름 은 f, 인자 이름은 x, f는 명령문 C의 이름 입니다.

2. x는 프로시져가 사용될 때의 인자값을 보관하는 메모리 주소의 이름입니다.

     x의  유효 범위는 C 입니다.

3. f의 유효범위는 C'. 재귀호출이 가능한 프로시져를 위해서는 f의 유효범위는 C' 뿐 아니라 C까지 포함되어야 합니다.

4. f(E) 는 f로 이름붙은 명령문을 실행합니다.

   그런데 E 값을 인자로 사용하라는 것인데, 의미를 정확히 해보자면, 

   우선 환경을 확장할 필요가 있습니다. 

동적으로 결정되는 이름의 유효범위(Dynamic scope)

정의 :Procedure = Id x Command

(이렇게 해보자)

두 집합 A, B가 있을 때 AxB는 두집합의 원소들으 쌍으로 구성된 집합입니다.

- 프로시져가 선언되면 프로시져 이름의 실체는 해당 명령문과 인자 이름이 됩니다.

- 프로시져 호출이 일어나면, 인자에 대해서는 let 명령문 같은 일이 벌어집니다. 

  새로운 메모리 주소를 프로시져 인자 이름으로 명명하고 그 주소에 인자로 전달할 값을 저장 하고, 프로시져 이름이 지칭하는 명령문을 실행합니다.

- 프로시져 이름이 지칭하는 명령문을 프로시져 몸통이라고 합니다.

아래의 프로그램 실행을 생각해보자.

let x:=10 in

    inc(5);--> 10+5

    inc(6); --> 15+6

    let x:=3 in 

       inc(1)

--- 재귀호출 이죠.

프로시져 호출 inc(1) 의 실행중에 몸통 명령문인 x:=x+n 에 나타나는 x는 무엇이 될까요? 처음 선언된 x? 아니면 두번째 선언된 x ?

위의 의미로는 두번째 선언된 x입니다.

이것이 이상한가요? 다음 C와 문법이 똑 같은 Dynamic scope 으로 동작하는 언어를 생각해봅시다.( 익숙한 것이 이해하기 편하니까요.)

이렇게 X가 procedure 가 선언 된 시점에 결정 된 것이 아니라, 호출 되는 시점에 결정되는 구조는 프로그램이 실행중에 동작이 바뀐다는 의미가 됩니다. 어려운 프로그램이 되겠죠.

정적으로 결정되는 유효 범위( static scope)

이름의 실체는 실행전에 정의 되어야 하지 않을까요?

프로시저 안에서 어떤 수식을 계산하기 위한 변수들은 프로시저를 정의 하는 시점에 이미 결정되어야 쉬워집니다. 적어도 동적으로 결정되는 것 보다는 말이죠.

이런 방식이 프로그램을 이해하기에 간단하고 쉽습니다. 그리고 이런 방식이 위에서 언급한 2000년간 사용해온 규칙이기도 합니다.

이렇게 되면 프로시져 정의와 호출의 의미가 아래와 같이 정의 됩니다.

프로시져 호출 방법

지금까지 방식은 값 전달 방식(Call by value)이었습니다.

그런데 이름이 뜻하는 메모리 주소를 전달해 줄 방법이 있었으면 한다. 그러기 위해서는 프로시져 호출문의 생김새부터 구분해주자.

주소를 전달해줄 call-by-reference 의 정의는 다음과 같습니다.

이렇게 되면, 다른 이름이 같은 메모리 주소를 지칭할 수 있게 됩니다.. 같은 대상을 지칭하는 다른 두개의 이름들이 생기게됩니다.( 별명:alias)

생각해 볼 문제는..

별명이 많아지면 프로그램을 이해하기가 어려워지지 않을까? 이런 별명들이 프로시져 호출에 의해서 실행중에 만들어진다면, 이런 다이나미즘, 혼돈스럽지 않을까?

이런 복잡한 상황을 지원하는 언어는 바람직한가?

명령문과 식의 통합

프로시져 호출은 명령문이었습니다.( 지금까지 정의한 언어로는 그렇다) 

메모리에 반을을 일으키는 프로시져 호출의 결과로 값이 계산되게 하고 싶으면?, 메모리를 변화시킨후에 최종적으로 어느 값을 결과로 내놓는 식이 있으면 어떤가? 

C에서는 return E 같은 명령문이 이 역할을 합니다. 

그런데 생각해보면, 명령문과 식, 두가지는 과연 다른가요? 

1. 메모리에 값을 쓸수 있는 것과 메모리를 읽기만 하는것. 

2. 결과 값이 없는 것과 결과 값이 있는것. 

3. 식의 실행결과는 항상 어떤 값이 된다.

4. 그리고 식은 메모리 변화를 일으킬 수 도 있다.

하나로 합칠 수 있습니다.

식

프로그램

프로그래머는 더욱 간단한 언어를 가지고 더욱 자유롭게 프로그래밍을 하게 될 것입니다. 명령문의 개념이 없어지고 모든 것이 식이 되기 때문입니다.

명령문 과 식 두가지 다른 타입의 프로그램 부품을 운용할 필요가 없습니다.

의미 정의는

을 증명하는 규칙들로 통일 됩니다.    명령문 들은 의미없는 빈 값 "." 을 계산한다고 하면,

와 같습니다.

다음 >> 기계중심의 언어 - 메모리 관리와 타입 시스템.

모양과 뜻

프로그래밍 언어는  문법구조(syntax)와 의미구조(semantics)로 구성되어있습니다.  문법구조는 언어의 겉 모양이고 의미구조는 언어의 속뜻을 의미합니다.

이 두가지를 정의하지 못하면 언어라고 볼수 없고, 이 두가지를 알지 못하면 언어를 사용할 수 없습니다.

제대로 생긴 프로그램을 어떻게 만들고 그 프로그램의 의미가 무엇인지에 대한 정의가 없이는 언어를 구현할 수 도 없고 사용할 수 도 없습니다. 

또, 그 정의들은 애매하지 않고 혼동이 없어야 합니다.

문법구조

문법구조는 프로그래밍 언어로 프로그램을 구성하는 방법입니다. 제대로 생긴 프로그매들의 집합을 만드는 방법으로, 귀납적으로 규칙을 정의합니다.

이 귀납적인 규칙으로 만들어지는 프로그램은 나무(TREE)구조를 갖춘 2차원의 모습입니다.

(여기서 나무라고 표현 했는데, 자료구조의 Tree라고 생각하시면 됩니다. 

책에 나무 라고 용어를 풀어서 사용하고 있는데, 아무래도 실제 프로그래밍에서 좀 멀어져서 바라보고자 하는 의도가 있다고 보여집니다. 

이 글에서 설명하고자 하는 내용들을 실제로 programming 언어의 특정 알고리즘 차원에서 바라보지 말고 좀 떨어져서 바라보는 것도 나름 의미가 있습니다.)

정수식을 만드는 귀납규칙을 생각해봅시다.

1. 임의의 정수는 정수식이라고 한다.

2.두개의 정수식을 가지고  + 를 이용해 정수식을 만들수 있다고한다.

3. 하나의 정수식을 가지고 -를 이용해 정수식을 만들수 있다.

이와 같은 형식으로 간단한 명령형 언어를 생각해봅시다.

0. E는 위에서 정의한 정수식이라고 하자.

1. skip 만 있는 명령문은 그것만 말단으로 가지고 있는 그것만 말단으로 가지고 있는 나무가 된다.

2. 정수식을 오른쪽에, 하나의 변수를 왼쪽에,  루트는 := 임을 표시하는 나무가 된다.

3. 세계의 나무를 하부나무로 가지고 있고 루트노드에는 "if"문 임을 표시하고 있는 나무가 된다.

4. 두개의 명령어 나무를 하부나무로 가지고 있고 루트 노드에는 순차적인 명령문임을 표시하는 ";" 나무가 된다.

위 규칙들은 읽는 사람을 돕기 위해 필요 이상의 정보가 들어있습니다.

if 와 then, else 이런 단어들이죠. 또 명령어의 순서 역시 마찬가지죠.

이를 필요한 정보만 가지도록 간략화 한다면,  

이와 같이 각 규칙마다 간단한 symbol만 있으면 그만이다, then else 같은 장식이 필요 없어집니다.

아니면, 우리가 각 규칙을 구분할 수 있다면, 심볼 조차도 생략할 수 있게 됩니다.

사실, 이렇게 심볼까지 생략해가면서 간소화 시킬 필요는 없지요. 프로그래밍 언어의 사용자는 사람이기 때문에 사람이 이해하는데 도움이 되는 수준으로 규칙을 만들 필요가 있습니다.

그래야 문법 규칙들을 보고 만드는 방법에 대한 힌트가 될 수 있기 때문이죠.

요약된 문법 구조와 구체적인 문법구조

(abstract syntax and concrete syntax)

지금까지 봐온 규칙들은 요약된 문법 규칙이라고도 합니다. 프로그램을 만들때 사용하는 문법은 지금까지 보아온 귀납적인 방법이면 충분합니다. 결과물은 나무구조를 가진 2차원의 구조물이죠.

그러나, 프로그램을 읽을 때의 문법은 더 복잡해집니다.  만들어진 프로그램을 표현할때는 나무를 그리지 않고 일차원적인 글로 표현하게 되고, 쓰거나 말하는 사람의 머리에 그려져 있었을 2차원의 나무구조를 복원시키는 규칙들이 되기 때문입니다.

즉,요약된 문법구조와 구체적인 문법구조의 차이를 표현하자면 , 프로그램을 만들때 사용하는 규칙이냐, 읽을때 사용하는 규칙이냐 하는 차이로 보시면 됩니다.

그렇다면 구체적인 문법은 얼마나 구체적일까?

다음의 정수식을 살펴봅시다.

-1+2

위 정수식은 다음 두개의 나무구조중 하나를 일차원으로 펼친 것입니다.

      <<-1>+2>      -<1+2>

어느것인가? 프로그램 "-1+2"를 둘 중 어느것으로 복구 시킬 것인가?

이 요약된 문법으로는 어느 구조로 복구 시켜야 할 지 알 수가 없습니다.

정수 문법식이 다음과 같다면 어떨까요?

이 규칙을 좀 설명하면,

음의 부호가 앞에 붙은 정수식인 경우는 2가지 밖에 없습니다.

1. 말단 자연수

2. 괄호가 붙은 정수식

구체적인 문법구조는 혼동없이 2차원의 프로그램 구조물을 복구하는데 사용되는데, 이 문법은 프로그램 복원 또는 프로그램의 문법검증이라는 과정의 설계도가 됩니다.(parsing)

의미구조 

문법구조로 1+2를 쓰는 방법을 앞에서 봤다면 1+2가 무엇을 뜻하는가에 대해서 살펴볼 때가 되었습니다.

1+2가 뜻하는 것을 2가지로 분류해서 볼수 있는데요.

1. 결과값 3을 뜻한다.

2. 1과 2를 더해서 결과를 계산하는 과정을 뜻한다.

결과값 3을 의미하는 스타일은 뜻하는 바 궁극을 수학적인 구조물의 원소로 정의해 가는 스타일 "궁극을 드러내는 의미구조( denotational semantics)"라고 합니다.

반면, 프로그램의 계산 과정을 정의함으로서 프로그램의 의미를 정의해 가는 스타일 " 과정을 드러내는 의미구조(operational semantics)" 라고 합니다.

이를 C 언어로 이를 표현해보자면, 아래와 같은 코드일것입니다.

그런데 새로운 언어인 ZX 라는 언어가 있다고 합시다. 이 언어의 표현 형식이 operational semantics만 지원한다고 한다면, 아래와 같은 동작으로 이어질 것입니다.

프로그래밍 언어들은 denotational semantics 와 operational semantics 를 모두 다 제공하고  있고 적절한 상황에서 사용 할 수 있도록 설계되어있습니다.

과정을 드러내는 의미구조(operational semantics)는 어느정도 수준으로 표현해야 할까요?

아주 low 하게 CPU에 전달되는 전기적 신호를 일일이 표시해야 할까요? 아니면 , 1이 1을 계산하고 2가 2를 계산하고 +가 1+2=3이라는 등식을 적용하는 것으로 표현해야 할까요?

아니면 실행되는 과정을 , 프로그램과 그 계산 결과를 결론으로 하는 논리적인 증명 과정이라고 표현해야 할까요?

의미구조를 정의하는 목표에 맞추어 그 디테일의 정도를 정하게 됩니다. 대개는 상위의 수준, 가상의 기계에서 실행되는 모습이거나, 기계적인 논리 시스템의 증멍으로 정의하게 됩니다.

과정을 드러내는 의미구조도 denotaional semantics 처럼 충분히 엄밀합니다.

1. 조립식이 아닐 수 있다: 프로그램의 의미가 그 프로그램의 부품들의 의미로만 구성되는 것은 아니다.

2. 하지만 귀납적이다 : 어느 프로그램의 의미를 구성하는 부품들은 귀납적으로 정의된다. 이 귀납이 프로그매의 구조만을 따라 돌기도 하지만, 프로그램 이외의 것을 따라 되돌기도 한다.

(이 문장들의 의미는 잘 이해 못했습니다.)

프로그램의 실행이 진행되는 과정을 큰 보폭으로 그려보자.  <<big-step semantics>>

명령문 C와 정수식 E에 대해서 각각 아래와 같이 정의합니다.

1. 명령문 C가 메모리 M의 상태에서 실행이 되고 결과의 메모리는 M'이다.

2. 정수식 E는 메모리 M의 상태에서 정수값 v를 계산한다.

이에 대한 모든 규칙을 쓰면 이렇습니다.

이 규칙들은 논리 시스템의 증명 규칙이라고 이해해도 됩니다. 명령 프로그램 C의 의미는 임의의 메모리 M 과 M'에 대해서 MㅏC => M' 를 증명할 수 있으면 그 의미가 그 의미가 됩니다.

대개는 M이 비어있는 메모리일때 C를 실행시키는 과정을 나타내고 싶으므로, 0ㅏC=>M' 의 증명이 가능하면 C의 의미가 됩니다.

그것이 증명 불가능 하면 C의 의미는 없는 것입니다.

명령문 C : x:=1 ; y:=x+1; 

는  다음과 같은 증명으로 표현된다.

이렇게 의미구조를 정의하는 방법을 자연스런, 구조적인, 혹은 관계형 의미구조라고 부릅니다.

natural semantics, structural operational semantics , relational semantics

1. 자연스런 : 추론규칙 꼴로 구성되어있고, 자연스런 추론 규칙(natural deduction rules)이라는 규칙때문에 이런 이름이 붙었다고 합니다.

2. 구조적: 계산 과정을 드러내는 의미구조 방식은 이전의 방식 보다 더욱 짜임새가 있었기 때문입니다.

 -   이전의 방식은 가상의 기계를 정의하고 프로그램이 그 기계에서 어떻게 실행되는지를 정의합니다. 이러다 보니, 기계의 실행과정중에 프로그램이 부자연스럽게 조각나면서 기계 상태를 표현하는 데 동원되기도 하고, 프로그램의 의미를 과도하게 낮은 수준의 실행과정으로 세세하게 표현하게 됩니다.

이런 방식을 구현을 통해서 정의하기(definition by implementation) , 어떻게 구현하는지 보임으로서 무엇인지 정의하기 라고 합니다.

프로그램의 구조마다 추론 규칙이 정의되고, 계산과정은 그 추론규칙들을 결합하여 하나의 증명이 되는 것입니다. 

- 의미규칙들이 한 집합을 귀납적으로 정의하는 방식이고 , 그 귀납이 프로그램이나 의미장치들의 구조를 따라 흐르기 때문입니다.

프로그램의 실행을 작은 보폭으로 정의해보자 <<small-step semantics>>

이 과정을 변이과정 의미구조(transition semantics) 라고도 합니다.

이 과정에서는 문법적인 부분들과 의미적인 부분들이 한데 섞이고 있습니다.

전통적으로는 것 모양을 구성하는 것과 속 뜻을 구성하는 것은 반드시 다른세계에 멀찌감치 떨어져  있어야 하지만, (Tarski :수학자가 시작한 전통)

문제될 것 또한 없습니다.

프로그램 이외의 의미장치 없이 프로그매만을 가지고도 변이과정 의미구조를 정의 할 수 있습니다.

예를 들어 메모리를 뜻하는 M이라는 프로그램이외의 의미장치 없이, 1+2+3 을 다시 쓰면 3+3 다시쓰면 6 으로 프로그램 이외의 다른 장치가 사용되지 않습니다.

위의 1+2+3 을 3+3으로 다시 6으로 다시 써 가는 과정이 프로그램의 실행과정과 같습니다.

이 경우 어느 부분을 다시 써야 하는가?, 다시 써야 할 부분을 무엇으로 다시 써야 하는가 ? 하는 것에 대한 정의가 필요합니다.

어느 부분을 다시 쓸것인가 하는 것은 실행 문맥(evaluation context)에 의해서 정의됩니다.

실행 문맥의 정의에 따라서 프로그램을 구성하다 보면, 다시 써야할 부분이 결정됩니다. 그 정의가 문법적으로 가능합니다.

실행 문맥을 가지고 있는 프로그램 K를 정의합니다.

K 안에는 [] 딱 하나가 있습니다. 그 곳이 프로그램에서 다시 써야할 부분, 먼저 실행되어야 할 부분이 됩니다.

이런 특징을 강조하기 위해서 "K[]" 라 쓰고, 그 빈칸에 들어있는 프로그램 부분 C까지 드러내어 "K[C]" 라고 표현합니다.

이 형식은 아래와 같은데요.

1. 지정문, 대입 처리에서 실행되어야 할 부분은 K는 오른쪽 식이고 x:=K 

2. 순차적 처리 구문 에서 명령문이 다음에 실행되어야 할 부분이라면, 앞의 명령문은 시행이 이미 끝났을 때 만이고, done; K 

3. 덧셈 식에서 오른쪽 식이 다음에 실행되어야 할 부분 이라면, 왼쪽 식의 결과는 나와 있어야 한다. v+K

위의 문법적인 표현을 다시쓰기 규칙을 정의하면, 아래와 같습니다.

그릭 속에서 어떻게 다시쓰이는가 하면, 즉,위의 규칙이 어떻게 동작하는지 보면,

x:=1 ; y:=x+1

의 의미를 위의 문맥구조로 풀어보면,

1       ) 

2) 

3  ) 

4 )

5)   

이러한 과정으로 풀이된다.

C : 명령문

M: 메모리

K: 실행 문맥

가상의 기계를 통해서

프로그램의 의미는 어떤 가상의 기계(virtual machine)가 정의되어있고 그 프로그램이 그 기계에서 실행되는 과정으로 나타나게 됩니다.

기계에서 실행되는 과정은 기계상태가 매 스탭마다 변화되는 과정이 됩니다.

예를 들면, 정수식의 의미가 한 게계의 실행과정으로 다음과 같이 정의됩니다.

변수가 없는 정수식만을 생각해보면,

이는 소위 말하는 "스택머신 (stack machine)" 입니다. 이 기계는  스택 S 와 명령어  C 로 구성되어있습니다.

스택은 정수들로 차곡 차곡 쌓여있습니다.

명령어들은 정수식이나 그 조각 들이 쌓여있습니다.

기계 동작 과정의 한 스텝은 다음과 같이 정의됩니다.

<S,n.C>\quad\rightarrow\quad<n.S,C>\\

<S,E_1+E_2.C>\quad\rightarrow\quad<n.E_1\cdot E_2,+,C>\\

<n_2.n_1.S,+.C>\quad\rightarrow\quad<n.S> \quad\quad(n=n_1+n_2)\\

<n.S,-.C>\quad\rightarrow\quad<-n.S,C>

정수식 E의 의미는 <e,E> --> .... 입니다.

정수식이 아닌 우리가 프로그래밍에서 사용하는 command 형식으로 다시 정의해보면 아래와 같습니다.

그리고 , 기계 작동과정도 다음과 같이 정의 됩니다.

<S,push n.C> --> <n.S,C>

<n.S,pop.C>  --> <S,C>

<n1.n2.S,add.C>  --> <n.S,C>   (n = n1+n2)

<n.S,rev.C> --> <-n.S,C>

그리고 스택 머신 안에서 정수식들은 다음과 같은 변환됩니다.

[[n]] = push n

[[E1+E2]] = [[E1]].[[E2]].add

[[-E]] =  [[E]].rev

이러한 기계의 과정이 매우 임의적이라 생각될수 있습니다. 가상의 기계를 어떻게 디자인 하는가? 그 기계의 디테일은 어느 레벨에서 정의해야 하는가? 

그 대답은 프로그램의 의미를 정의하는 목적, 그에 따라 결정될 것이다.

대개 가상 기계를 사용해서 프로그램의 의미를 정의하는 것은 프로그래밍 언어를 구현하는 단계에서 사용됩니다: 프로그래밍 언어의 번역기나 실행기를 구현할때 말이죠.

프로그래밍 언어의 성질을 굴이하거나 그 언어로 짜여진 프로그램들의 관심있는 성질을 분석할 때에 사용하는 의미구조로 사용되는 예는 드뭅니다.

가상 기계는 대개가 이와 같은 분석에서는 필요하지 않은 디테일을 드러내기 때문입니다.

기계중심의 언어로 빨리 넘어가고 싶기 때문에, 다음 내용들에 대해서는 현재는 생략 합니다. 다음에 기회가 되면 정리하도록 하겠습니다. 

- 궁극을 드러내는 의미 구조 (denotaional semantics)  

- 조립식일 수 있는 이유(의미공간 이론 : domain theory)

- CPO, 연속함수, 최소고정점

다음 >>기계중심의 언어

2. 기본기 

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

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

귀납법 ( inductive definition)

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

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

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

귀납법은, 

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

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

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

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

방법 1

방법 2

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

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

자연수 집합

혹은 

스트링 집합

혹은

리스트

혹은 

정수 트리 

혹은

정수식 들의 집합

자연수 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 은 '논리 승' 이라고 표현하기도 하는데 아래와 같은 참,것짓 테이블을 가집니다.

추론규칙

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

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

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

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

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

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

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

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

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

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

(R5)   (R6)

(R7)    (R8)

(R9)  (R10)

(R11) (R12)

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

문법 구조와 의미 구조 

안전한 혹은 완전한

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

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

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

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

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

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

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

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

다음 >> 모양과 뜻