SNU Programming Languages Lecture Notes Kwangkeun Yi 1 School of Computer Science & Engineering Seoul National University 1 Homepage: cse.snu

Transcription

1 SNU Programming Languages Lecture Notes Kwangkeun Yi 1 School of Computer Science & Engineering Seoul National University 1 Homepage: cse.snu.ac.kr/~kwang

2 2

3 머리말 이노트는컴퓨터프로그래밍언어에대한것입니다. 이분야에서축적된성 과와문제들의해결과정에대한이야기입니다. 학부프로그래밍언어강의용 입니다. 두개의축 이야기의내용은두개의축을따라구성되있습니다. 가로축은프로그래밍언어자체에대한이야기입니다. 세로축은생각하는방식에대한이야기입니다. 프로그래밍언어를공부할때사용하는생각의방식에대한. 이두축을기준으로분포되는좌표들이내용을구성합니다. 염려 바라건데다음의것들은빠뜨리지않고전달하려고합니다 : 오랫동안살아남을기본기, 단단한핵심. 그리고, 모국어로강의한내용입니다. 물론전문용어는항상영어를 italic 글꼴로병기합니다. 그리고내가내스승의언어인라틴어대신에나의언어인프랑스어로쓰 기로한것은, 태어나면서가지고있는순수이성만을사용하는사람들이 옛날책만을믿는사람들보다더바르게내의견을이해하리라고믿고있 기때문이다. 나는양식을가지고꾸준히노력하는사람들만이내심판

4 4 관이되기를바라거니와그런사람들은내가통속의언어로내논거를설 명했다고해서이논거를들으려하지않을만큼라틴어를편애하지는않 을것이라고믿는다. 데카르트, 방법서설 ( 마지막에서두번째단락 )

5 차례 1 장소개 프로그래밍언어는미개하다 프로그래밍언어의위치 장 기본기 귀납법inductive definition 집합의정의 증명의방법 형식논리formal logic 모양과뜻 추론규칙 안전한혹은완전한 장 모양과뜻 문법구조syntax 요약된혹은구체적인 의미구조semantics 과정을드러내는 궁극을드러내는 장기계중심의언어 주어진기계

6 6 차례 4.2 언어키우기 0: K 변수 : 메모리주소에이름붙이기 이름의두가지의미 이름의유효범위 환경 자유로운혹은묶여있는 설탕구조 언어키우기 I: K 프로시져 : 명령문에이름붙이기 이름의유효범위 프로시져호출방법 재귀호출 명령문과식의통합 메모리관리 언어키우기 II: K 레코드 : 구조가있는데이타, 혹은메모리뭉치 포인터 : 메모리주소를데이타로 같은값 메모리관리 언어키우기 III: K 실행되서는않될프로그램들 오류검증의문제 타입시스템 : 소개 K = K- + 타입시스템 K- 타입시스템의논리적문제 K- 타입시스템의구현문제 이름공간, 같은타입 정리

7 차례 7 5 장 값중심의언어 언어의모델 람다계산법Lambda Calculus 람다로프로그램하기 언어키우기 0: M 소극적인실행lazy evaluation과적극적인실행eager evaluation 시작언어 : 값은오직함수 언어키우기 I: M 다른값 : 정수, 참 / 거짓 언어키우기 II: M 구조가있는값 : 쌍pair 언어키우기 III: M 메모리주소값 : 명령형언어의모습 오류검증의문제 정적타입시스템static type system 형식논리시스템formal logic 리뷰 단순타입시스템simple type system 단순타입추론규칙 추론규칙의안전성 추론규칙의구현 안전한그러나경직된 M3로확장하기 다형타입시스템polymorphic type system 다형타입추론규칙 추론규칙의안전성 추론규칙의구현 M3로확장하기 정리

8 8 차례 6 장 번역과실행 프로그램입력 프로그램실행 실행기interpreter 번역기compiler 자가발전 번역 : 불변성질invariant 유지하기 가상의기계virtual machine

9 1 장 소개 이강의를통해서다음과같은질문들에대한답을익히거나, 좋은답을만들어내기위해서필요한소양을닦게된다. 다양한프로그래밍언어들이품고있는공통된원리들은무엇인가? 현재의프로그래밍언어들은얼마만큼미개한가? 좀더나아지기위해서필요한것들은무엇인가? 새로운프로그래밍환경을효과적으로운용할수있는언어는무엇인가? 이러한질문들에대한답은왜필요한것일까? 고난도소프트웨어시스템을손쉽게다룰수있는방법은프로그래밍언어의내용을공부하면서효과적으로익혀진다. 소프트웨어방법론중에는프로그래밍언어이론의뒷받침이없이는공허해지는것이대부분이기때문이다. 대부분의소프트웨어들이컴퓨터언어를처리하는부품을가지게되는데, 이부품들이프로그래밍언어에서축적한이론과실제를올바로이해하고설계될필요가있다. 성급한상식의수준에서고안되는프로그래밍언어시스템은어느순간무너져버리는다리와같이위태로울수밖에없기때문이다. 프로그래밍언어의연구성과들덕택에소프트웨어개발이라는것이급

10 10 소개 속도로수학적이고엄밀한기술이되어가고있는데, 이에우리가프로그 래밍언어를어떻게해야할것인지를고민해야한다. 우리소프트웨어 산업의경쟁력을창출할근간으로써. 프로그래밍언어의성과, 문제, 그리고그생각의틀을이해하는것이컴퓨터 과학 / 공학 computer science, computer engineering 을전공하는데중요한밑거름이다. 1.1 프로그래밍언어는미개하다 현재의프로그래밍언어는얼마나미개할까? 프로그래밍언어로짜여진소프트웨어를기계가실행해준다. 우리가고안한기계가소프트웨어를자동으로실행해준다. 대단하고놀라운일이다. 더놀라운일은, 하나의기계가실행할수있는프로그램들이무수히많이있을수있다는것이다. 이런기계는이세상에없었다. 자동차라는기계는 가고서는 프로그램만실행해줄뿐이다. 자동차페달을밟아서문서를편집하거나동영상을상영하거나에어백을통제하는등의일을할수는없다. 그런데, 문제는프로그래밍언어로짜여진소프트웨어라는인공물이매우위태로운상태에서실행된다는점이다. 제대로작동하는물건인지를확인하지않고실행되게된다. 그확인을미리자동으로해주는기술이아직은미개하다. 다른분야와비교해보자. 제대로작동할지를미리검증할수없는기계설계는없다. 제대로서있을지를미리검증할수없는건축설계는없다. 인공물들이자연세계에서문제없이작동할지를미리엄밀하게분석하는수학적기술들은잘발달해왔다. 뉴튼역학, 미적분방정식, 통계역학등등이그러한기술들일것이다. 소프트웨어라는인공물에대해서는어떠한가? 작성한소프트웨어가제대로실행될지를미리엄밀하게확인해주는기술들은있는가? 이문제는아직도해결되지않은문제이다. 이문제에대한답을프로그래밍언어에서도해줘야한다. 이방향에서지금까지연구된것들이아직은미

11 1.2 프로그래밍언어의위치 11 흡하다. 지금까지성공적인연구결과가어떤모습으로프로그래밍언어에장착되고있는지이강의를통해살펴볼것이다. 그렇게얻어진시각으로소프트웨어기술의현재수준을간파하고, 보다나은미래기술을열어갈씨앗을품게되길. 1.2 프로그래밍언어의위치 우선프로그래밍언어는무엇인가? 에대해서다양하게이야기될수있다. 컴퓨터라는기계에게명령하는도구, 프로그래머들사이의소통의수단, 상위레벨의디자인을표현하는도구, 알고리즘을기술하는표기법, 생각한바를실행시킬수있도록표현하는도구, 등등.

12 12 소개 여담으로오해하나를바로잡자. 프로그래밍언어가컴퓨터를돌리기위해만들어진것이아니다. 컴퓨터가프로그램을돌리기위해만들어진것이다. 역사적으로그렇다. 만들어진컴퓨터를사용하기위해고안한것이프로그래밍언어가아니고, 그전에이미논리학자와수학자들이프로그래밍언어를고안했다. 그리고나서전기회로로구현된디지탈컴퓨터가발명되었다. 1930년대말부터, 일군의수학자들은과연 기계적으로계산가능한함수 가무엇일까를고민했다. 하나의아이디어로, 언어를하나고안해서그언어로정의될수있는것들을기계적으로계산가능한함수라고하자, 고제안하였다. 정확하게현재의디지탈컴퓨터로실행될수있는모든프로그램을작성할수있는언어들이었다. 놀랍게도. 지금의디지탈컴퓨터는그러한함수들을자동으로빨리실행시켜주는도구일뿐이다. 실행해주는기계가뭐가되었든지간에, 프로그래밍언어란자동실행을염두 에두고고안한언어이다. 그레벨이기계어수준이건그보다훨씬상위의언

13 1.2 프로그래밍언어의위치 13 어이건간에. 프로그래밍언어의효용을조금구체적으로보자. 다음그림에서표현하였듯이, 모든소프트웨어시스템은 언어 를기반으로한다. 소프트웨어가외부세계와소통하는데는, 어떤형태든항상언어를통해서이루어지기때문이다. 데이타베이스시스템의질의처리query processing, 로봇프로그래밍, 하드웨어디자인, 커뮤니케이션프로토콜디자인, 소프트웨어검증, 프로그래밍언어시스템 ( 번역기compiler나실행기interpreter), 게임프로그래밍등등 언어 없이작동하는소프트웨어시스템은없다. 모든것들은언어처리시스템을품고있다. 따라서모든소프트웨어시스템의경쟁력의일부분은프로그래밍언어분야의연구성과에기초해서발전하게된다. 프로그래밍언어의첨단기술에대한이해가없이는로봇프로그래밍시스템 / 하드웨어칩디자인시스템 / 프로토콜디자인시스템 / 소프트웨어검증시스템 / 게임프로그래밍시스템 / 데이타

14 14 소개 베이스시스템등을제대로디자인하거나구현하기가어렵다. 모두프로그래밍언어분야의 축복 을지렛대로삼아발전할수있다. 그리고, 프로그래밍언어분야자체는또, 논리학과수학의축복아래에서만단단하게발전할수있다.

15 2 장 기본기 프로그래밍언어를이야기하는데기본적으로사용하는어휘들과말하는방식 이있다. 그어휘와방식의기본은수학이다. 이장에서는앞으로우리가사 용할어휘와말하는방식을알아보고, 그사용예들을살펴보자. 2.1 귀납법 inductive definition 집합의정의 집합을정의하는방법에는조건제시법과원소나열법, 그리고하나가더있다. 귀납법이다. 귀납법은즐겁다. 유한하게무한한것을정의할수있기때문이다. 유한한개수의유한한규칙들로무한히많은원소를가지는집합을정의하는방법이귀납법이다. 귀납법은대게증명의한방법이라고배우지만, 사실그증명이수긍이가는이유는집합을정의하는귀납법의얼개를따라서증명해나가는것이기때문이다. 귀납증명에대해서는다음장 (2.1.2) 에서살펴보기로하고귀납이집합을정의하는데사용되는것에대해서우선살펴보자. 귀납법으로집합을정의하는방법은, 그이름이의미하는데로, 되돌아서바

16 16 기본기 치는것이다 ( 되돌아서 return 歸, 바치다 dedicate 納 ). 되돌아서만들어바친다는것은, 그집합의원소를가지고그집합의원소를만든다는것이다. 귀납법으로정의되는집합은몇개의규칙들로구성되고, 그규칙들이귀납적이다 : 무엇무엇이이미집합의원소들이라면그것들로어떻게어떻게하면다시집합의원소가된다, 는식이다 그집합은이것이다조금일반적인톤으로이야기해보면이렇다. 하나의규칙은짝으로구성된다 : 가정들 X와결론 x. 그규칙이말하는바는 X에있는것들이정의하려는집합에모두있으면, x도있어야한다 는것이다. 이러한규칙들이모여서하나의집합을정의한다. 그집합은, 규칙들이요구하는원소들은모조리포함하고있는집합가운데가장작은집합으로한다. 최소의집합이라고고집하는이유는, 규칙들이요구하는원소들은모두포함하지만그밖의것들은제외하고싶어서이다. 좀더명확하게가보자. 가정들 X와결론 x의짝 (X, x) 로표현되는규칙들의모임을 Φ라고하자. 그규칙을만족하는원소들을모두품고있는집합을 Φ에대해서닫혀있다 혹은, Φ-닫힘 이라고한다. 즉, 집합 A가 Φ-닫힘, 은 (X, x) Φ 이고 X A 이면 x A 인경우를말한다. 이제, Φ 가정의하는집합은모든 Φ- 닫힌집합들의교집합 으로정의된다 : {A A 는 Φ- 닫힘 }. 그러한집합은 Φ- 닫힌집합이면서가장작다. ( 왜?) Example 1 자연수의집합은다음두개의규칙들로정의된다 : (, 0) ({n}, n + 1)

17 2.1 귀납법 inductive definition 17 즉, 0 은자연수이고, n 이자연수라면 n + 1 도자연수이다. 이규칙들에대해서 닫혀있는집합들은우리가알고있는자연수의집합 N 뿐아니라유리수의집 합 Q 도있다. 하지만가장작은그러한집합은 N 이다. Example 2 영문소문자알파벳으로만들어지는스트링의집합은다음의규칙들로정의된다 : (, ɛ) ({α}, xα for x {a,, z}) 즉, ɛ은스트링이고, s가스트링이라면그앞에영문소문자를하나붙여도스트링이다. 이규칙들에대해서닫혀있는가장작은집합이이규칙들이정의하는 스트링 이라는집합이다 표기법 귀납법의규칙을나타내는편리한표기로프로그래밍언어에서는다음두가 지것을주로쓴다. 위의자연수집합은 : n 0 n + 1 혹은 이고, 위의스트링집합은 : 0 n n + 1 α ɛ xα (x {a,, z}) 혹은 ɛ α xα x {a,, z} 으로표현한다. 그리고, 귀납규칙들은반드시되돌아서표현될필요는없다. 집합이유한하다면재귀가필요없이원소나열법과같이주욱쓰면된다. 예를들어, 집합

18 18 기본기 {1, 2, 3} 을규칙들로표현하면 (, 1) (, 2) (, 3) 혹은 혹은 x 가된다. 다음그림은자연수집합, 두갈래나무 binary tree 집합, 리스트집합, 사과와 배만가지는집합을귀납적으로정의한것이다.

19 2.1 귀납법 inductive definition 19 Example 3 리스트의집합도다음두개의규칙들로정의된다 : nil l l 혹은 l nil l 즉, nil 은리스트이고, l 이리스트라면그앞에하나의노드를붙인 l 도리 스트이다. 이규칙들에대해서닫혀있는가장작은집합이이규칙들이정의 하는 리스트 라는집합이다. Example 4 말단에정수를가지는두갈래나무 binary tree 들의집합은다음네 개의규칙들로정의된다 : n n Z t N(t, nil) t N(nil, t) t 1 t 2 N(t 1, t 2 ) 혹은 t n (n Z) N(t, nil) N(nil, t) N(t, t) 즉, 임의의정수 n은두갈래나무이고, t가두갈래나무라면그것을왼편이나오른편에매단것도두갈래나무이고, 두개의두갈래나무를각각왼편과오른편에매단것도두갈래나무이다. 이규칙들에대해서닫혀있는가장작은집합이이규칙들이정의하는 두갈래나무 라는집합이다. Example 5 그래프 graph 는노드들과두노드를연결하는선들로이루어진구

20 20 기본기 조물이다. 그래프들의집합도다음세개의규납규칙들로정의된다 : G G G G 혹은 G a node G adding a node G adding an edge 위에서 G 은그래프 G 에있는노드를선 edge 으로연결하는것을뜻한다. Example 6 정수식들의집합은다음의규칙들로정의된다 : n n N e e e 1 e 2 e 1 +e 2 e 1 e 2 e 1 e 2 혹은 e n (n N) e e + e e e 즉, 자연수 n은정수식이고, e가정수식이라면그앞에음의부호를붙여도정수식이고, 두개의정수식사이에덧셈부호나곱셈부호를끼워넣어도정수식이다. 이규칙들에대해서닫혀있는가장작은집합이이규칙들이정의하는 정수식 이라는집합이다. Example 7 다음의규칙들이만들어내는 A, a 쌍들의집합은무엇일까? A, a a A

21 2.1 귀납법 inductive definition 21 A, a A, b A, a b A, a b A, a A {a}, b A, a b A, a b A, a A, b 그집합은이렇게만든다 그런데, 위의정의는명확하지만한가지가의아하다. 규칙들이정의하는집합이무엇인지정의하고있지만, 그집합을만드는방법을알려주고있지않다. (The definition is non-constructive.) 자장면은무엇이다라고정의해놓았지만, 자장면을만드는방법은가르치고있지않다! 만드는방법을알려주는정의는다음과같다. 규칙들의집합 Φ는함수 φ를정의한다. φ는집합을받아서그집합을가지고 Φ 규칙들을이용해서만들어지는모든원소들을내놓는다 : φ(y ) = {x X x Φ, X Y } Φ 규칙들이정의하는집합은함수 φ에의해서닫혀있는집합 (φ가더이상새로운것을만들어내지못하는집합, 즉 φ(x) X인집합 X) 중에서최소의집합 {X φ(x) X} (2.1) 이고, 이것은함수 φ의최소의고정점least fixed point가된다. ( 왜?) 함수 φ의최소의고정점인이집합은빈집합에서부터출발해서 (φ 0 라고하자 ) φ를한번적용하고나온집합 φ 1, 두번적용하고나온집합 φ 2 등을모두모으면만들어진다. 즉, φ 0 = φ n = φ(φ n 1 ) n N

22 22 기본기 라고하고 φ 0 φ 1 φ 2 = i N φ i 런식으로만들어지는것이 Φ 규칙들이정의하는집합이되는것이다. 이렇 게만들어진집합은식 2.1 과일치한다. ( 왜?) Example 8 자연수의집합은다음두개의규칙들로정의된다 : n 0 n + 1 이규칙들이지정하는집합 N 은다음과같이만들어진다 : φ 0 = φ 1 = {0} φ 2 = {0, 1} φ 3 = {0, 1, 2} 들의합집합. Example 9 리스트의집합도다음두개의규칙들로정의된다 : l nil l 이규칙들에정의하는 리스트 라는집합은다음과같이만들어진다 : φ 0 = φ 1 = {nil} φ 2 = {nil, nil} φ 3 = {nil, nil, nil} 들의합집합.

23 2.1 귀납법 inductive definition 23 Example 10 두갈래나무 binary tree 의집합은다음네개의규칙들로정의된다 : t N(t, nil) N(nil, t) N(t, t) 이규칙들이정의하는 두갈래나무 라는집합은다음과같이만들어진다 : φ 0 = φ 1 = { } φ 2 = {, N(, nil), N(nil, ), N(, )} 들의합집합. Example 11 영문소문자알파벳으로만들어지는스트링의집합은다음의규 칙들로정의된다 : α ɛ xα (x {a,, z}) 이규칙들이정의하는집합은 φ 0 = φ 1 = {ɛ} φ 2 = {ɛ, aɛ,, zɛ} 들의합집합이다. Example 12 귀납규칙 Φ에있는모든규칙 X 가 X를공집합으로가진게없 x 다면, Φ가정의하는집합은공집합이된다. 만들어지는시작이제공되지않았기때문이다 : φ 0 = φ 1 = =.

24 24 기본기 원소들의순서 Φ 규칙들로귀납적으로만들어지는집합 i N 의모든원소들은 φ를 i번적용해서만들어진다. 원소들의순서를정의하기를, φ i 번째에새롭게만들어지는원소들의순서를 i라고하자. 원소들마다자기가몇째번에만들어진것이냐에따라순서가있는것이다. i째번에만들어지는원소들 x는 i 1째번에만들어졌던원소들 X 덕택에귀납규칙 (X, x) 에의해서만들어진것이다. i 1째번의원소들은또 i 2째번의원소들덕택에만들어진것이고. 이연쇄반응은결국에는바닥에닿는다 : 궁극에는항상 0째번에만들어진원소들이씨가된다. 이렇게언젠가는바닥을드러내는순서를 기초가튼튼한순서well-founded order 라고한다. 귀납법으로정의한집합은항상기초가튼튼한순서를가지고있다. 이성질이귀납법증명의기술을가능하게해준다.( 장 2.1.2) φ i 우리가다루는귀납규칙규칙들이만드는집합의원소들은규칙들을유한번적용해서만들어지는원소들로생각한다. 또, 애매하지않는규칙들만사용한다. 일반적으로, 한집합을정의하는귀납규칙들은무한히많을수도있고, 애매한경우도있을수있다 ( 두개의다른규칙 (X, x) 와 (X, x) 이같은원소 x에대해서말하는경우 ) 증명의방법 집합 S의모든원소들이어떤성질 P 를만족하는지를증명하려고한다고하자. 즉, x S.P (x) 를증명하려고한다. P (x) 는 x가 P 라는성질을만족한다는뜻이다. 그리고

25 2.1 귀납법 inductive definition 25 그집합 S가귀납적인규칙들 Φ에의해서정의되었다고하자. 따라서, S의원소들사이에는순서가있고 (0째번원소, 1째번원소, ), 그순서는항상 0째번에기초하고있다. i째번원소들이란, Φ 규칙들을 i번적용해서새롭게만들어지는원소들이다. 집합 S는모든 i째번원소들을모두모은집합이므로, S의모든원소에대한증명은모든 i째번에만들어지는원소들에대한증명을하면된다. 0째번에만들어지는원소는없다. 따라서증명할것도없다. 시작은, 1째번에만들어지는원소들에대해서 P 가사실임을증명해야한다. 그리고, 임의의 i 이전번에만들어진원소들에대해서 P 가사실이라는가정하에 ( 귀납가정induction hypothesis라고함 ), i째번에만들어지는원소들이 P 를만족하는지를증명하자. 그러면집합 S 의모든원소들에대해서 P 를만족하는지를증명한것이된다. 왜냐면, 집합 S는모든 i번째만들어지는원소들만으로구성되므로 귀납규칙들에대한것으로이증명기술을귀납규칙들에대한것으로다시이야기하면, 우선, 첫째번에만들어지는원소들은 Φ에있는규칙들중에는공집합을전제로가지고있는규칙들 (, x) 가만드는 x들이다. 고로, 그러한 x들에대해서증명하는것이첫째번의원소들에대한증명이된다. 그다음, 그이상째번에만들어지는원소들은 Φ에있는규칙들중에서공집합이아닌전제 (X ) 를가지고있는규칙들 (X, x) 이만드는 x들이다. x가 i째번에만들어지는원소라면 X에있는원소들은그이전번에만들어진원소들이다. 따라서 X에나타나는원소들에대해서사실이라는가정하에 x에대해서사실인지를증명한다. 이렇게위의두가지를증명하면, 모든 i째번에만들어지는원소들 (Φ가정의하는모든원소들 ) 에대해서증명한것이된다.

26 26 기본기 일반적으로 두개로쪼개지는위와같은증명을하나로이야기하면, 귀납법증명은다음을 증명하면된다 : 모든 i O 에대해서, ( j < i.p (j 째번원소 )) P (i 째번원소 ). 한꺼번에두개가포섭되는이유를따져보면, i가 0일때, j < i 를만족하는 j는없다. 공집합의모든원소들에대해서는임의의사실이성립하므로, j < i.p (j째번원소 ) 는항상성립. 따라서위의식은 true P (0째번원소 ) 와같다. 0 째번원소도없으므로 P (0째번원소 ) 는항상성립. i가 1일때, j < i 를만족하는 j는 0이고 0째번원소는없으므로위의식은 true P (1째번원소 ) 즉 P (1째번원소 ) 가된다. i가 2 이상인임의의 째번 에대해서는특별한것없이, 위의식그대로를증명하면, 귀납가정을안고 ( j < i.p (j째번원소 )) 증명하는것이된다. Example 13 모든자연수 n에대해서, n = n(n + 1)/2인지를증명하자. 모든자연수는귀납규칙 n 0 n + 1를유한번적용해서만들어지는원소들의모임이다. 첫째번에만들어지는원소는 0이다. n이 0일때위의등호가성립하는지증명한다. 그다음은 i 이전번에만들어지는자연수에대해서위의등호가성립한다고가정하고, i째번에만들어지는자연수에대해서사실인지증명한다. i째번에만들어지는자연수를 n + 1이라고하자. 그이전번에만들어진자연수들중에는 n이있다. 그러면, n + (n + 1) = n(n + 1)/2 + (n + 1) = (n + 1)(n + 2)/2 이므로위의등식이성립한다. 귀납규칙들을따라증명하면, 0일때사실인지증명하고, n일때사실이라는가정하에 n + 1일때사실인지증명하면된다.

27 2.1 귀납법 inductive definition 27 Example 14 두갈래가꽉찬나무complete binary tree에대해서, 말단노드의갯수는내부노드의갯수보다항상하나많다는것을증명하자. 두갈래가꽉찬나무 t를만드는귀납규칙은 t N(t, t) 이다. 임의의 t에서 ( 말단노드 ) 의개수 l이 N( 내부노드 ) 의개수 n 더하기 1이다. 인경우는, 그렇다. t 1 과 t 2 의성질이그렇다고하자 : l 1 = n 이고 l 2 = n 그러면, N(t 1, t 2 ) 의말단노드의수는 l 1 + l 2 이고, 내부노드의수는 n 1 + n 2 + 1이다. l 1 + l 2 = (n 1 + n 2 + 1) + 1이성립한다. Example 15 그래프 graph 집합을정의하는두개의귀납규칙이있다. 두규 칙이정의하는두집합은같은집합이라는것을증명하자. G G G H H H H 우선, 임의의 G는 H로볼수있다. G를만드는세가지규칙마다귀납적으로쉽게확인해볼수있다. 거꾸로, 임의의 H도 G로볼수있다. H에대한귀납법으로증명하자. H가 H 1 H 2 일경우이다 : 귀납가정은 H 1 과 H 2 가 G 1 과 G 2 로볼수있다는것이다. 따라서, G 1 G 2 가 G-규칙으로만들수있다는증명을하면된다. G 2 에대한귀납법으로다시파고들수있다. 귀납가정은 G 2 의부품 G 2에대해서 G 1 G 2는 G-규칙으로만들수있다는것이다. G 2 가 일때 : G 1 G 2 = G 1 이고당연히 G-규칙으로만들어진다. G 2 가 G 2 일때 : G 1 G 2 = G 1 (G 2 ) = (G 1 G 2) 이고귀납가정에의해 G 1 G 2는 G-규칙으로만들수있으므로 (G 1 G 2) 도그러하다. G 2 가 G 2 이면 G 1 G 2 = G 1 (G 2 ) = (G 1 G 2) 이고귀납가정에의해 G 1 G 2는 G-규칙으로만들수있으므로 (G 1 G 2) 도그러하다.

28 28 기본기 다른경우는명백하다. 2.2 형식논리 formal logic 형식논리는프로그래밍언어이다. 그언어로짜여진프로그램은참이거나거짓을계산한다. 형식논리에대한이야기는프로그래밍언어에대해서이야기할때만나게될여러개념들을익숙하게해준다. 선언논리propositional logic를중심으로알아보자 모양과뜻 선언논리에서생각하는논리식 f 는다음의귀납법칙으로만들어지는집합의 원소이다. 즉, 논리식 f 는다음의방법으로만들어진다. f T F f f f f f f f 위의귀납법칙이정의하는집합의원소들, 그것들이선언논리라는언어로짜여진프로그램들이다. 선언논리식은위의방법대로만들어지는것만이제대로생긴선언논리식인것이다. 무한히많은선언논리식들은모두위의일곱가지방법을반복적용해서만들어진다. 그럼, 선언논리식의의미는무엇인가? 무한히많은선언논리식들하나하나마다그뜻이무었인지유한하게정의할방법은있는가? 이경우에도귀납법을이용해서의미하는바를정의할수있다. 임의의논리식은 i째번에만들어진다. i째번에만들어지는논리식은그이전번에만들어진논리식을가지고만들어진다. 따라서, i째번이전에만들어진논리식의의미를가지고,

29 2.2 형식논리 formal logic 29 i 째번에만들어진논리식의의미를정의하는방법이면되겠다.( 다른더좋은 방법이있을까?) 논리식 f 의의미를 [f ] 라고표기하자. 첫째번에만들어지는논리식의의미를정의하자. T 는참을뜻하고 F 는 거짓을뜻한다. [T ] = true [F ] = false i 째번논리식 f 의의미는그이전에만들어진 f 의의미를가지고정의 된다. 그의미의부정이된다. [ f ] = not[f ] 마찬가지로, 이전에만들어진 f 1 과 f 2 의의미를가지고, 다른식들의의미 가결정된다. f 1 f 2 의의미는그둘의논리곱이고, f 1 f 2 의의미는그 둘의논리합이고, f 1 f 2 의의미는그둘의논리승이다. [f 1 f 2 ] = [f 1 ] andalso [f 2 ] [f 1 f 2 ] = [f 1 ] orelse [f 2 ] [f 1 f 2 ] = [f 1 ] implies [f 2 ] 이렇게어느논리식의의미가그논리식을구성하는하부논리식의의미로정 의되면임의의논리식의의미가정의되는셈이다. 임의의논리식은기초가되 는 (1 째번 ) 논리식에서부터차곡차곡만들어진것이기때문이다. Example 16 논리식 (T (T F )) F 의의미는, 정의에따라차곡차곡써

30 30 기본기 보면 [(T (T F )) F ] = [T (T F )] implies [F ] = ([T ] andalso [T F ]) implies false = (true andalso ([T ] orelse [F ])) implies false = (true andalso (true orelse false)) implies false = false 이다 추론규칙 선언논리식의의미가정의되었다. 그의미는참이거나거짓이다. 논리식이참인지를판별하는방법은무엇일까? 물론, 논리식의의미를정의한대로따라가다보면결과를알수있다 : 참혹은거짓. 의미의결과를보면논리식이참인지아닌지를판별하면된다. 이것은프로그램을돌려보고그프로그램이참을결과로내는지를판별하는것과같다. 혹시, 프로그램을돌리지않고알아내는방법은없을까? 논리식의의미를계산하지않고, 참인지거짓인지를알수있는방법은없을까? 논리식의모양만을보면서참인지를판별할수는없을까? 이러한판별규칙이가능하지않을까? 그런규칙을증명규칙proof rule 혹은추론규칙inference rule이라고한다. 이규칙들도어떤집합을만들어내는귀납적인규칙들로정의된다. 그규칙들이만들어내는집합은우리가원하는논리식들 ( 참인논리식들 ) 로구성되는집합이다. 예를들어다음과같은증명규칙proof rules/ 추론규칙inference rules들을생각하

31 2.2 형식논리 formal logic 31 자. 귀납규칙들을분수꼴로표현한것이다. (Γ, T ) (Γ, f) f Γ (Γ, F ) (Γ, f) (Γ, f) (Γ, f) (Γ, f 1 ) (Γ, f 2 ) (Γ, f 1 f 2 ) (Γ, f 1 f 2 ) (Γ, f 1 ) (Γ, f 1 ) (Γ, f 1 f 2 ) (Γ, f 1 f 2 ) (Γ {f 1 }, f 3 ) (Γ {f 2 }, f 3 ) (Γ, f 3 ) (Γ {f 1 }, f 2 ) (Γ, f 1 f 2 ) (Γ, f 1 f 2 ) (Γ, f 1 ) (Γ, f 2 ) (Γ {f}, F ) (Γ, f) (Γ, f) (Γ, f) (Γ, F ) (Γ, f) 쌍들의집합을만드는규칙들이다. 특히, Γ 에있는모든논리식들이참 이면 f 는참 인경우에 (Γ, f) 를만들어내는규칙들이다. 대개형식논리에서는, (Γ, f) 를 Γ f 로표기한다. 규칙마다번호를붙 이고다시쓰면 : Γ T (r1) Γ f f Γ (r2) Γ F Γ f (r3) Γ f Γ f (r4) Γ f 1 Γ f 2 Γ f 1 f 2 (r5) Γ f 1 f 2 Γ f 1 (r6) Γ f 1 Γ f 1 f 2 (r7) Γ f 1 f 2 Γ {f 1 } f 3 Γ {f 2 } f 3 Γ f 3 (r8) Γ {f 1 } f 2 Γ f 1 f 2 (r9) Γ f 1 f 2 Γ f 1 Γ f 2 (r10)

32 32 기본기 Γ {f} F Γ f (r11) Γ f Γ f Γ F (r12) 이증명규칙들을 Γ f 들의집합을만드는귀납규칙으로볼뿐아니라, Γ f 의증명을만드는귀납규칙으로도볼수있다. 그래서 증명규칙 이라고 부른다. 예를들어, 증명규칙 Γ f 1 Γ f 2 Γ f 1 f 2 이귀납적으로이야기하는것이두가지다. Γ f 1 와 Γ f 2 가집합에있다면, Γ f 1 f 2 도집합의원소여야한다는것이하나. 그리고, Γ f 1 f 2 의증명 을만드는 ( 귀납적인 ) 방법으로, Γ f 1 와 Γ f 2 의증명이있다면그증명들을 분자에매달고분모에는 Γ f 1 f 2 를놓은것이 Γ f 1 f 2 의증명을만드는 방법이라는것이다. 이렇게만들어지는증명은하나의나무구조가된다. 이나무구조의뿌리 노드는증명의최종결론이다. 나무의갈래구조는사용한증명규칙들이만들 어낸다. 규칙의식들이각각노드가되는데, 분모식노드에서분자식노드들 로가지치는구조가된다. 그분자식들은다시다른규칙의분모가되서그규 칙의분자식들로다시가지치고. 그가지들의최종잎새는증명규칙중에서분 자가없는규칙들의분모식으로끝맺게된다. 예를들어, {p p} p 의증명을위의증명규칙으로만들면아래의나 무구조가된다 : (r2) {p p, p} p (r2) {p p, p} p p {p p, p} p (r2) (r10) {p p, p} p (r12) {p p, p} F {p p} p (r11) 안전한혹은완전한 위의규칙들이만들어내는 f의 f는모두참인가? 반대로, 참인식들은모두위의증명규칙들을통해서 f 꼴로만들어지는가?

33 2.2 형식논리 formal logic 33 첫질문에예라고답할수있으면우리의규칙은안전sound하다고, 믿을만하다고한다. 둘째질문에예라고답할수있으면우리의규칙은완전complete하다고, 빠뜨림이없다고한다. 증명규칙들이안전하기도하고완전하기도하다면, 참인식들만빠짐없이만들어내는규칙이된다. 안전하냐완전하냐는기계적인증명규칙들의성질에대한것이다. 그기계적인규칙들의성질은오직우리가생각하는의미에준해서결정될수있다. 증명규칙이라는기계가만들어내는식들의의미를참조해야만안전한지완전한지를결정할수있다. 신라면을찍어내는기계는맹목적일뿐이다. 그기계가좋은이유는항상인기있는맛좋은신라면을만들어낸다는그기계바깥의의미를참조할때에비로소결정된다. 프로그램에서도그겉모양 ( 문법 ) 과속내용 ( 의미 ) 은대개다른두개의세계로정의되고, 프로그램을관찰하고분석하는모든과정은기계적으로정의된다. 컴퓨터로자동화하기위해. 그기계적인과정들의성질들 ( 과연맞는지, 무엇을하는것인지 ) 등에대한논의는항상그과정의의미나결과물들의의미를참조하면서확인된다.

34 34 기본기

35 3 장 모양과뜻 프로그래밍언어의겉모양은문법구조syntax를말한다. 프로그래밍언어의속뜻은의미구조semantics를말한다. 그두가지를정의하지못하면그언어를정의한것이아니다. 그두가지를알지못하면그언어를사용할수없다. 제대로생긴프로그램을어떻게만들고그프로그램의의미가무엇인지에대한정의가없이는언어를구현할수도없고사용할수도없다. 더군다나그정의들은애매하지않고혼동이없어야한다. 3.1 문법구조 syntax 문법구조syntax는프로그래밍언어로프로그램을구성하는방법이다. 제대로생긴프로그램들의집합을만드는방법이다. 귀납적인규칙으로정의된다. 이귀납적인규칙들로만들어지는프로그램은나무구조를갖춘이차원의모습이다. 왜나무구조인가? Example 17 정수식을만드는귀납규칙을생각해보자. E n (n Z) E + E - E

36 36 모양과뜻 첫번째규칙은임의의정수는정수식이라고한다. 하나의정수만말단으로가지고있는나무가되겠다. 두번째규칙은두개의정수식을가지고 + 를이용해서정수식을만들수있다고한다. 이것이나무두개를양쪽으로매달고있고뿌리에는 + 를가지고있는나무가되겠다. 마지막규칙은하나의정수식을가지고 를이용해서정수식을만드는것이다. 이것도나무하나를매달고있고뿌리에는 - 를가지고있는나무가된다. Example 18 간단한명령형언어를생각해보자. 이언어로짤수있는프로 그램 C 는명령문 (command) 으로서다음의방법으로만들어진다 : C skip x := E if E then C else C C ; C E는위의예에서정의한정수식이라고하자. 위의방법들로만들수있는명령문들은모두나무구조물들이다. skip 만있는명령문은그것만말단으로가지고있는나무가되겠다. 두번째규칙은정수식나무를오른편에, 하나의변수를왼편에, 루트노드는 := 임을표시하고있는나무가된다. 세번째규칙은세개의나무 ( 정수식나무와두개의명령어나무 ) 를하부나무로가지고있고루트노드에는 if 문임을표시하고있는나무가된다. 마지막규칙은두개의명령어나무를하부나무로가지고있고루트노드에는순차적인명령문 ( ; ) 임을표시하고있는나무가된다. 프로그램을만들때필요한최소한의정보를가지고있는가장간단한문법을써보자. Example 17와 Example 18에서보여준규칙들에는규칙을읽는사람을돕기위해서필요이상의정보가있기도하다.

37 3.1 문법구조 syntax 37 다음이필요한정보만가지고있는더욱날씬한규칙일것이다 : C & = x E? E C C ; C C E n (n Z) + E E - E 긴심볼을쓸필요도없고, 심볼이중간에끼일필요도없고, 사이사이에 then 이나 else 같은장식이있을필요도없다. 오직각규칙마다다른간 단한심볼을쓰면그만이다. 아니면아예그러한심볼이필요없어도된다. 우리가각규칙마다구분할 수만있다면 : C & x E E C C C C E n (n Z) E E - E 하지만, 이렇게까지프로그램만드는방법을최대한요약해서보여줄필요는 없다. 문법규칙들을보고무엇을만드는방법인지를힌트해주는규칙들을사 용하게된다.

38 38 모양과뜻 요약된혹은구체적인 지금까지보아온문법규칙들을 요약된문법구조 abstract syntax라고도하는데, 요약된문법구조abstract syntax와구체적인문법구조concrete syntax의차이는프로그램을만들때사용하는규칙이냐, 읽을때사용하는규칙이냐, 에달려있다. 프로그램을만들때사용하는문법은지금까지보아온귀납적인방법이면충분하다. 만든결과는나무구조를가진이차원의구조물이다. 반면에프로그램을읽을때의문법은더복잡해진다. 왜냐하면, 대개만들어진프로그램을표현할때는나무를그리지않고일차원적인글자들의나열이되고이러한글자나소리의일차원적인실을받아서, 쓰거나말한사람의머리에그려져있었을 2차원의나무구조를복원시키는규칙들이되기때문이다. 구체적인문법 concrete syntax 은얼마나구체적일까? 나무구조가아니라일

39 3.1 문법구조 syntax 39 차원의실로표현되는다음의정수식프로그램을생각해보자 : -1+2 위의것은다음두개의나무구조중하나를일차원으로펼친것이다 : 어느것인가? 프로그램실 -1+2 를둘중의어느프로그램으로복구시킬것 인가? 요약된문법 E n (n Z) E + E - E 으로는둘중에어느구조로복구시켜야할지알수없다. 두가지구조를모 두구축할수있다. 정수식의문법이다음과같다면어떨까? E n (n Z) E + E - F F n ( E ) 위의규칙이말하는것은, 음의부호가앞에붙은정수식인경우는, 두가지밖에없다 : 말단자연수이거나, 괄호가붙은정수식이거나. 따라서, 프로그램실 -1+2 의경우는 의구조밖에는없다. 구체적인문법구조concrete syntax는혼동없이 2차원의프로그램구조물을복구하는데사용되는데, 이문법은프로그램복원parsing 혹은프로그램의문법검증parsing이라는과정의설계도가된다. 그과정은우리가프로그램을쓰면 ( 문자들의 1차원실로 ) 컴퓨터가그구조물을자동으로복원하는과정이다.

40 40 모양과뜻 우리는구체적인문법을더이상다루지않는다. 프로그램 이라고하면, 요약된문법규칙들로만들어진이차원의나무구조를뜻한다. 비록이곳에적는프로그램들이그나무구조를직접그리지는않았더라도, 그 2차원의구조물이무엇인지혼동되지않도록적절히괄호를쓰거나할것이다. 3.2 의미구조 semantics 의미구조semantics는프로그램이뜻하는바를정의한다. 프로그램이뜻하는바는무엇인가? 1+2 라는프로그램은무엇을뜻하는가? 결과값 3을뜻하는가, 1과 2을더해서결과를계산한다, 는과정을뜻하는가? 3을뜻한다고정의하는스타일, 뜻하는바궁극을수학적인구조물의원소로정의해가는스타일을 궁극을드러내는의미구조 denotational semantics라고한다. 반면에프로그램의계산과정을정의함으로써프로그램의의미를정의해가는스타일을 과정을드러내는의미구조 operational semantics라고한다. 다양한스타일의의미구조정의법은모두충분히엄밀하다. 그리고각스타일마다프로그램의미의성질을증명하는다양한기술이개발되어있다. 그럼왜여러가지스타일을살펴볼필요가있을까? 그것은다양한의미구조정의방식과증명기술들이모두종합적으로사용되는것이흔하기때문이다. 어떤때는궁극의스타일이적절하고어떤때는과정을드러내는스타일이적절하다. 각경우마다우리가드러내고싶은디테일의수준만큼만표현해주는의미구조방식을취사선택하게된다 과정을드러내는 과정을드러내는의미구조operational semantics는프로그램이실행되는과정을정의한다. 프로그램실행의과정을어느수준표현해야할까? 어느정도로자세한수준이필요할까? 계산과정에서삼성의칩들사이에일어나는전기신호들의흐름을일일이표현해야할까? 아니면 1이 1을계산하고 2가 2를계산하고 + 가

41 3.2 의미구조 semantics = 3이라는등식을적용하는것으로표현해야할까? 아니면실행되는과정을, 프로그램과그계산결과를결론으로하는논리적인증명의과정이라고표현해야할까? 의미구조를정의하는목표에맞추어그디테일의정도를정하게된다. 대개는상위의수준, 가상의기계에서실행되는모습이거나, 기계적인논리시스템의증명으로정의하게된다. 과정을드러내는의미구조도궁극을드러내는스타일denotational semantics처럼충분히엄밀하다. 다른것이있다면, 조립식 (compositional) 이아닐수있다 : 프로그램의의미가그프로그램 의부품들의의미들로만구성되는것은아니다. 그렇게되면좋지만, 아 니어도상관없다. 하지만귀납적 (inductive) 이다 : 어느프로그램의의미를구성하는부품들은귀납적으로정의된다. 이귀납이프로그램의구조만을따라되돌기도하지만 ( 이렇게되면조립식이된다 ), 프로그램이외의것 ( 의미를드러내는데사용되는장치들 ) 을따라되돌기도한다 큰보폭으로프로그램의실행이진행되는과정을큰보폭으로그려보자big-step semantics. 논리시스템의증명규칙들로표현된다. 증명하고자하는바는, 명령문 C와정수식 E에대해서각각 M C M 와 M E v 이다. M C M 는 명령문 C가메모리 M의상태에서실행이되고결과의메모리는 M 이다 로읽으면된다. M E v는 정수식 e는메모리 M의상태에서정수값 v를계산한다 로읽고.

42 42 모양과뜻 모든규칙들을쓰면이렇게된다 : M skip M M E v M x := E M{x v} M C 1 M 1 M 1 C 2 M 2 M C 1 ; C 2 M 2 M E 0 M C 2 M M if E then C 1 else C 2 M M E v M C 1 M M if E then C 1 else C 2 M v 0 M E 0 M while E do C M M E v M C M 1 M 1 while E do C M 2 M while E do C M 2 v 0 M n n M x M(x) M E 1 v 1 M E 2 v 2 M E 1 + E 2 v 1 + v 2 M E v M - E v 위의규칙들은논리시스템의증명규칙이라고이해해도된다. 명령프로그 램 C 의의미는임의의메모리 M 과 M 에대해서 M C M 를증명할수 있으면그의미가되겠다. 대개는 M 이비어있는메모리일때 C 를실행시키는 과정을나타내고싶으므로, C M 의증명이가능하면 C 의의미가된다. 그것이증명불가능하면 C 의의미는없는것이다. Example 19 x := 1 ; y := x + 1 의의미는 메모리에대해서다음과같은증

43 3.2 의미구조 semantics 43 명으로표현된다. 위의명령문을 C 라고하자. {x 1} x 1 {x 1} {x 1} x x := 1 {x 1} {x 1} y := x + 1 {x 1, y 2} C {x 1, y 2} 이렇게의미구조를정의하는방법을 자연스런 natural semantics, 구조적인 structural operational semantics, 혹은 관계형 relational semantics 의미구조라고도불린다. 자연스럽 다고하는이유는아마도 추론규칙 꼴로구성되어있고, 자연스런추론규칙 natural deduction rules 이라고불리는추론규칙이있어서그런이름을붙였을것이다. 구조적 이라고하는이유는두가지정도다. 지금돌아보면당연한모습처럼보이지만, 이러한스타일로계산과정을드러내는의미구조방식은당시의흔한방식보다는더욱짜임새가있었기때문이다. 당시의흔한방식은가상의기계를정의하고프로그램이그기계에서어떻게실행되는지를정의한다. 이러다보니, 기계의실행과정중에프로그램이부자연스럽게조각나면서기계상태를표현하는데동원되기도하고, 프로그램의의미를과도하게낮은수준의실행과정으로세세하게표현하게된다. ( 절에서자세히다룸 ). 이러한옛방식을 구현을통해서정의하기 (definition by implementation), 어떻게구현하는지보임으로서무엇인지정의하기 라고하는데, 이것보다는확연히 구조적 이지않은가. 프로그램의구조마다추론규칙이정의되고, 계산과정은그추론규칙들이레고블락이되어만들어내는하나의증명이되는것이다.

44 44 모양과뜻 구조적 이라고부르는다른이유는의미규칙들이한집합 ( 프로그램과 의미장치들간의관계쌍들의집합 ) 을귀납적으로정의하는방식이고, 그 귀납이프로그램이나의미장치들의구조를따라흐르기때문이다. 관계형 이라고도하는이유는위의추론규칙들이관계된짝들의집합을정의하는귀납적인방법으로도바라볼수있기때문이다. 관계된짝들이란 M C M 인 M, C, M 와 M E v인 M, E, v 들이다. 위의규칙들에의해서그러한관계를맺을수있는 M, C, M 과 M, E, v들이모아진다 작은보폭으로 프로그램의실행을작은보폭으로정의해보자 small-step semantics. (M, skip) (M, done) (M, E) (M, E ) (M, x := E) (M, x := E ) (M, x := v) (M{x v}, done) (M, E) (M, E ) (M, if E then C 1 else C 2 ) (M, if E then C 1 else C 2 ) (M, if 0 then C 1 else C 2 ) (M, C 2 ) (M, if n then C 1 else C 2 ) (M, C 1 ) n 0 (M, C 1 ) (M, C 1) (M, C 1 ; C 2 ) (M, C 1 ; C 2 ) (M, while E do C) (M, if E then C ; while E do C else skip) (M, done ; C 2 ) (M, C 2 )

45 3.2 의미구조 semantics 45 (M, E 1 ) (M, E 1) (M, E 1 + E 2 ) (M, E 1 + E 2 ) (M, E 2 ) (M, E 2) (M, v 1 + E 2 ) (M, v 1 + E 2) (M, v 1 + v 2 ) (M, v 1 + v 2 ) 이러한스타일을변이과정의미구조 transition semantics 라고도한다. 이방식에서재미있는것은문법적인 ( 겉모양을구성하는 ) 물건들과의미적 인 ( 속뜻을표현하는 ) 물건들이한데섞이고있다는것이다. 이것이문제될것은없다. 것모양을구성하는것들과속뜻을구성하는것 들이반드시다른세계에서멀찌감치떨어져있어야한다는것은, Tarski 라는 수학자가시작한전통일뿐이다. 프로그램이외의의미장치없이프로그램만을가지고도변이과정의미구 조 transition semantics 를정의할수도있다. 예를들어, 메모리를뜻하는 M 이라는 프로그램이외의의미장치없이. 예를들어, 간단한정수식프로그램들의의미는프로그램을다시쓰는과정 으로정의된다 : 다시쓰면 다시쓰면 6. 프로그램이외에다른 장치가사용되지않는다 문맥구조를통해서프로그램실행을프로그램을다시쓰는과정으로정의해보자. 예를들어, 다시쓰면 다시쓰면 6. 이렇게프로그램을다시써가는과정이프로그램의실행이라고볼수있다transition semantics. 두가지를정의해야한다 : 프로그램의어느부분을다시써야 ( 계산해야 ) 하는가? 다시써야할부분을무엇으로다시써야하는가? 프로그램의어느부분을다시써야 ( 계산해야 ) 하는가? 이질문에대한답은 실행문맥 evaluation context에의해서정의된다. 실행문맥의정의에따라서현재의프로그램을구성하다보면, 다시써야할부분 ( 계산해야할속부분 ) 이결정된다. 재미있는것은그정의가문법적으로가능하다는것이다.

46 46 모양과뜻 다음의정의를보자. 실행문맥을가지고있는프로그램 K를정의한다. K안에는 [] 가딱하나있다. 그곳이프로그램에서다시써야할부분, 먼저실행되야할부분이된다. 그러한부분을품은프로그램을강조하기위해 K[] 라고쓰고, 그빈칸에들어있는 ( 다시써야할 ) 프로그램부분 C 까지드러내어 K[C] 라고표현한다. 지금까지예로사용되어온언어에서, 다시써야할부분 [] 을내포한실행 문맥이문법적으로다음과같이정의된다 : K [] x := K K ; C done ; K if K then C else C while K do C K + E v + K - K 즉, 지정문 (assignment command) 에서는다음에실행되야할부분 K는오른쪽식에있고 x := K 순서문에서 (sequential command) 뒤의명령문이다음에실행되야할부분이라면, 앞의명령문은시행이이미끝났을때만이고 done ; K 덧셈식에서오른쪽식이다음에실행되야할부분이라면, 왼쪽식의결과는나와있어야한다 v + K.

47 3.2 의미구조 semantics 47 다시써야할부분을무엇으로다시써야하는가? 이제이질문에대한답 은다시쓰기규칙 rewriting rule 에의해서정의된다. 우선, 다시쓸곳은다시쓰 면되고 속에서어떻게다시쓰여지는가하면 : (M, C) (M, C ) (M, K[C]) (M, K[C ]) (M, E) (M, E ) (M, K[E]) (M, K[E ]) (M, x := v) (M{x v}, done) (M, done ; done) (M, done) (M, if 0 then C 1 else C 2 ) (M, C 2 ) (M, if v then C 1 else C 2 ) (M, C 1 ) (v 0) (M, while 0 E do C) (M, done) (M, while v E do C) (M, C ; while E do C) (v 0) (M, v 1 + v 2 ) (M, v) (v = v 1 + v 2 ) (M, - v) (M, v) (M, x) (M, M(x)) 이다. Example 20 x := 1 ; y := x + 1 의의미를문맥구조를통해서알아보면, (, x := 1) ({x 1}, done) (, [x := 1] ; y := x + 1) ({x 1}, done ; y := x + 1) 다음은, ({x 1}, x) ({x 1}, 1) ({x 1}, done ; y := [x] + 1) ({x 1}, done ; y := 1 + 1)

48 48 모양과뜻 다음은, ({x 1}, 1 + 1) ({x 1}, 2) ({x 1}, done ; y := [1 + 1]) ({x 1}, done ; y := 2) 다음은, ({x 1}, y := 2) ({x 1, y 2}, done) ({x 1}, done ; [y := 2]) ({x 1, y 2}, done ; done) 다음은 ({x 1, y 2}, done ; done) ({x 1, y 2}, done) 가상의기계를통해서 어떤가상의기계virtual machine가정의되어있고프로그램의의미는그프로그램이그기계에서실행되는과정으로정의된다. 기계에서실행되는과정은기계상태가매스텝마다변화되는과정이된다. 예를들면, 정수식의의미가한기계의실행과정으로다음과같이정의된다. 변수가없는정수식만을생각해보자 : E n E + E - E 정의하는기계는소위말하는 스택머신 이다. 그기계는스택 S와명령어들 C로구성되어있다 : S, C

49 3.2 의미구조 semantics 49 스택은정수들로차곡차곡쌓여있다 : S ɛ ( 빈스택 ) n.s (n Z) 명령어들은정수식이나그조각들이쌓여있다 : C ɛ ( 빈명령어 ) E.C +.C -.C 기계작동과정의한스텝은다음과같이정의된다 : S, n.c n.s, C S, E 1 + E 2.C S, E 1.E 2.+.C n 2.n 1.S, +.C n.s, C (n = n 1 + n 2 ) n.s, -.C n.s, C 정수식 E 의의미는 ɛ, E 가된다. 또다른스타일로는, 명령어들을정수식과는다른, 기계고유의명령어들로 정의할수도있다 : C ɛ ( 빈명령어 ) push n.c (n Z) pop.c add.c rev.c

50 50 모양과뜻 그리고, 기계작동과정의한스텝도다음과같이정의된다 : S, push n.c n.s, C n.s, pop.c S, C n 1.n 2.S, add.c n.s, C (n = n 1 + n 2 ) n.s, rev.c n.s, C C에있는첫명령어를수행하면서기계상태가변하는과정이다. 그리고, 이제정수식들이스택머신의어떤명령어들로변환되는지를정의하면된다 : [n] = push n [E 1 + E 2 ] = [E 1 ].[E 2 ].add [- E ] = [E ].rev 어떻게정의하든간에, 이러한기계의과정이매우임의적이라고생각될수있다. 가상의기계를어떻게디자인하는가? 그기계의디테일은어느레벨에서정해야하는가? 그에대한답은프로그램의의미를정의하는목적, 그에따라결정될것이다. 대개가상기계를사용해서프로그램의의미를정의하는것은프로그래밍언어를구현하는단계에서사용된다 : 프로그래밍언어의번역기compiler나실행기interpreter를구현할때. 프로그래밍언어의성질을궁리하거나그언어로짜여진프로그램들의관심있는성질을분석할때에사용하는의미구조로사용되는예는드물다. 가상의기계는대개가이와같은분석에서는필요하지않은디테일 ( 기계의볼트넛트들 ) 을드러내기때문이다 궁극을드러내는 궁극을드러내는의미구조denotational semantics는프로그램의의미를전통적인수학의세계에서정의한다. 프로그램이뜻하는바를수학의물건으로정의하는것이다. 영어 denotational 을 궁극을드러내는 이라고번역한이유는? 지칭하

51 3.2 의미구조 semantics 51 는바를드러내는의미구조 라고직역할수있지만, 그러면그고유특징을드러내지못하기때문이다. denotational semantics 는프로그램의의미를결정하는한방법을뜻하는고유명사이다. 그방법의특징은, 수학의세계에서의미하는바그궁극을드러내는것이다. 특히, 프로그램부품들의의미들이전체프로그램의의미를구성한다. 이러한이유로조립식의미구조compositional semantics라고불리기도한다. 조립식의미구조가좋은이유는명백하다. 프로그램의의미가쉽게결정된다. 프로그램생김새만잘뜯어서그부품들을파악하면, 그부품들의의미를가지고전체프로그램의의미가결정된다. 예를들어보자. 아래와같은명령형언어imperative language를생각해보자. 우리가늘알고있는명령형언어라고보면된다. C skip x := E if E then C else C C ; C E n (n Z) x E + E - E 프로그램은명령문이되고, 명령문은기계의메모리에정수값들을저장시키면서일을진행한다. 프로그램의변수는메모리의주소를뜻하기도하고 ( 지정문 x := E 의왼편에사용되는경우 ) 그주소에저장된정수값을뜻하기도한다 ( 계산식 E에서사용되는경우 ). 이렇게간단한의미구조를수학적으로모델하기는어렵지않다. 우선, 명령어 C의의미는메모리상태를변화시키는함수로정의한다 : 메모리를받아서메모리를내어놓는. 메모리도또다른함수로정의한다 : 프로그램변수를받아서그변수가가지는정수값을내어놓는. 프로그램변수는프로그램에서

52 52 모양과뜻 사용하는변수이름이다. 그리고, 이런물건들이어느집합에소속되는지를정의하자. 그러한집합을의미공간semantic domain이라고한다. 아래 Memory, Value, Var, Memory Memory, Memory Value등이의미공간이되겠다 : M Memory = Var Value z Value = Z x Var = ProgramVariable 명령문 C의의미 [C ] Memory Memory 계산식 E의의미 [E ] Memory Z 이제, 프로그램의의미는프로그램의각각의경우에대해서위에마련한의미 공간의원소들을가지고다음과같이정의된다 : [skip] M = M [x := E ] M = M{x [E ] M} [if E then C 1 else C 2 ] M = if [E ]M 0 then [C ]M else [C 2 ]M [C 1 ; C 2 ] M = [C 2 ] ([C 1 ] M) [n] M = n [E 1 + E 2 ] M = ([E 1 ] M) + ([E 2 ] M) [- E ] M = ([E ] M) 조립식인것이보이는가? 보기좋다. 모든프로그램의의미는그부품들의의 미만을가지고구성되어진다. 예로, if- 문의의미는그부품들의의미들로정 의되어있지않은가 : [if E then C 1 else C 2 ] = [E ] [C 1 ] [C 2 ] 조립식일수있는이유 : 의미공간이론 domain theory 그런데, 이렇게부품들의의미로전체의의미를구성하는상식적인방식이일

53 3.2 의미구조 semantics 53 사천리가능하지는않다. 명령형언어에서반복문이가능하다고하면, 반복문의의미를반복문을구성하는부품들의의미만으로정의하는것이간단치않게된다. 조립식으로의미를결정하기가난처한경우를살펴보자. 명령문중에반복문으로 while문을쓸수있다고하자. C while E do C while 문은조건식 E 의값이 0 이면아무것도안하고끝나지만, 조건식의값이 0 이아닐때는명령문 C 를실행하고난후다시같은 while 문을반복하게된다. 따라서아래와같이 while 문의의미를정의해보려고할수있겠다 : [while E do C ]M = if [E ]M 0 then [while E do C ]([C ]M) else M 조립식인가? 그렇지않다. [while E do C ] 가 [E ] 와 [C ] 만가지고정의되지않고자기자신 [while E do C ] 도사용되고있다. 따라서위의것은 [while E do C ] 의정의가아니다. 이것은단순히 [while E do C ] 에대한방정식일뿐이다. 그방정식의해가바로 [while E do C ] 의정의일것이다. 그렇다면그해는무엇일까? 해는과연있을까? 항상있을까? 있다면유일하게있을까? 이에대한모든답은모두예, 라고할수있다. 이유는의미방정식에서사용하는모든물건들 ( 원소들과연산자들 ) 이소속된의미공간semantic domain이좀특별하기때문이다. 그러한의미공간에대한이론이의미공간이론domain theory인데, 이이론은다음을확인해준다 : 모든컴퓨터프로그램 ( 모든계산가능한함수들 ) 의의미 ( 의미방정식의해 ) 는의미공간이론에서규정하는성질의집합안에서유일하게존재하고그것은이러이러하다. 의미공간이론이규명해낸그러한집합은 CPOcomplete partial order set라는

54 54 모양과뜻 성질을만족하는집합이다. 그래서, 모든프로그램의의미방정식들에쓰이는것들은모두어떤 CPO의원소들이고, 특히방정식에서사용하는연산자들은모두 CPO에서 CPO로가는연속함수continuous function로정의된다. 그러면, 의미방정식의해는유일하게항상어떤 CPO안에존재하게된다. 프로그램 C의의미 [C ] 에대한의미방정식은항상다음과같고 [C ] = F([C ]) 여기서 [C ] D ( 어떤 CPO) 그리고 F D D (D 에서 D 로가는연속함수들의 CPO) ([while E do C ] 의의미방정식에해당하는 F는무엇?) 이방정식의해는항상연속함수 F의최소고정점least fixpoint으로정의된다. 연속함수의최소고정점은 CPO의성질과연속함수의조건때문에항상유일하게존재한다. 이내용은다음절에서다루기로하자. 아무튼, 이렇게최소고정점least fixed point이라는수학적기법을통해서궁극의의미가조립식으로가능해지는이유로해서, 궁극적인의미구조를고정점의미구조fixpoint semantics라고불리기도한다 CPO, 연속함수, 최소고정점프로그램의수학적인 ( 궁극적인 ) 의미는 CPO(complete partial order) 라는공간의원소로정의된다. 어느집합이 CPO가되려면, 그집합의원소들간에어떤순서가있고 ( 임의의두원소간에순서가있을필요는없다, 따라서 partial order), 모든원소보다아래에있는밑바닥원소 ( 주로 으로표현한다 ) 가항상있고, 그순서를가지고일렬로줄을세울수있는원소들 (chain) 이있다면그줄에있는모든원소들보다위에있으면서가장작은원소 (LUB, least upper bound) 를항상가지고있는집합이다. CPO D 1 에서 CPO D 2 로가는함수 f : D 1 D 2 가연속함수란, 체인chain을체인으로보내면서, D 1 의체인chain의 LUB를보전해주는함수이다. 체인의 LUB을취하고함수를적용한결과가함수를그체인의원소들에각각취하고

55 3.2 의미구조 semantics 55 그결과를 LUB 한것과일치하는함수이다 : chain X D 1.f( X) = x X f(x). CPO 에서 CPO 로가는연속함수 f 는항상최소고정점 fixf 이유일하게있고, 그것은 f( ) f(f( )) = i N f i ( ) 이다.( 왜?) CPO성질을만족하는집합들은매우다양하게만들수있다. 집합을가지고 CPO를만들수있고, 만들어논 CPO들을가지고조합해서새로운구조의 CPO를만들수있다. 집합에밑바닥원소를하나추가하고올려붙인 (x y iff x = y x = ) 집합은 CPO이다. CPO와 CPO의데카르트곱Cartesian product도 CPO이다. CPO와 CPO의출신을기억하는합separated sum도 CPO이다. CPO에서 CPO로가는연속함수들의집합도 CPO이다. ( 이렇게 CPO들을가지고구축한 CPO들의원소사이의순서는부품 CPO들의순서를가지고정의되는데, 그순서를어떻게정의해야결과가 CPO가될까?) Example 21 다음과같이정수의집합 Z에서올려붙인집합 Z = Z { } 을생각하자. Z 원소들사이의순서는없고, 순서는오직 과 Z 사이에만존재한다 : x Z. x. 모든체인은유한한길이를가지고있으면맨꼭대기의원소가그체인의 LUB이된다. 따라서 Z 은 CPO이다. Example 22 CPO D 1 과 D 2 의데카르트곱 Cartesian product D 1 D 2 = { x, y x D 1, y D 2 } 은 CPO가된다. 이곱집합의원소들사이의순서를조립식component-wise으로했을때이다 : x, y x, y iff x D1 x y D2 y.

56 56 모양과뜻 이때, 최소의원소는 D1, D2 가된다. Example 23 CPO D 1 과 D 2 의합 D 1 + D 2 = { x, 1 x D 1 } { x, 2 x D 2 } { } 은 CPO 가된다. 이합집합의원소들사이의순서는, 이가장작고, 그외에는 고향이같은원소들끼리그고향에서의순서로정했을때이다 : x, 1 x, 1 iff x D1 x x, 2 x, 2 iff x D2 x 여기서잠깐, 인자가 x인연속함수를표현하는방법을이야기하고가자. 연속함수는람다계산법Lambda Calculus에서사용하는함수를표현하는방법을빌려서, λx. 함수몸통 로표현하도록하자. 예를들어, 1을더하는연속함수는 λx.x + 1 로표현한다. Example 24 CPO D 1 에서 D 2 로가는모든연속함수의집합 D 1 D 2 은 CPO가된다. 연속함수들사이의순서를조립식point-wise으로정의했을때이다 : f g iff x D 1.f(x) D2 g(x). 가장작은원소는 λx. D2 가된다. 의미방정식에서사용하는모든물건들은 CPO의원소이다. 연산자들은모두 CPO에서 CPO로가는연속함수들이고, 연산자가아닌물건들도모두 CPO의원소들이다. 따라서모든의미방정식의해는항상어떤연속함수 F의고정점임을나타내고있고 : X = F(X)

57 3.2 의미구조 semantics 57 위의방정식의해는 F 의최소고정점 fixf 로정의할수있다 : fixf = i N F i ( ) 자이제, CPO 와연속함수의최소고정점이라는장치를이용해서 while- 문의 의미가어떻게조립식이되는지보자. 우선, 우리가직관적으로구성한의미공간들은모두 CPO 가되야한다 : M Memory = Var Value 연속함수 CPO z Value = Z 올려붙인 CPO x Var = ProgramVariable 올려붙인 CPO 명령문 C의의미, 연속함수 [C ] Memory Memory 연속함수 CPO 계산식 E의의미, 연속함수 [E ] Memory Z 연속함수 CPO 그위에서 while- 문의의미방정식은 [while E do C ]M = if [E ]M 0 then [while E do C ]([C ]M) else M 이다. 메모리를받아서메모리를내어놓는연속함수의표현 (λm. ) 으로다 시쓰면, [while E do C ] = λm.if [E ]M 0 then [while E do C ]([C ]M) else M. 위의방정식을 X = F(X) 의모양으로보면, X 는 [while E do C ] 에해당하고, 연속함수 F 는 λx.(λm.if [E ]M 0 then X([C ]M) else M) (Memory Memroy) (Memory Memroy)

58 58 모양과뜻 에해당하게되므로, while- 문의의미 [while E do C ] 는위함수의최소고정점 으로정의된다 : [while E do C ] = fixf Memory Memory = fix(λx.(λm.if [E ]M 0 then X([C ]M) else M)) 조립식인것이보이는가? [while E do C ] 는 [E ] 와 [C ] 를가지고조립되어있 다.

59 4 장 기계중심의언어 5 리에걸친안개속. 어떻게프로그래밍언어를디자인해야하는지, 무엇이문 제일지가드러나지않은상태. 그렇게디자인한프로그래밍언어. 그모습을 따라가보자. 상식선에서디자인해간언어의모습. 옆에컴퓨터가있다. 사용해야한다. 컴퓨터에게시킬일을편하게정의할 수있는방법을고안하자. 이렇게 C 언어를만들었던과정은당시로서는매우 상식적인과정을밟는다. 그러나되돌아보면아쉬움이많다. 현재의프로그래밍언어기술에기대어 바라볼때 C 로대표되는옛시절의솜씨, 이과정을되돌아볼것이다. 왜이과정을반복할까? 우선그과정에서도지금까지살아남은중요한개념들이있다. 살펴볼것이다. 또다른의도는, 과거가어설펐듯이현재의바람직한프로그래밍언어기술이라는것도미래에는어설픈모습으로보일수있다는경계.

60 60 기계중심의언어 4.1 주어진기계 우리에게주어진기계는다음과같다 : 메모리가있다. 중앙처리장치가있다. 입출력이가능하다. 메모리를읽고, 메모리에쓸수있다. 메모리에서읽은것을화면에뿌릴수있고, 키보드에서읽은것을메모리에저장할수있다. 중앙처리장치cpu는기초적인기계어명령들을처리하는실행기interpreter이다. 실행할수있는기계어명령의갯수는유한하고고정되어있다. 그실행기는전자회로디지탈컴퓨터의경우매우작은전깃줄들로구현되어있다. 그기계는폰노이만머신Von Neuman machine이다. 기계가실행할명령문들이메모리에보관될수있다. 그기계는명령문하나하나를메모리에서읽어와서실행한다. 메모리에실려있는명령문들에따라그기계는다른일을하

61 4.2 언어키우기 0: K 는셈이다. 그기계는보편만능의기계universal machine이다. 기계적으로계산가능한모든것 들을계산해낼수있다. 기계적으로계산가능한어떤일이라도주어진명령문들로구성해낼수있다. 놀랍다. 기계적으로계산가능한것은무한히많이있을수있다. 하지만어느것이라도유한개의정해진기계어명령들로조합할수있다. 마치유한한한국어단어들만으로무한히많은말을조합하고이해할수있듯이. 아무튼, 그기계의중앙처리장치cpu는유한개의정해진명령문들만을알고있다. 그것으로 보편만능 이가능한것이다. 기계가실행하도록준비하는명령문들의조합이프로그램이다. 프로그램은그기계에내리는명령이다. 그기계는그명령대로충실히일을진행한다. 이기계를좀더편리하게사용하기위한언어를고안해보자. 그기계어보다더상위의언어를고안하자. 4.2 언어키우기 0: K 변수 : 메모리주소에이름붙이기 프로그램에서는이름을사용하고자한다. 우선, 메모리주소에이름을지을수있게하자. 이름으로메모리주소를대신하도록. 명령문은여러개가순서대로실행되도록하고싶다. 반복이있다. 입출력이있다. 조건에따라서실행되는명령을구분하고싶다. 이러한기초적인조건에맞추어서다음과같은문법의언어로시작해보자. 아래의정의가 K---언어로짤수있는프로그램들의집합을정의한다. 명령문과식을만드는귀납적인방법이정의되있다. 프로그램은하나의명령문

62 62 기계중심의언어 이다. 명령문은여러명령문들과식들로꾸며진다. 명령문 Command C skip x := E C ; C if E then C else C while E do C for x := E to E do C read x write E 식 Expression E n (n Z) true false x E + E - E E < E not E 프로그램 P C 명령문은기계의메모리상태를변화시킨다. 식은기계의메모리를참고해서 값을계산한다. 각명령문과식의의미를정확히정의하자. 우선의미를정의해갈때사용할원소semantic object들이어느집합 ( 의미공간 )semantic domain의원소들인지를정하자. 값은정수거나참 / 거짓이다. 따라서값의집합은정수집합이거나참 / 거짓집합니다. 메모리는주소에서값으로가는테이블일것이다. 테이블은수학적으로는하나의함수이다. 정의구역은메모리주소, 공변역은값. 특히정의구역은메모리주소집합중에서유한한집합이되겠다. 주소는프로그래머가사용하는이름들의집합으로정의하자.

63 4.2 언어키우기 0: K 그래서의미정의에사용할의미공간 semantic domain 들은아래와같다 : n Z Integer b B Boolean v Val = Z + B M Mem = Addr fin Val x, y Addr = Id 정수를 n 으로쓸것이다. 참이나거짓은 b 로, 값은 v 로, 메모리는 M 으로, 주소 는 x, y, z 등으로쓸것이다. Notation 1 Z + B는두집합 Z와 B의합집합을뜻한다. Addr fin Val는함수 들의집합을뜻한다. 함수들의이미지는 Val 집합에포함된다. 함수들의정의 구역은집합 Addr 의유한한부분집합이다. 마크 fin (finite) 을화살표위에붙 인이유이다. 함수 f A fin B를가지고 f{x v} 라고쓰면 ( 이때, x A 이고 v B), A fin B에있는새로운함수인데 x에서의이미지만 v로정해지고나머지는 f와 똑같은함수를뜻한다. 프로그램의의미는논리시스템의증명규칙들로정의된다. 다음을증명하 는규칙들이될것이다. M C M 와 M E v M C M 는메모리 M에서명령 C를실행하면메모리상태가 M 로변한다, 는사실을뜻한다. M E v는메모리 M에서식 E를실행하면값이 v가계산된다, 는사실을뜻한다. 아래는위와같은사실들을증명하는논리시스템이다. 주어진프로그램 C가있을때, 이논리시스템에서 M C M 가증명되는경우만프로그램 C는의미가있는것이다. 그러한증명이불가능한 C와 E는의미없는명령문이고식인것이다.

64 64 기계중심의언어 M C M M skip M M E v M x := E M{x v} M C 1 M 1 M 1 C 2 M 2 M C 1 ; C 2 M 2 M E true M C 1 M M if E then C 1 else C 2 M M E false M C 2 M M if E then C 1 else C 2 M M E false M while E do C M M E true M C M 1 M 1 while E do C M 2 M while E do C M 2 M E 1 n 1 M E 2 n 2 M{x n 1 + 0} C M 0. M{x n 1 + (n 2 n 1 )} C M n2 n 1 M for x := E 1 to E 2 do C M n 2 n 1 M E v M read x M{x n} M E v M write E M M n n M x M(x) M E 1 n 1 M E 2 n 2 M E 1 + E 2 n 1 + n 2 M E n M - E n

65 4.2 언어키우기 0: K M E 1 n 1 M E 2 n 2 M E 1 < E 2 n 1 < n 2 M E b M not E not b 이름이곧메모리주소다. 새메모리주소를사용하고자하면다른이름을 사용하면된다. 입출력문의의미를정한규칙이특이하다. 입력문은외부에서임의의정수 를받아서지정한메모리주소에보관하는것이다. 외부세계에묻고입력받는 과정을드러낼필요는없다. 출력도외부세계에계산한값을보여주는과정을 드러낼필요는없다. 의미를결정하는데필요한내용들은아니므로 이름의두가지의미 이름안에는무엇이있나? 이름이의미하는것은무엇인가? 혼동되게도 K--- 에 서는두가지역할을한다. 이름의의미가두가지다. 했다 : 우선메모리주소에이름을붙인것이므로, 이름지어진메모리주소를뜻 M E v M x := E M{x v} 하지만, 그이름으로그이름이지칭하는메모리주소에있는값을뜻하기 도했다 : M x M(x) 이렇게이름이뜻하는두개의값을이름의 L-value (left-value) 와 R-value (rightvalue) 라고부른다. 이름이 x := E 의왼쪽에나타났을때와오른쪽식 E 안에 나타났을때그의미하는바가다르기때문이다. 왼쪽에나타났다면이름은 메모리주소를뜻한다. 오른쪽에나타났을때는그메모리주소에보관된값 을뜻한다. 메모리주소의이름이어떤때는그주소에보관되있는값이되기도하는 혼동이싫다면, 두개의다른의미는두가지다른문법으로표현하도록하면될 것이다. 예를들어, 이름의의미를하나로정의하자. 메모리주소로. 그리고

66 66 기계중심의언어 그메모리주소의값을뜻할때는이름앞에! 표시를하도록하는것이다. 예를 들어, K--- 의 x := x + 1 는 x :=!x + 1 로쓰도록하는것이다. 그런데, 이렇게하면프로그래머가조금불편해하지 않을까? 프로그램식에나타나는모든이름앞에! 를붙여야하므로 x + y + 1 대신에!x +!y + 1. 이러한편리함이언어가복잡해지면서는프로그램을이해하기어렵게만드는눈엣가시가된다. K---를키워가면서살펴볼것이다. 이름을기계중심의언어에서는변수variable라고도부른다. 이름이의미하는메모리주소의값이변할수있으므로. 프로그램실행중에변수가의미하는주소에새로운값을써넣을수있으므로 이름의유효범위 프로그래머가메모리주소에이름을짓기시작하면서문제가생긴다. 같은이름을다른용도로도쓰고싶다면? 즉, 같은이름을다른메모리주소를위해재사용하고싶다면? 이것은자연스러운요구이다. 항상다른이름을고안해야한다면프로그래머의불편은클것이다. 이세상에태어나는모든사람들의이름이모두달라야한다면이름짓는것이얼마나골치아프겠는가? 위의 K---언어에서는같은이름은같은메모리주소를뜻한다. 다른메모리주소를위해서는다른이름을사용해야한다. 같은이름을다른메모리주소의이름으로사용할수가없다. 프로그램에서사용하는메모리주소가매우많다면, 얼마나많은다른이름을고안해야할까? 같은이름을다른메모리주소를위해서쓸수는없을까? 이름을재활용할수는없을까?

67 4.2 언어키우기 0: K 이문제를해결한방안은이미있다. 수학이나모든엄밀한논술에서사용하는방안이다. 이름의유효범위scope를일정한범위로만제한하는것이다. 이름들의유효범위scope를프로그램전체중에서일부분이되도록하는것이다. 그러면유효범위가겹치지않는다면, 같은이름이다른메모리주소를뜻하는것으로재사용될수있는것이다. 그렇다면, 그유효범위scope는어떻게표시할까? 수학에서사용하는방안을빌려오자. 프로그램텍스트의범위로이름의유효범위scope가결정되도록하자. 이방식이훌륭한이유는, 수학에서지난 2000년이상성공적으로사용돼왔기때문이다. 왜? 이름의유효범위를쉽게알아볼수있기때문이다. 이름의유효범위scope는다음의방식으로정해진다 : C. let x := E in C 우선 x라는이름은새로운메모리주소를뜻한다. 이름을새롭게선언하는셈이다. 그주소에저장되는초기값은 E의값이다. 그리고그이름이그주소를의미한다는것은명령문 C 안에서만유효하다. 즉, x의유효범위scope는 C 이다. 이름의유효범위scope는프로그램텍스트의일부분인것이다. 그범위이외에서는 x는다른메모리주소를뜻할수있다. 같은이름이여러주소를뜻하도록재사용될수있다. 이름이명령문에나타날때, 어느주소를뜻하는가? 그곳을감싸는가장가까운 let-명령문이다. 그이름을선언한. 당연한규칙이다. 이름의실체가그이름이나타나는프로그램텍스트에의해결정되므로. 프로그램은나무구조라는것을상기하자. 이름이나타난곳에서그나무구조를타고위로위로올라가면서가장먼저만나는, 그이름을선언한 let-명령문. 그곳에서정한메모리주소가그이름의실체가된다. 그리고유효범위들은서로완전히포섭되거나완전히별개의경우밖에는없다. 프로그램의문법이그것을보장한다. 유효범위두개가일부분만겹치는경우는없다.

68 68 기계중심의언어 환경 같은이름이다른것을지칭할수있는프로그램에서, 이름의실체를결정해주는규칙은위에서이야기한대로다. 나타난이름, 그곳을감싸는가장먼저만나는, 그이름을선언한 let-명령문. 프로그램의의미를정확히정의하는데는위와같은규칙을정확히드러내야한다. 환경environment이라는것을가지고의미구조를정확히정의할수있다. 환경environment은이름의실체를정의한함수이다. σ Env = Id fin Addr M Mem = Addr fin Val l Addr an index set

69 4.2 언어키우기 0: K 환경은이름의실체 ( Addr, 메모리주소 ) 를결정한다. 이름들에서주소들로가는유한함수이다. 메모리는주소들에값들을대응시키는유한함수이다. 주소는이제더이상프로그램에나타나는이름이될수없다. 그것과는다른집합이될것이다. 환경이새롭게의미구조semantics 정의에사용된다. 그래서프로그램의의미는다음두개를증명하는규칙들이된다 : σ, M C M 와 σ, M E v 예전과는다르게환경 environment σ 가명령문 C 와식 E 의의미를정의하는데 필요하게되었다. 이름이 C 나 E 에나타날때, 그이름이지칭하는메모리주 소가어떤것이되는지를환경 σ 가결정해준다. 이름은이제더이상곧메모 리주소가아니다. 이름이지칭하는주소는현재의환경 (σ) 이결정해준다. 의미정의의판단 σ, M C M 는메모리 M 과환경 σ 에서명령 C 를 실행하면메모리상태가 M 로변한다, 는사실을뜻한다. σ, M E v 는메 모리 M 과환경 σ 에서식 E 를실행하면값이 v 가계산된다, 는사실을뜻한다. 이제는이름을사용하고자하면, 항상 let- 명령문으로정의하고사용해야 한다. 이름은환경을통해서실체가결정되고, let- 명령문에의해서만이새로 운이름의실체가환경 (σ) 에덧붙여지기때문이다 : σ, M E v σ{x l}, M{l v} C M σ, M let x := E in C M l Dom M 사용하려는이름의실체를현재의환경 (σ) 이모른다면, 프로그램은의미가 없다. 실행될수없다. 이름이나타나면그실체는항상현재환경 (σ) 을참조 해서결정된다 : σ, M E v σ, M x := E M{σ(x) v} σ, M x M(σ(x)) σ, M read x M{σ(x) n}

70 70 기계중심의언어 같은이름이다른주소를지칭할수있다. 이름의재활용, 동명이인. 그러나거꾸로는아니다. 다른이름이같은주소를지칭할수는없다. 같은대상을지칭하는다른이름은가능하지않다. 별명alias은없다. 위의언어로별명alias이만들어지는경우는없다. σ, M C M σ, M E v σ{x l}, M{l v} C M σ, M let x := E in C M l Dom M σ, M skip M σ, M E v σ, M x := E M{σ(x) v} σ, M C 1 M 1 σ, M 1 C 2 M 2 σ, M C 1 ; C 2 M 2 σ, M E true σ, M C 1 M σ, M if E then C 1 else C 2 M σ, M E false σ, M C 2 M σ, M if E then C 1 else C 2 M σ, M E false σ, M while E do C M σ, M E true σ, M C M 1 σ, M 1 while E do C M 2 σ, M while E do C M 2 σ, M E 1 n 1 σ, M E 2 n 2 σ, M{x n 1 + 0} C M 0. σ, M{x n 1 + (n 2 n 1 )} C M n2 n 1 σ, M for x := E 1 to E 2 do C M n 2 n 1 σ, M read x M{σ(x) n}

71 4.2 언어키우기 0: K σ, M E v σ, M E v σ, M write E M σ, M n n σ, M x M(σ(x)) σ, M E 1 n 1 σ, M E 2 n 2 σ, M E 1 + E 2 n 1 + n 2 σ, M E n σ, M - E n σ, M E 1 n 1 σ, M E 2 n 2 σ, M E 1 < E 2 n 1 < n 2 σ, M E b σ, M not E not b 자유로운혹은묶여있는 프로그램에서사용되는이름의실체를찾을수없다면그이름은자유로운이 름 free variable 이라고한다. 자유로운이름을가지고있는프로그램의의미는정 의될수없다. 프로그램내에서는모든이름들은 let-명령문의선언으로정의되어있어야한다. 이름의실체가정의된정상적인경우를묶여있는이름bound variable이라고한다.

72 72 기계중심의언어 전체프로그램이아니라제한된지역을기준으로자유로운이름과묶여있 는이름이이야기되기도한다. 프로그램텍스트의어느지역만한정해서보면 서, 그안에서사용되는이름이자유롭거나묶여있다고판단하기도한다 설탕구조 프로그래밍언어는꼭필요한것만으로구성되어있지는않다. 위의 K--- 언어에서도불필요하지만사용자의편의를위해서제공해주는것이있다. 예를들어, for x := E 1 to E 2 do C는 while문을이용해서같을일을하는명령어로바뀔수있다 : for x := E 1 to E 2 do C low := E 1; high := E 2 ; while high low do (x := low; C; low := low + 1)

73 4.3 언어키우기 0: K 단, 위와같이 for-문을 녹이는 것이항상옳으려면 low와 high라는이름들이 E 1, E 2, C에서사용되어서는않된다. 특히, 위의 for-문이프로그램에포함되있을수있는데, 이경우에는 low와 high라는이름들이 E 1, E 2, C 뿐아니라전체프로그램에서사용되어서는않된다. 아무튼, 이렇게편의를의해서제공하는문법구조를설탕구조syntactic sugar라고한다. 설탕구조syntactic sugar는언어에진정새로운것을제공하지는않는다. 프로그래밍언어에서설탕구조syntactic sugar는프로그래머의편의를위해서제공될뿐이다. 프로그래밍언어자체를연구하는사람들은그런모든설탕을없앤최소의코어만을가지고연구한다. 프로그래밍언어를처리하는실행기interpreter나번역기compiler도실행이나번역전에프로그램에뿌려져있는모든설탕을코어만으로다시쓰는작업을진행한다. 그리하여실행이나번역은작은코아에대해서만정의해놓으면되도록.

74 74 기계중심의언어 4.3 언어키우기 I: K 프로시져 : 명령문에이름붙이기 메모리주소뿐아니라, 명령문에도이름을붙일수있도록하자. 그래서그명령문을반복해서쓰지않고도이름만으로그명령문을수행할수있도록. 조금더나아가, 이름붙은명령문들을일반화해서인자에의해서조금씩다른일을할수있도록하자. 예를들어, 변수 x의값을읽어서 1을더한값을다시쓰는명령문보다는, 변수 x의값을임의의크기만큼증가시키는명령문으로일반화하자. 그명령문에인자가있어서인자를통해서증가시키고싶은양을전달할수있도록. 이렇게인자를받는명령문에이름을붙인것을프로시져procedure라고한다. 이름을지을때는항상그유효범위를정하도록하므로, 기존의 let-명령문을이용해서프로시져를정의할수있도록하자 : C. let proc f(x) = C in C f (E) let proc f(x) = C in C 에서는두개의이름이선언되었다. 프로시져이름 f와인자이름 x. f는명령문 C의이름이다. x는프로시져가사용될때의인자값을보관하는메모리주소의이름이다. 인자이름 x의유효범위scope는 C이다. 프로시져이름 f의유효범위scope는 C 이다. 재귀호출이가능한프로시져를위해서는 f의유효범위는 C 뿐아니라 C까지도포함되야한다. 프로시져를사용하는명령문 f (E) 은 f로이름붙은명령문을실행시킨다. 그런데, 인자로 E 값을사용하라는것이다. 의미를정확히정의하자. 우선환경environment이확장된다. 이름의실체는

75 4.3 언어키우기 I: K-- 75 메모리주소뿐아니라프로시져까지포함된다 : σ Env = Id fin Addr + Procedure 그러나프로지져의실체 Procedure 가무엇이되야하는지에따라서프로시져 의호출에관한의미가전혀달라질수있다 이름의유효범위 동적으로결정되는유효범위 우선 Procedure = Id Command 로정의해보자. Notation 2 두집합 A 와 B 가있을때, A B 는두집합의원소들의쌍으로구 성된집합을뜻한다 : A B = { a, b a A, b B}. 메모리는변함없다 : M Mem = Addr fin Val l Addr an index set 의미규칙은 : σ{x x, C 1 }, M C M σ, M let proc f(x) = C 1 in C M σ(f) = x, C l Dom σ σ, M E v σ{x l}, M{l v} C M σ, M f (E) M

76 76 기계중심의언어 프로시져가선언되면프로시져이름의실체는해당명령문과인자이름 이된다. 프로시져호출이일어나면인자에대해서는 let-명령문같은일이벌어진다. 새로운메모리주소를프로시져인자이름으로명명하고그주소에인자로전달할값을저장하고, 프로시져이름이지칭하는명령문을실행한다. 프로시져이름이지칭하는명령문을프로시져몸통이라고부른다. 위의의미정의를보면, 프로시져호출은명령문텍스트가움직이는것과같은효과를가진다. 프로시져몸통명령문이프로시져호출이일어난곳으로끼여들어오는. 이렇게명령문이프로그램안에서움직여다닌다면, 프로시져의몸통명령문안에있는이름들의실체는어떻게결정되야할까? 이름들의실체가프로그램텍스트의위치로결정되야하는데, 텍스트가실행중에옮겨다니는형국이되버렸으니. 예를들어다음의프로그램을생각하자. let x := 0 in let proc inc(n) = x := x+n in let x := 1 in (inc(1); write x) 프로지셔호출 inc(1) 의실행중에몸통명령문 x := x+n에나타나는 x의실체는어느것인가? 첫번째로선언된 x인가? 두번째로선언된 x인가? 위의의미정의에따르면, 두번째로선언된 x이다. 왜냐하면프로시져가호출되어몸통명령문이실행될때의환경은프로시져가호출될때의환경을참조하기때문이다. 프로시져몸통명령문안에있는자유변수free variabl들의실체가그프로시져가어디에서호출되냐에따라서결정된다. 몸통명령문의위치가아니라그프로시져의호출위치에따라.

77 4.3 언어키우기 I: K-- 77 이렇게이름의실체가실행중에결정되는것을동적으로유효범위가정해 진다 dynamic scoping 라고한다 정적으로결정되는유효범위이름의실체가실행전에결정되야하지않을까? 정적유효범위static scoping를유지하고싶다. 프로시져몸통명령문안에있는자유변수free variabl들의실체가몸통명령문의위치에의해서미리결정되야하지않을까? 그프로시져가어디에서호출되냐에따라서실행중에다이나믹하게결정되는것보다는. 그래야프로그램을이해하기쉬워진다. 프로그램을이해하기간단하고쉬운방식이다. 그리고이것이수학에서인류가 2000년이상사용한규칙이기도하다. 이것을위해서는프로시져의의미가인자이름과몸통명령문의쌍으로는부족하다. 그프로시져가정의되는위치에서의환경까지가지고있어야한다 : Procedure = Id Command Env 이렇게되면프로시져정의와호출의의미가아래와같이정의된다 : σ{x x, C 1, σ }, M C M σ, M let proc f(x) = C 1 in C M σ(f) = x, C, σ l Dom σ σ, M E v σ {x l}, M{l v} C M σ, M f (E) M 프로시져호출방법 지금까지는값전달호출 call-by-value 이다 : σ(f) = x, C, σ l Dom σ σ, M E v σ {x l}, M{l v} C M σ, M f (E) M

78 78 기계중심의언어 호출될때인자식 E 의값 v 가프로시져의인자이름 formal parameter 에전달되고 프로시져몸통명령어가실행된다. 그런데, 이름이뜻하는메모리주소를전달해줄방법이있었으면한다. 그 러기위해서는우선, 프로시져호출문의생김새부터구분을해주자. 값전달 호출 call-by-value 인경우와주소전달호출 call-by-reference 인경우를 : C. let proc f(x) = C in C f (E) f <x> 주소전달호출 call-by-reference 의정의는다음과같다 : σ(f) = x, C, σ σ {x σ(y)}, M C M σ, M f <y> M 이렇게되면, 다른이름이같은메모리주소를지칭할수있게된다. 같은 대상을지칭하는다른두개의이름들, 별명 alias 이생기게된다. 별명이많아지면프로그램을이해하기가어려위지지않을까? 특히, 별명들이프로시져호출에의해서실행중에만들어진다. 프로시져 f의인자이름formal parameter이 x라고하면, f <y> 에의해서는 x와 y가별명이되었다가, 또다른호출 f <z> 에의해서는 x와 z가별명이된다. 이런다이나미즘, 혼동스럽다. 이런복잡한상황을지원하는언어는바람직한가?

79 4.3 언어키우기 I: K 재귀호출 의미정의를보면, 재귀호출은불가능했다 : σ(f) = x, C, σ l Dom M σ, M E v σ {x l}, M{l v} C M σ, M f (E) M 몸통명령문안에자신의프로시져이름 f가나타나면자신임을환경environment σ 에서알려줘야한다. 그러나 σ 는프로시져가정의되는위치를감싸는환경이었다. 재귀호출을지원하는의미정의는아래와같다 : σ(f) = x, C, σ l Dom M σ, M E v σ {x l}{f x, C, σ }, M{l v} C M σ, M f (E) M

80 80 기계중심의언어 명령문과식의통합 프로시져호출은명령문이었다. 메모리에반응을일으키는. 프로시져호출의결과로값이계산되게하고싶으면? 메모리를변화시킨후에최종적으로어느값을결과로내놓는식이있으면어떤가? C에서는 return E라는명령문이이역할을한다. 그런데생각해보자. 명령문과식, 두가지가과연다른것들인가? 메모리에값을쓸수있는것과메모리를읽기만하는것. 결과값이없는것과결과값이있는것. 하나로합칠수있다. 식의실행결과는항상어떤값이된다. 그리고식은메모리변화를일으킬수도있다. 식 Expression E skip x := E E ; E if E then E else E while E do E for x := E to E do E read x write E let x := E in E let proc f(x) = E in E f (E) f <x> n (n Z) true false x E + E - E E < E not E 프로그램 P E 그래서프로그래머는더욱간단한언어를가지고더욱자유롭게프로그램하게될것이다. 간단한이유는모든것은식이므로. 자유스러운이유는식과명령문이제한없이섞일수있으므로. 명령문과식, 두가지다른타입의프로그램

81 4.3 언어키우기 I: K-- 81 부품을운용할필요가없다. 의미정의는 σ, M E v, M 을증명하는규칙들로통일된다. 명령문들은의미없는빈값 을계산한다고하자 : v Val = Z + B + { } 실은, 프로그램에서새로운타입의값을다룰수있게하려면, 그언어는그집합의값을만들고사용하는문법을제공해주게된다. 새로운값 을만드는문법은? 이미있는 skip 명령문이그값을만드는식이라고하자. 덩달아서, 이전의모든명령문들이그값을만드는식이라고한것이다. 그리고 를사용하는문법은없다. 불행하게도 은만들어지기만하고사용할데는없는무의미한값이다. σ, M E v, M σ, M E 1 v, M 1 σ{x l}, M 1 {l v} E 2 v 2, M 2 σ, M let x := E 1 in E 2 v 2, M 2 l Dom M σ{x x, E 1, σ }, M C v, M σ, M let proc f(x) = E 1 in E v, M σ, M skip, M σ, M E v, M σ, M x := E v, M {σ(x) v} σ, M E 1 v 1, M 1 σ, M 1 E 2 v 2, M 2 σ, M E 1 ; E 2 v 2, M 2 σ, M E true, M σ, M E 1 v, M σ, M if E then E 1 else E 2 v, M σ, M E false, M σ, M E 2 v, M σ, M if E then E 1 else E 2 v, M

82 82 기계중심의언어 σ, M E 1 false, M σ, M while E 1 do E 2, M σ, M E 1 true, M σ, M E 2 v, M 1 σ, M 1 while E 1 do E 2 v, M 2 σ, M while E 1 do E 2 v, M 2 σ, M E 1 n 1, M σ, M E 2 n 2, M σ, M {σ(x) n 1 + 0} C v 0, M 0. σ, M n2 n 1 1{σ(x) n 1 + (n 2 n 1 )} E 3 v n2 n 1, M n2 n 1 σ, M for x := E 1 to E 2 do E 3, M n2 n 1 n 2 n 1 σ, M E 1 n 1, M σ, M E 2 n 2, M σ, M for x := E 1 to E 2 do E 3, M n 1 > n 2 σ(f) = x, E, σ σ, M E v, M l Dom M σ {x l}{f x, E, σ }, M {l v} E v, M σ, M f (E) v, M σ(f) = x, E, σ σ {x σ(y)}{f x, E, σ }, M E v, M σ, M f <y> v, M σ, M read x n, M{σ(x) n} σ, M E v, M σ, M write E v, M σ, M n n, M σ, M x M(σ(x)), M σ, M E 1 n 1, M 1 σ, M 1 E 2 n 2, M 2 σ, M E 1 + E 2 n 1 + n 2, M 2 σ, M E n, M σ, M - E n, M σ, M E 1 n 1, M 1 σ, M 1 E 2 n 2, M 2 σ, M E 1 < E 2 n 1 < n 2, M 2

83 4.3 언어키우기 I: K-- 83 σ, M E b, M σ, M not E not b, M 메모리관리 K-- 프로그램의실행에대해서생각해보자. 컴퓨터는 K-- 프로그램을자동으로실행해준다. 프로그램을구성하는식의의미정의에따라컴퓨터는어김없이실행할뿐이다. 이때프로그램이소모하는자원은컴퓨터의시간과메모리이다. 컴퓨터의시간은무한하지만메모리는유한하다. 프로그램이한없이컴퓨터메모리를소모할수는없다. 메모리가어디에서소모되는지보자. 프로그램실행중에메모리는 let-식과프로시져호출식의실행을위해하나씩소모된다 : σ, M E 1 v, M 1 σ{x l}, M 1 {l v} E 2 v 2, M 2 σ, M let x := E 1 in E 2 v 2, M 2 l Dom M σ(f) = x, E, σ σ, M E v, M l Dom M σ {x l}{f x, E, σ }, M {l v} E v, M σ, M f (E) v, M let- 식에서선언된이름과프로시져의인자이름을위해서매번새로운메 모리가소모된다. 그리고, 소모되기만한다. 소모되기만한다. 소모되기만한 다. let- 식과프로시져호출이많은횟수반복되게되면언젠가는컴퓨터가메 모리부족으로프로그램실행을못하게된다. 메모리는유한하기때문이다. 따라서메모리는재활용되야한다. 어느메모리가재활용되야하나? 프로 그램실행중에사용한메모리중에서앞으로더이상사용되지않을메모리다. 를. 그런메모리를어떻게알아낼수있나? 앞으로더이상사용안될메모리 K-- 프로그램에서는쉽다. 메모리주소의사용기간이곧그주소의이름 의유효범위이기때문이다. 메모리주소는하나의이름만붙고그이름을통 해야만그메모리주소를사용할수있기때문이다. 따라서이름의유효범위

84 84 기계중심의언어 가끝나면그이름이지칭하는메모리는더이상사용될방법이없다. 따라서 K-- 프로그램에서는이름의유효범위가끝나는곳에서그이름이붙은메모리주소를재활용하면된다. 그곳이어디인가? let-식의마지막이나프로시져몸통 ( 인자이름의유효범위 ) 의마지막이다. 그곳이선언한이름들의유효범위가끝나는곳이다. 그러나, 언어가좀더확장되면, 이렇게간단한메모리재활용garbage collection이간단치않게된다. 메모리주소가프로그램식의결과값으로프로그램의여기저기를흘러다니게되면, 그메모리주소의사용기간은그주소에붙은이름의유효범위와일치하지않게된다. 이런언어에서의메모리재활용garbage collection 문제는 4.4.4절에서다룬다. 4.4 언어키우기 II: K- K--는그럴듯하다. 이름붙일수있는것은메모리주소와프로그램코드. 이름의유효범위scope가있고, 재귀호출recursive call이가능하고, 값전달호출call- by-value과주소전달호출call-by-reference이가능하고. while-식과 for-식으로반복이가능하고 레코드 : 구조가있는데이타, 혹은메모리뭉치 그런데, 리스트list나나무구조tree를만들고사용하는프로그램을짤수있는가? 자동차를만들고사용하는프로그램을짤수있는가? 집합을만들고사용하는프로그램을짤수있겠는가? 할수는있다. 그런구조물들을정수나참 / 거짓으로표현하는방안만정한다면. 그러나, 손쉽게다룰수있도록프로그래밍언어에서지원이되면좋겠다. 기초적인값primitive value( 정수나참 / 거짓 ) 이외의, 구조가있는값compound value를프로그램에서손쉽게다룰수있도록. 기초적인값를보관하는데는메모리주소하나로충분했다. 구조가있는값은여러개의메모리주소가필요하다. 왜냐하면 구조 란관계를가지는것

85 4.4 언어키우기 II: K- 85 이고관계는여러개들을끌어들여표현할수밖에없기때문이다. 구조가있는값을다루는데는메모리뭉치를하나의단위로이름짓고프로그램할수있으면편리할것이다. 메모리뭉치는메모리주소가하나이상모여있는것이다. 그런것들을레코드record라고하자. C에서는 struct라고한다. 그리고그뭉치안에있는각각의메모리주소들도이름이있다. 그러한이름들을레코드필드라고부르자. 참고로, 배열array도메모리뭉치다, 각각의메모리주소들의이름이자연수인. 이제레코드가프로그램에서하나의값이되어자유롭게쓸수있도록할 것이다. 우선레코드라는값을다음과같이정의하자 : r Record = Id fin Addr

86 86 기계중심의언어 한레코드란메모리뭉치들이고뭉치안의각메모리주소가이름이붙은것이 다. 하나의유한함수 ( 테이블 ) 로생각할수있다 : {x 1 l 1,, x n l n }. 이제값들은레코드까지포함하게되고, 메모리는레코드를보관할수있게된 다 : v Val = Z + B + { } + Record M Mem = Addr fin Val 프로그래밍언어에서레코드를만들고사용하는문법이아래와같이제공된 다 : E. {} {x := E, y := E} E.x E.x := E 레코드필드의수 ( 메모리뭉치의메모리수 ) 가 0 이거나 2 개인것만생각해도 충분하다. 의미정의는다음과같다 : σ, M {}, M σ, M E 1 v 1, M 1 σ, M 1 E 2 v 2, M 2 σ, M {x := E 1, y := E 2 } {x l 1, y l 2 }, M 2 {l 1 v 1 }{l 2 v 2 } {l 1, l 2 } Dom M 2 σ, M E r, M σ, M E.x M (r(x)), M σ, M E 1 r, M 1 σ, M 1 E 2 v, M 2 σ, M E 1.x := E 2 v, M 2 {r(x) v} 레코드에이름을붙이고, 레코드의필드가아래와같이사용된다.

87 4.4 언어키우기 II: K- 87 let item := {id := , age := 20} in item.id + item.age 이제는나무가프로그램하기쉽다. 나무의각노드가레코드가된다. 필드 는 left, v, right 이다. 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 )... 위의경우 tree 의유효범위는 let- 식에한정되지만, let- 식의결과로만들 어지는레코드 ( 메모리뭉치 ) 들은프로시져 f 로전달되어사용되게된다. 메모 리재활용 garbage collection 이어려워진다 ( 절 ) 포인터 : 메모리주소를데이타로 지금까지프로그램에서값으로운용되는것들은정수, 참 / 거짓,, 그리고레코드였다 : Val = Z + B + { } + Record

88 88 기계중심의언어 그것들은자유자재로사용된다. 변수에저장되기도하고, 프로시져에전달되기도하고, 프로시져의결과값이될수도있고, 또레코드에저장되기도한다. 프로그램식의계산결과로만들어지는것들이었다. 다른각도에서이야기하면, 값들로자유롭게운용될수있는것들이란, 반드시이름이붙어있을필요가없이계산되는것들이기도하다. 정수마다이름을붙여서써야한다면얼마나귀찮은일인가? 레코드마다이름이있어야한다면? 정수를더할때마다그결과에이름을붙여야만그결과를사용할수있다면? 불편할것이다. 불평은정당할것이다. 그런데, 지금까지항상이름을붙여야만사용할수있는값들이있었다. 두가지였다. 메모리주소와프로그램식 ( 프로시져 ) 이였다. 메모리주소를이름없이도쓸수있게하자. ( 프로시져에마저에도이름을붙일필요가없이자유자재의값이되는방안은 5장에서자연스럽게등장한다.) 즉, 이제는값들중에메모리주소가값이되게해보자 : Val = Z + B + { } + Record + Addr 프로그램에서메모리주소를값으로다룰수있게하려면, 그언어는메모리주 소값을만들고사용하는문법을제공해줘야한다. 아래와같다 : E. malloc E &x &E.x *E *E := E malloc E와 &-식은메모리주소값을만드는식이다. malloc E는새로운메모리주소를할당받아서그시작주소를값으로하는식이다. &-식은메모리주소의이름으로부터그주소를가져오는식이다. *E와 *E := E는메모리주소에저장된값을가져오거나그주소에값을저장하는식이다.

89 4.4 언어키우기 II: K- 89 Exercise 1 레코드는메모리주소뭉치이고, 레코드는값이므로, 레코드를이 용해서메모리주소가값으로여겨지는프로그램을할수는있다. 어떻게? 의미정의는다음과같다. σ, M E n, M σ, M malloc E l, M n > 0, {l, l + 1,, l + n 1} Dom M σ, M &x σ(x), M σ, M E r, M σ, M &E.x r(x), M σ, M E l, M σ, M *E M (l), M σ, M E 1 l, M 1 σ, M 1 E 2 v, M 2 σ, M *E 1 := E 2 v, M 2 {l v} *E 는그자체가식인경우와메모리지정문의왼쪽에있을경우, 의미가 다르다. 변수 x 가지정문의왼쪽이냐오른쪽이냐에따라의미가달라졌듯이. *E 가지정문의왼쪽에있는경우는 E 가뜻하는메모리주소값을뜻한다. 항 상메모리주소여야한다. *E 가지정문의오른쪽에있는경우는 E 가뜻하는 메모리주소에보관되어있는값을뜻한다. (C 언어가이렇다.) 그래서아래프로그램을실행하면 x 가가르키는주소의다음번주소에는 3 이보관된다. let x := malloc(2) in *x := 1; *(x+1) := *x + 2