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

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

2

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

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

차례 1 장소개 9 1.1 프로그래밍언어는미개하다.................... 10 1.2 프로그래밍언어의위치....................... 11 2 장 기본기 15 2.1 귀납법inductive definition........................ 15 2.1.1 집합의정의.......................... 15 2.1.2 증명의방법.......................... 24 2.2 형식논리formal logic......................... 28 2.2.1 모양과뜻........................... 28 2.2.2 추론규칙........................... 30 2.2.3 안전한혹은완전한..................... 32 3 장 모양과뜻 35 3.1 문법구조syntax............................ 35 3.1.1 요약된혹은구체적인.................... 37 3.2 의미구조semantics........................... 40 3.2.1 과정을드러내는....................... 40 3.2.2 궁극을드러내는....................... 50 4 장기계중심의언어 59 4.1 주어진기계.............................. 59

6 차례 4.2 언어키우기 0: K---........................ 61 4.2.1 변수 : 메모리주소에이름붙이기............. 61 4.2.2 이름의두가지의미..................... 65 4.2.3 이름의유효범위....................... 66 4.2.4 환경.............................. 68 4.2.5 자유로운혹은묶여있는................... 71 4.2.6 설탕구조........................... 72 4.3 언어키우기 I: K--.......................... 73 4.3.1 프로시져 : 명령문에이름붙이기.............. 73 4.3.2 이름의유효범위....................... 75 4.3.3 프로시져호출방법..................... 77 4.3.4 재귀호출........................... 78 4.3.5 명령문과식의통합..................... 79 4.3.6 메모리관리.......................... 83 4.4 언어키우기 II: K-.......................... 84 4.4.1 레코드 : 구조가있는데이타, 혹은메모리뭉치...... 84 4.4.2 포인터 : 메모리주소를데이타로.............. 87 4.4.3 같은값............................ 89 4.4.4 메모리관리.......................... 90 4.5 언어키우기 III: K.......................... 97 4.5.1 실행되서는않될프로그램들................ 97 4.5.2 오류검증의문제....................... 98 4.5.3 타입시스템 : 소개...................... 102 4.5.4 K = K- + 타입시스템................... 103 4.5.5 K- 타입시스템의논리적문제............... 109 4.5.6 K- 타입시스템의구현문제................ 115 4.5.7 이름공간, 같은타입..................... 120 4.6 정리.................................. 121

차례 7 5 장 값중심의언어 123 5.1 언어의모델.............................. 123 5.1.1 람다계산법Lambda Calculus.................. 125 5.1.2 람다로프로그램하기..................... 132 5.2 언어키우기 0: M0......................... 135 5.2.1 소극적인실행lazy evaluation과적극적인실행eager evaluation 136 5.2.2 시작언어 : 값은오직함수................. 138 5.3 언어키우기 I: M1.......................... 140 5.3.1 다른값 : 정수, 참 / 거짓................... 140 5.4 언어키우기 II: M2.......................... 142 5.4.1 구조가있는값 : 쌍pair.................... 142 5.5 언어키우기 III: M3......................... 145 5.5.1 메모리주소값 : 명령형언어의모습............ 145 5.6 오류검증의문제........................... 147 5.6.1 정적타입시스템static type system.............. 149 5.6.2 형식논리시스템formal logic 리뷰.............. 151 5.7 단순타입시스템simple type system.................. 154 5.7.1 단순타입추론규칙..................... 155 5.7.2 추론규칙의안전성..................... 159 5.7.3 추론규칙의구현....................... 162 5.7.4 안전한그러나경직된.................... 172 5.7.5 M3로확장하기........................ 174 5.8 다형타입시스템polymorphic type system............... 177 5.8.1 다형타입추론규칙..................... 181 5.8.2 추론규칙의안전성..................... 187 5.8.3 추론규칙의구현....................... 187 5.8.4 M3로확장하기........................ 188 5.9 정리.................................. 192

8 차례 6 장 번역과실행 195 6.1 프로그램입력............................ 195 6.2 프로그램실행............................ 196 6.2.1 실행기interpreter........................ 196 6.2.2 번역기compiler......................... 197 6.2.3 자가발전........................... 198 6.3 번역 : 불변성질invariant 유지하기.................. 199 6.4 가상의기계virtual machine...................... 202

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

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

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

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

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

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

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

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

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

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

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 기본기 조물이다. 그래프들의집합도다음세개의규납규칙들로정의된다 : 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

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 2.1.1.3 그집합은이렇게만든다 그런데, 위의정의는명확하지만한가지가의아하다. 규칙들이정의하는집합이무엇인지정의하고있지만, 그집합을만드는방법을알려주고있지않다. (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 기본기 라고하고 φ 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} 들의합집합.

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

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번째만들어지는원소들만으로구성되므로. 2.1.2.1 귀납규칙들에대한것으로이증명기술을귀납규칙들에대한것으로다시이야기하면, 우선, 첫째번에만들어지는원소들은 Φ에있는규칙들중에는공집합을전제로가지고있는규칙들 (, x) 가만드는 x들이다. 고로, 그러한 x들에대해서증명하는것이첫째번의원소들에대한증명이된다. 그다음, 그이상째번에만들어지는원소들은 Φ에있는규칙들중에서공집합이아닌전제 (X ) 를가지고있는규칙들 (X, x) 이만드는 x들이다. x가 i째번에만들어지는원소라면 X에있는원소들은그이전번에만들어진원소들이다. 따라서 X에나타나는원소들에대해서사실이라는가정하에 x에대해서사실인지를증명한다. 이렇게위의두가지를증명하면, 모든 i째번에만들어지는원소들 (Φ가정의하는모든원소들 ) 에대해서증명한것이된다.

26 기본기 2.1.2.2 일반적으로 두개로쪼개지는위와같은증명을하나로이야기하면, 귀납법증명은다음을 증명하면된다 : 모든 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에대해서, 0 + 1 + 2 + + n = n(n + 1)/2인지를증명하자. 모든자연수는귀납규칙 n 0 n + 1를유한번적용해서만들어지는원소들의모임이다. 첫째번에만들어지는원소는 0이다. n이 0일때위의등호가성립하는지증명한다. 그다음은 i 이전번에만들어지는자연수에대해서위의등호가성립한다고가정하고, i째번에만들어지는자연수에대해서사실인지증명한다. i째번에만들어지는자연수를 n + 1이라고하자. 그이전번에만들어진자연수들중에는 n이있다. 그러면, 0 + + n + (n + 1) = n(n + 1)/2 + (n + 1) = (n + 1)(n + 2)/2 이므로위의등식이성립한다. 귀납규칙들을따라증명하면, 0일때사실인지증명하고, n일때사실이라는가정하에 n + 1일때사실인지증명하면된다.

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

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

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 기본기 Γ {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) 2.2.3 안전한혹은완전한 위의규칙들이만들어내는 f의 f는모두참인가? 반대로, 참인식들은모두위의증명규칙들을통해서 f 꼴로만들어지는가?

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

34 기본기

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

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

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

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

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

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

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 의의미는 메모리에대해서다음과같은증

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

44 모양과뜻 구조적 이라고부르는다른이유는의미규칙들이한집합 ( 프로그램과 의미장치들간의관계쌍들의집합 ) 을귀납적으로정의하는방식이고, 그 귀납이프로그램이나의미장치들의구조를따라흐르기때문이다. 관계형 이라고도하는이유는위의추론규칙들이관계된짝들의집합을정의하는귀납적인방법으로도바라볼수있기때문이다. 관계된짝들이란 M C M 인 M, C, M 와 M E v인 M, E, v 들이다. 위의규칙들에의해서그러한관계를맺을수있는 M, C, M 과 M, E, v들이모아진다. 3.2.1.2 작은보폭으로 프로그램의실행을작은보폭으로정의해보자 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 )

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 이라는 프로그램이외의의미장치없이. 예를들어, 간단한정수식프로그램들의의미는프로그램을다시쓰는과정 으로정의된다 : 1 + 2 + 3 다시쓰면 3 + 3 다시쓰면 6. 프로그램이외에다른 장치가사용되지않는다. 3.2.1.3 문맥구조를통해서프로그램실행을프로그램을다시쓰는과정으로정의해보자. 예를들어, 1 + 2 + 3 다시쓰면 3 + 3 다시쓰면 6. 이렇게프로그램을다시써가는과정이프로그램의실행이라고볼수있다transition semantics. 두가지를정의해야한다 : 프로그램의어느부분을다시써야 ( 계산해야 ) 하는가? 다시써야할부분을무엇으로다시써야하는가? 프로그램의어느부분을다시써야 ( 계산해야 ) 하는가? 이질문에대한답은 실행문맥 evaluation context에의해서정의된다. 실행문맥의정의에따라서현재의프로그램을구성하다보면, 다시써야할부분 ( 계산해야할속부분 ) 이결정된다. 재미있는것은그정의가문법적으로가능하다는것이다.

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.

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

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 모양과뜻 그리고, 기계작동과정의한스텝도다음과같이정의된다 : 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를구현할때. 프로그래밍언어의성질을궁리하거나그언어로짜여진프로그램들의관심있는성질을분석할때에사용하는의미구조로사용되는예는드물다. 가상의기계는대개가이와같은분석에서는필요하지않은디테일 ( 기계의볼트넛트들 ) 을드러내기때문이다. 3.2.2 궁극을드러내는 궁극을드러내는의미구조denotational semantics는프로그램의의미를전통적인수학의세계에서정의한다. 프로그램이뜻하는바를수학의물건으로정의하는것이다. 영어 denotational 을 궁극을드러내는 이라고번역한이유는? 지칭하

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 모양과뜻 사용하는변수이름이다. 그리고, 이런물건들이어느집합에소속되는지를정의하자. 그러한집합을의미공간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 ]. 3.2.2.1 조립식일수있는이유 : 의미공간이론 domain theory 그런데, 이렇게부품들의의미로전체의의미를구성하는상식적인방식이일

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 모양과뜻 성질을만족하는집합이다. 그래서, 모든프로그램의의미방정식들에쓰이는것들은모두어떤 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라고불리기도한다. 3.2.2.2 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을취하고함수를적용한결과가함수를그체인의원소들에각각취하고

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 모양과뜻 이때, 최소의원소는 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)

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 모양과뜻 에해당하게되므로, 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 ] 를가지고조립되어있 다.

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

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

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

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의원소들인지를정하자. 값은정수거나참 / 거짓이다. 따라서값의집합은정수집합이거나참 / 거짓집합니다. 메모리는주소에서값으로가는테이블일것이다. 테이블은수학적으로는하나의함수이다. 정의구역은메모리주소, 공변역은값. 특히정의구역은메모리주소집합중에서유한한집합이되겠다. 주소는프로그래머가사용하는이름들의집합으로정의하자.

4.2 언어키우기 0: K--- 63 그래서의미정의에사용할의미공간 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 기계중심의언어 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

4.2 언어키우기 0: K--- 65 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 이름이곧메모리주소다. 새메모리주소를사용하고자하면다른이름을 사용하면된다. 입출력문의의미를정한규칙이특이하다. 입력문은외부에서임의의정수 를받아서지정한메모리주소에보관하는것이다. 외부세계에묻고입력받는 과정을드러낼필요는없다. 출력도외부세계에계산한값을보여주는과정을 드러낼필요는없다. 의미를결정하는데필요한내용들은아니므로. 4.2.2 이름의두가지의미 이름안에는무엇이있나? 이름이의미하는것은무엇인가? 혼동되게도 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 기계중심의언어 그메모리주소의값을뜻할때는이름앞에! 표시를하도록하는것이다. 예를 들어, K--- 의 x := x + 1 는 x :=!x + 1 로쓰도록하는것이다. 그런데, 이렇게하면프로그래머가조금불편해하지 않을까? 프로그램식에나타나는모든이름앞에! 를붙여야하므로 x + y + 1 대신에!x +!y + 1. 이러한편리함이언어가복잡해지면서는프로그램을이해하기어렵게만드는눈엣가시가된다. K---를키워가면서살펴볼것이다. 이름을기계중심의언어에서는변수variable라고도부른다. 이름이의미하는메모리주소의값이변할수있으므로. 프로그램실행중에변수가의미하는주소에새로운값을써넣을수있으므로. 4.2.3 이름의유효범위 프로그래머가메모리주소에이름을짓기시작하면서문제가생긴다. 같은이름을다른용도로도쓰고싶다면? 즉, 같은이름을다른메모리주소를위해재사용하고싶다면? 이것은자연스러운요구이다. 항상다른이름을고안해야한다면프로그래머의불편은클것이다. 이세상에태어나는모든사람들의이름이모두달라야한다면이름짓는것이얼마나골치아프겠는가? 위의 K---언어에서는같은이름은같은메모리주소를뜻한다. 다른메모리주소를위해서는다른이름을사용해야한다. 같은이름을다른메모리주소의이름으로사용할수가없다. 프로그램에서사용하는메모리주소가매우많다면, 얼마나많은다른이름을고안해야할까? 같은이름을다른메모리주소를위해서쓸수는없을까? 이름을재활용할수는없을까?

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

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

4.2 언어키우기 0: K--- 69 환경은이름의실체 ( 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 기계중심의언어 같은이름이다른주소를지칭할수있다. 이름의재활용, 동명이인. 그러나거꾸로는아니다. 다른이름이같은주소를지칭할수는없다. 같은대상을지칭하는다른이름은가능하지않다. 별명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}

4.2 언어키우기 0: K--- 71 σ, 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 4.2.5 자유로운혹은묶여있는 프로그램에서사용되는이름의실체를찾을수없다면그이름은자유로운이 름 free variable 이라고한다. 자유로운이름을가지고있는프로그램의의미는정 의될수없다. 프로그램내에서는모든이름들은 let-명령문의선언으로정의되어있어야한다. 이름의실체가정의된정상적인경우를묶여있는이름bound variable이라고한다.

72 기계중심의언어 전체프로그램이아니라제한된지역을기준으로자유로운이름과묶여있 는이름이이야기되기도한다. 프로그램텍스트의어느지역만한정해서보면 서, 그안에서사용되는이름이자유롭거나묶여있다고판단하기도한다. 4.2.6 설탕구조 프로그래밍언어는꼭필요한것만으로구성되어있지는않다. 위의 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)

4.3 언어키우기 0: K--- 73 단, 위와같이 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 기계중심의언어 4.3 언어키우기 I: K-- 4.3.1 프로시져 : 명령문에이름붙이기 메모리주소뿐아니라, 명령문에도이름을붙일수있도록하자. 그래서그명령문을반복해서쓰지않고도이름만으로그명령문을수행할수있도록. 조금더나아가, 이름붙은명령문들을일반화해서인자에의해서조금씩다른일을할수있도록하자. 예를들어, 변수 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이확장된다. 이름의실체는

4.3 언어키우기 I: K-- 75 메모리주소뿐아니라프로시져까지포함된다 : σ Env = Id fin Addr + Procedure 그러나프로지져의실체 Procedure 가무엇이되야하는지에따라서프로시져 의호출에관한의미가전혀달라질수있다. 4.3.2 이름의유효범위 4.3.2.1 동적으로결정되는유효범위 우선 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 기계중심의언어 프로시져가선언되면프로시져이름의실체는해당명령문과인자이름 이된다. 프로시져호출이일어나면인자에대해서는 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들의실체가그프로시져가어디에서호출되냐에따라서결정된다. 몸통명령문의위치가아니라그프로시져의호출위치에따라.

4.3 언어키우기 I: K-- 77 이렇게이름의실체가실행중에결정되는것을동적으로유효범위가정해 진다 dynamic scoping 라고한다. 4.3.2.2 정적으로결정되는유효범위이름의실체가실행전에결정되야하지않을까? 정적유효범위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 4.3.3 프로시져호출방법 지금까지는값전달호출 call-by-value 이다 : σ(f) = x, C, σ l Dom σ σ, M E v σ {x l}, M{l v} C M σ, M f (E) M

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가별명이된다. 이런다이나미즘, 혼동스럽다. 이런복잡한상황을지원하는언어는바람직한가?

4.3 언어키우기 I: K-- 79 4.3.4 재귀호출 의미정의를보면, 재귀호출은불가능했다 : σ(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 기계중심의언어 4.3.5 명령문과식의통합 프로시져호출은명령문이었다. 메모리에반응을일으키는. 프로시져호출의결과로값이계산되게하고싶으면? 메모리를변화시킨후에최종적으로어느값을결과로내놓는식이있으면어떤가? 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 그래서프로그래머는더욱간단한언어를가지고더욱자유롭게프로그램하게될것이다. 간단한이유는모든것은식이므로. 자유스러운이유는식과명령문이제한없이섞일수있으므로. 명령문과식, 두가지다른타입의프로그램

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 기계중심의언어 σ, 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

4.3 언어키우기 I: K-- 83 σ, M E b, M σ, M not E not b, M 4.3.6 메모리관리 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 기계중심의언어 가끝나면그이름이지칭하는메모리는더이상사용될방법이없다. 따라서 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-식으로반복이가능하고. 4.4.1 레코드 : 구조가있는데이타, 혹은메모리뭉치 그런데, 리스트list나나무구조tree를만들고사용하는프로그램을짤수있는가? 자동차를만들고사용하는프로그램을짤수있는가? 집합을만들고사용하는프로그램을짤수있겠는가? 할수는있다. 그런구조물들을정수나참 / 거짓으로표현하는방안만정한다면. 그러나, 손쉽게다룰수있도록프로그래밍언어에서지원이되면좋겠다. 기초적인값primitive value( 정수나참 / 거짓 ) 이외의, 구조가있는값compound value를프로그램에서손쉽게다룰수있도록. 기초적인값를보관하는데는메모리주소하나로충분했다. 구조가있는값은여러개의메모리주소가필요하다. 왜냐하면 구조 란관계를가지는것

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

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} 레코드에이름을붙이고, 레코드의필드가아래와같이사용된다.

4.4 언어키우기 II: K- 87 let item := {id := 200012, 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 이어려워진다 ( 4.4.4 절 ). 4.4.2 포인터 : 메모리주소를데이타로 지금까지프로그램에서값으로운용되는것들은정수, 참 / 거짓,, 그리고레코드였다 : Val = Z + B + { } + Record

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

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

90 기계중심의언어 4.4.3 같은값 이제프로그램에서계산되는값들은다양한종류가가능하게되었다 : v Val = Z + B + { } + Record + Addr n Z b B r Record l Addr 프로그램식중에값의동치여부를계산하는식을추가하고 E. E = E 그의미를정의하자. 같은종류 ( 타입 ) 의값들끼리일치하면참이고, 그이외는 모두거짓을낸다고정의한다 : σ, M E 1 v 1, M 1 σ, M 1 E 2 v 2, M 2 v 1 = v 2 σ, M E 1 = E 2 true, M 2 σ, M E 1 v 1, M 1 σ, M 1 E 2 v 2, M 2 v 1 v 2 σ, M E 1 = E 2 false, M 2 n = n b = b = l = l Dom r 1 = Dom r 2 x Dom r 1 : r 1 (x) = r 2 (x) r 1 = r 2 otherwise v 1 v 2

4.4 언어키우기 II: K- 91 4.4.4 메모리관리 이제 K- 프로그램을실행할때컴퓨터의유한한메모리를어떻게재활용할수있는지를생각해보자. 이제프로그램실행중에메모리를소모하는경우는 let-식과프로시져호출식뿐아니라레코드식과메모리할당식들이되었다. 그리고메모리주소가값으로사용될수있기때문에, 그주소들의사용기간이어떻게되는지알방법이쉽지가않다. 예전의 K-- 언어의경우는메모리재활용garbage collection이쉬었다. 메모리주소의사용기간이그주소에붙은이름의유효범위와일치했기때문이다. K-- 프로그램을실행하면서이름의유효범위가끝나는시점에서그이름이붙은메모리를컴퓨터가재활용하면되었다. K-에서는쉽지가않다. 어떻게해야할까? 4.4.4.1 수동메모리재활용해결을미루는쉬운방법이있다. 메모리재활용을프로그래머에게맡기는것이다. 프로그래머의책임으로. 그래서프로그래밍언어에메모리재활용명령문을제공하는것이다 (C가이렇다 ): E. free E free E 식의의미를정의해보자. 식 E 는메모리주소를계산한다. 그주소는 반드시할당받은메모리주소이어야한다. 메모리뭉치를재활용하려면뭉치 에포함된모든주소를재활용해야한다. 엄밀하게정의하면다음과같다 : σ, M E l, M σ, M free E, M l Dom M 위의정의에서이상한것이있다. 메모리재활용효과가표현되지않았다.

92 기계중심의언어 메모리는그대로다. 그래도괜찮은가? 의미정의에서메모리재활용효과가표현되지않아도충분하다. 메모리재활용은프로그래밍언어의의미바깥의일이다. 메모리재활용은유한한메모리를가진컴퓨터가 K- 프로그램을실행하게되서생기는문제다. 의미정의에명시된메모리모델대로 ( 의미정의대로 ) 구현하기위해서해결해야하는문제인것이다. 의미정의에는메모리재활용에대해서명시할필요는없다. 의미정의의목적은프로그램의의미를우리가필요로하는디테일의정도에서혼동이없게정의하는것이다. 마치요리책과같다. 자장면의요리법을명시하고있다. 그러나필요이상의디테일까지는명시하지않는다. 돼지고기를구하기위해서돈은어떻게벌수있는지, 센불을구하려면어디로가야하는지, 등은명시하지않는다. K-의의미정의로부터메모리관리에대해알수있는사실들은 : 새메모리가필요할때 (let-식, 프로시져호출, 레코드식, malloc-식 ) 새로운메모리는항상거기에있다. 항상필요한메모리는있어야한다. 메모리주소에저장된데이타가없을때, 그주소를접근하는식은의미가없다. 예를들어 let x := malloc(1) in *x 는의미가없다. *x 식의의미를정의할수없기때문이다. 메모리할당이일어났어도식 x가계산하는메모리주소는어떤값도아직보관하고있지는않다. 의미정의에따르면, 그메모리주소는아직메모리의정의구역에없다. 따라서식 *x의의미인그주소의메모리이미지는정의되지않는다. 마지막으로, 할당된메모리들은서로에게서서로에게도달할수있는방법이없다. 할당받은주소로부터몇발자국을움직여서별도로할당받은다른메모리에도달할수있는방법이없다.

4.4 언어키우기 II: K- 93 이게 C 와다른점이기도하다. C 에서는기준주소에서임의의보폭으 로떨어진메모리주소를접근하는것이가능하기때문이다. 아무튼, 메모리재활용을프로그래머에게미루는것은바람직한가? 어쩔 수없는선택인듯하다. 언어가이미복잡해질대로복잡해졌고, 메모리재활 용을자동으로할수있는방안이오리무중이므로. 그러나, 프로그래머가신경쓰는것은많아졌다. 프로그램의논리적인흐름만이아니다. 유한한메모리를가진컴퓨터가자신의프로그램을실행하게된다는조건을항상생각해야한다. 그래서적절히재활용명령문을프로그램의적절한위치에넣어줘야한다. 소비한각각의메모리주소마다. 좋은가? 프로그래머가자신의프로그램이소모하는메모리의사용기간을 제일잘알수있는가? 그런가? C 프로그래밍의경험이지난 20년넘게쌓이면서, 그답은 아니다 이다. 프로그래머가가장많이하는실수가메모리재활용garbage collection 오류이다. 메모리관리를프로그래머에게맡기면서 C 프로그램의가장골치아픈오류가메모리재활용이되었다. 그오류는두가지이다. 재활용지점을너무늦게잡는오류와너무빨리잡는오류이다. 재활용이너무늦게되면자칫컴퓨터의메모리자원이고갈될수있다. 프로그램은계속메모리를소모할터이고메모리재활용이제때되지않는다면필요한메모리가고갈될것이다. 재활용이너무빨리되면사용중인메모리가용도변경이되버리는것이다. 재활용이너무늦게되는오류를메모리누수 memory leak 오류라고한다. 너 무빨리되는오류를메모리도난 dangling pointer 오류라고한다.

94 기계중심의언어 4.4.4.2 자동메모리재활용 메모리재활용을프로그래머가제대로하기에는너무어렵다. 프로그래머에게맡기면서소프트웨어의심각한오류가쉽게나타났다. 메모리누수memory leak와메모리도난dangling pointer이다. 자동으로메모리재활용이되었으면한다. 프로그램실행은계속메모리를소모한다. 메모리소모량이어느수위에오르면, 실행을잠시멈춘다. 그리고메모리를재활용한다. 이제컴퓨터의메모리자원이풍부해졌다. 멈춘프로그램의실행을재개한다. 가능할까? 이과정을또다른소프트웨어로자동화하는것이가능할까? 프로그램을멈추고, 그프로그램이사용했지만앞으론사용하지않을메모리를찾아서재활용해야한다. 이것이가능할까? 미래를여행하는타임머신을만들수있을까?

4.4 언어키우기 II: K- 95 그런타임머신 ( 프로그램 ) 은만들수없다. 디지탈컴퓨터의한계이다. 좀더정확하게이야기하면, 프로그램의미래에사용되지않을메모리를정확하게골라내서모두재활용하는프로그램은만들수없다. 뭐가어려운걸까? 정확하게모두 가어렵다. 앞으로사용않될메모리를모두빠뜨림없이재활용해야하고, 그렇지않은것은고스란히남기고. 이게불가능하다. 그런프로그램이불가능하다는것을어떻게확신하는가? 그런프로그램이있다면, 그프로그램을이용해서, 불가능undecidable하다고증명된멈춰요문제Halting Problem를푸는프로그램을짤수있기때문이다. 불가능하다고증명된것을가능하게만들수가있는가? 그럴수는없다. 멈춰요문제Halting Problem를푸는프로그램이불가능하다는증명은간단하다. 다음과같다 : 그러한프로그램이존재한다고하자. 그러면모순이다. 그러한프로그램은 H(p) 라고하자. 프로그램 p를받아서 p가유한시간에끝나는프로그램이면 true, 그렇지않으면 false를낸다. 그프로그램 H를가지고다음과같은모순된함수 f를정의할수있게된다 : 이다. function f() = if H(f) then (while true skip) else skip f() 는끝나는가? 끝난다면안끝나야한다. 안끝난다면끝나야한다. 모순 정확한메모리재활용이불가능한이유는, 미래에사용않될메모리를정 확하게빠뜨리지않고골라내는프로그램 G 가있다면, 멈춰요문제 Halting Problem 를해결하는프로그램 H(p) 를다음과같이작성할수있게된다 : 입력된프 로그램 p 를다음과같이 let x := malloc() in p; x 고친다. x 는 p 에서사용되지않는이름이라고하자. 이렇게고쳐진플로그램 을실행시킨후, let- 몸통식의 p 가시작되기직전에 G 를실행시킨다. 그결과

96 기계중심의언어 에 x가가지고있는메모리주소가포함되었다면, p는끝나는프로그램이고, 그렇지않다면 p는끝나지않는프로그램이다. 그러나희망은있다. 모두정확히재활용해주는프로그램은불가능하지만, 조금이라도재활용해주는프로그램은만들수있다. 몇개는빠뜨릴수있지만, 대부분은재활용해주는프로그램을만들수있다. 자동메모리재활용기garbage collector의원리는이렇다 : 원칙 : 프로그램의진행을멈추고나서, 지금까지할당된메모리중에서 미래에사용할수있는메모리를제외하고나머지는모두재활용해야한 다. 사실 : 재활용을완전하게 ( 빠뜨리지않고 ) 할수있는방법은없다. 있다 면그런재활용기를이용해서멈춰요문제 Halting Problem 를풀수있기때 문이다. 양보 : 그러나재활용을안전하게는 ( 빠뜨리는것은있으나 ) 할수있는방 법은있다. 뭔고하니, 앞으로실행할식인 E만있다고하자. 식 E의현재환경environment으로부터현재의메모리를통해다다를수있는모든주소들은앞으로 E를실행중에다시사용될수있다. 이것들만빼고재활용하자. 즉, 그렇게해서다다를수없는메모리주소들은, 과거에할당되어서사용되었으나앞으로의 E를실행하는데는사용되지않을것이분명하므로, 재활용해도된다. 모든현대언어들의메모리재활용기garbage collector는위의방식으로구현되어있다. (Java, ML, Scheme, Haskell, C#, Prolog, etc.) 메모리재활용기구현알고리즘은대표적으로두가지가있다 :

4.5 언어키우기 II: K- 97 하나의딜레마가있다. 메모리재활용기들이실행되는데에도메모리가필요하다. 메모리부족으로재활용을하는것인데, 그러려면메모리가필요하다. 프로그램실행중에메모리에만들어진구조물들 ( 그래프graph) 을모두따라가면서앞으로사용될수있는메모리주소들을모으게된다. 그런데, 그래프를누비고다니는알고리즘depth-first-, breath-first-traversal algorithms들은메모리를소모한다. 그래프의가장긴경로만큼의스택stack이필요하다. 메모리가없어서메모리재활용기를돌리는것인데, 메모리가필요하다니. 메모리를소모하지않는그래프를누비는알고리즘graph traversal algorithms이있어야한다. 가능할까? 스택없이가능한알고리즘이있다.

98 기계중심의언어 4.5 언어키우기 III: K 4.5.1 실행되서는않될프로그램들 K-는그럴듯한언어이지만, 현재모든프로그래밍언어에공통인문제를가지고있다. 제대로돌수없는프로그램을쉽게만들수있다는것이다. 프로그램이문법은틀린곳이없지만오류로실행될수없는프로그램들. 프로그램만드는방법을충실히따라서제대로생긴프로그램을만들기는쉽다. 그런데, 그중에는실행될수없는프로그램들이많다. 실행을더이상진행할수없는프로그램들이많다. 레코드의필드이름들이항상제대로접근되나. 함수호출의결과가분별력있게사용되는가. 함수의인자값이그함수가바라는값들이흘러드는가? 제대로생긴 ( 문법에맞는 ) K-프로그램들중에서제대로실행될수있는프로그램은일부분에불과하다. 제대로실행될수있는 프로그램이란우리의의미규칙에따라서의미가정의될수있는프로그램이다.

4.5 언어키우기 III: K 99 4.5.2 오류검증의문제 주어진 K- 프로그램이제대로실행될지를미리확인할수있는기술이없을까? 미리검증해야만한다. 프로그램소스를컴퓨터가실행시키기전에. 소프트웨어를팔고나서오류를수정해야할까? 로봇에내장된소프트웨어가실행중에오류로무쇠팔을갑자기휘두르게된다면? 소프트웨어가자체로상품인경우는말할것도없고, 모든전자기계제품들의경쟁력중에서내장된소프트웨어의신뢰도가차지하는비중은적어도제품디자인만큼은될것이다. 다른분야는우리보다훨씬앞서있다. 제대로작동할지를미리검증할수없는기계설계는없다. 제대로서있을지를미리검증할수없는건축설계는없다. 인공물들이자연세계에서문제없이작동할지를미리엄밀하게분석하는수학적기술들은잘발달해왔다. 뉴튼역학, 미적분방정식, 통계역학등등이그러한기술들일것이다.

100 기계중심의언어 소프트웨어라는인공물에대해서는어떠한가? 작성한소프트웨어가제대로실행될지를미리엄밀하게확인해주는기술들은있는가? 소프트웨어오류를소스만을보고미리자동으로찾아주는기술들. 이기술을향한연구들이소프트웨어기술의발달과정의중요축이었다. 최종목표는소프트웨어가오류없이작동할지를실행전에자동으로검증하는기술을이룩하는것이다. 소프트웨어의오류를자동으로찾아주는기술이다. 오류가없다면오류가없다고확인해주는기술이다. 소프트웨어가생각대로 ( 기획한대로 ) 구현되었는지, 그소프트웨어가작동하기전에엄밀하고안전하게자동으로확인할수있는기술. 이축을따라프로그래밍언어에서는어떤성과를내었는가? 프로그래밍언어가어떻게디자인되면이문제가어디까지해결될수있을까? 프로그래밍언어분야에서는이시급한문제에어떤답을내놓고있나? 그수준은현재어느정도인가? 4.5.2.1 오류검증기술의발전과정프로그래밍언어분야를돌이켜보면, 소프트웨어오류를자동으로찾는기술은세박자의호흡만에한발전진하는형태였다. 첫번째호흡에서는우리가확인할수있는오류의한계를정확하게정의하고, 두번째호흡에서는정의한오류의존재를찾는방법을고안하며, 세번째호흡에서는그방법을컴퓨터가자동으로실행할수있도록소프트웨어로만들어낸다. 이때, 각호흡마다애매하고허술한구석이없을때에만비로소한발짝의전진이있게된다. 오류의정의는모호하지않아야하고, 고안된방법은프로그램이그렇게정의된오류를품고있다면반드시찾아낼수있어야하고, 그방법을구현한소프트웨어는그방법그대로충실히구현되어야한다. 반드시 와 충실히 라는것은엄밀한증명과정을거친다는뜻이다. 이세박자호흡을반복하면서확인할수있는소프트웨어오류의정의는기술발전이진행되면서점점정교해진다. 첫세대에서는비교적쉬운소프트웨어오류들을확인해주는기술이만들어지고, 두번째세대에서는그보다정

4.5 언어키우기 III: K 101 교한오류들을확인해주는기술이만들어지고, 세번째세대에서는더욱더정교한오류들을확인해주는기술이만들어지고... 이렇게하면서궁극적으로는, 소프트웨어가생각대로작동할지를자동으로확인해주는소프트웨어기술을달성해가는것이다. 이러한과정을밟으며소프트웨어기술이전진한횟수는이제겨우두발짝이다. 1세대기술 : 문법검증기술. 1970년대에달성된첫발짝은, 생긴게잘못된프로그램을자동으로찾아내는기술이다. 프로그램이제대로작동하려면우선프로그램의생긴것이제대로되야한다. 이때오류는프로그램의생김새가틀린것이라고정의된경우고, 이러한오류를정확히자동으로찾아주는기술이달성되었다. 정확히찾아준다는뜻은, 안전하고sound 빠뜨림없다는complete 뜻이다. 멀쩡한프로그램을기형이라고진단하는경우 ( 빠뜨리는경우 ) 도없고, 기형인프로그램을멀쩡하다고하는경우 ( 믿을수없는경우 ) 도없다는뜻이다. 이기술을 1세대오류잡는기술이라고하자. 이기술을문법검증기술 (parsing) 이라고하고, 완전히완성되어오늘날의프로그래머가프로그램을짜면서늘상아무렇지도않게사용할만큼관심밖으로사라져버린성숙한기술이다. 그러나이오류잡는기술이겨우 1세대인까닭은, 생긴건멀쩡한데생각대로돌아가지않는소프트웨어에는속수무책인기술이기때문이다. 겉모습의오류뿐이아닌, 속내용 ( 논리 ) 의오류까지자동으로찾아주는기술이필요했다. 2세대기술 : 타입검증기술. 1990년대에빛을보기시작한두번째기술은, 타입검증type checking이라는기술이다. 제 2세대오류잡는기술이라고할수있다. 이때오류의정의는겉모양이틀린프로그램만이아니고, 속내용이잘못될수있는경우

102 기계중심의언어 까지를포함하게된다. 여기서잘못된속내용이란, 프로그램이실행중에잘못된값이잘못된계산과정에휩쓸리는경우로정의된다. 프로그램의실행은일종의계산인데, 그계산중에는분별있는일들이일어난다. 더하기에는숫자만들어와야한다든지, 결혼하기라는계산에는남자와여자가한쌍으로있어야한다던지, 수력발전하기에는우라늄대신에물이있어야한다던지. 이렇게분별있게값들이소통되야하는데, 그렇지않은경우를타입에맞지않다고한다. 이러한경우가발생하면프로그램의진행은생각대로흐르지못하고급기야는값작스럽게멈추고만다. 휘발유가공급되야할전투기의엔진에물이새어들어비행중에추락해버리듯이. 프로그램에서타입에맞지않는계산이실행중에발생할지를미리검증하는방법이바로타입검증이다. 이성과는프로그래밍언어를연구하는분야에서달성되었는데, 프로그램의안전한타입검증은그프로그래밍언어가제대로디자인된경우에만가능하다. ( 대표적인언어가 ML, OCaml, Haskell등이다.) 안전한타입검증을갖춘프로그래밍언어기술은아직은문법검증기술만큼모든프로그래머들이늘상사용하는기술로널리퍼지지는않았다. 그러나그런타입검증기술은앞으로모든소프트웨어개발자가당연한기술이라고생각하면서사용하게될날이멀지않다. 4.5.3 타입시스템 : 소개 타입시스템은말이되는프로그램을판단하는한방법이다. 말이되는프로그램을판단하는방법들은점점정교해져가고있는데, 타입시스템은프로그램이말이되는지를판단하는두번째로정교한방법이라고할수있다. 첫번째방법은문법규칙이다. 제대로생긴프로그램인지를확인하는방법. 문법규칙은간단한귀납규칙들이다 : 부품이제대로생긴프로그램이기만하면그것들을가지고어떻게어떻게하면제대로생긴프로그램이된다, 는식

4.5 언어키우기 III: K 103 이다. 간단한 이유는조건이간단해서다. 부품이제대로생긴프로그램이기만하면된다. 이렇게조건이간단하다보니, 말이되지않는프로그램을모두걸러내지못하는경우가많다. Example 25 프로그램식 E의문법규칙이다음과같다고하자 : E n 정수 s 스트링 E + E 이때 2+ a 는문법규칙에맞는다. 2와 a 는제대로생긴것들이고, 그것들을가지고 + 식을만들었으므로. 하지만말이되지않는프로그램이다. 정수와스트링은더할수없다. 대개의문법규칙들이요구하는조건은너무간단하다. 말이되는프로그램을판단하기에는. 문맥을생각하지않는규칙들이기때문이다. 고려해야할문맥은이런것이다 : + 식은두개의부품식들이모두정수식이어야한다는. 이러한문맥에대한조건을대개의 문법규칙 에는표현하지않는다. 표현하고정교하게다듬으면그것은우리가 문법규칙 의영역에서 타입시스템 의영역으로은근슬쩍넘어가게되는셈이다. 타입시스템 에서는어떤문맥을고려하는가? 프로그램의겉모습만을따지는문맥이아니라, 한단계더파고들어서, 텍스트가가지는속내용을문맥으로고려해야한다. 타입시스템은타입을문맥으로고려한다. 예를들어, x+1 이말이되는프로그램이려면변수 x는정수값을가진변수여야한다. 타입시스템은 x가정수값을가지는상황에서만말이된다고판단한다. 타입시스템은타입에맞는값들이분별있게계산되는프로그램인지를판단해준다. 프로그램의실행은일종의계산이고그계산중에값들은분별있게흘러다닌다. 더하기계산에는숫자들이, 결혼이라는계산에는남자와여자가, 라면끓이기계산에는라면과물과불이, 수력발전계산에는물과터빈이, 등등. 숫자더하기에남자와여자가들어가면안되고, 수력발전에불과자동차가들어가면안된다.

104 기계중심의언어 4.5.4 K = K- + 타입시스템 K- 언어에도타입시스템 type system 을통해서논리적인오류를미리자동으로 찾을수있도록해보자. 타입검증 type checking 이가능하도록. 우선동적타입검증dynamic type checking을알아보자. K-의의미정의대로실행하는실행기interpreter를구현했다면, 실행중에타입을확인해가는과정이필요하게된다. 덧셈식 E 1 + E 2 의두식들은정수값을만들어내는식들인경우에만더하기가진행될수있다. 실행결과가정수인지를확인한후에덧셈이진행되야한다. 프로시져호출식 f (E) 은 f의실체가프로시져인지를실행중에확인한후에나호출이일어날수있다. 실체가메모리주소인보통의변수라면호출이일어날수가없다. 이렇게실행중에값의종류가예상대로흘러다니는지를확인하는것을동적타입검증dynamic type checking이라고한다. 그러나, 위에서이야기한대로, 우리는정적타입검증static type checking이필요하다. 프로그램실행전에타입검증하기. 실행하다가문제가발생하는것보다는문제를미리찾아내고무결점임을확인한후에실행을시작하는것이필요하다. 이런기술을정적타입검증static type checking이라고한다. 검증기가프로그램을분석해서 실행중에타입오류가없을것임 이라고했을때에만프로그램을실행시키고싶다. 더군다나그검증기는믿을만sound하면좋겠다. 타입검증결과문제없을것이라고했는데실행중에문제가발생하는경우가없었으면좋겠다.

4.5 언어키우기 III: K 105 미리이야기하지만, 우리 K- 에서는믿을만sound한타입검증기를만들어내지는못한다. K-는안전한타입검증기sound type checker를갖춘언어를다자인하자는목표를처음부터가지고디자인된언어는아니다. 현재대부분의인기있는프로그래밍언어의모습이기도하다. 그러한언어들의타입시스템이어디까지와있는지를 K-를통해서살펴보자. 현재대부분의프로그래밍언어의모습이어떻게해서그모습이되었는지.

106 기계중심의언어 4.5.4.1 K- 에서계산되는값들의종류 위에서이야기한 K- 에서프로그램식들이계산하는값들의종류는 5 가지가있 다 : Val = Z + B + { } + Record + Addr Record = Id fin Addr 기본값 primitive value 의종류마다이름을붙이자. 이것들이기본타입 primitive type 들이다. 그리고레코드는복합값 compound value 이고, 그타입은레코드부 품들의타입으로만들어진복합타입 compound type 이된다. 메모리주소는값을 보관하고있고, 메모리주소의타입은보관하고있는값의타입에따라분류한 복합타입 compound type 이다. 프로시져는 K- 에서값은아니지만, 그타입을가 지고호출식들이제대로쓰이는지확인할필요가있다. 인자타입과결과타

4.5 언어키우기 III: K 107 입으로구성된복합타입 compound type 이된다. Type τ int bool unit τ loc location type {} {x τ, y τ} record type τ τ procedure type 4.5.4.2 타입검증규칙 K- 타입시스템은다음의판단 typing judgment Γ E : τ 을증명하는논리규칙들이다. 프로그램의미정의규칙과동일한프래임웍이 다. 타입환경 type environment Γ Id fin Type 이라고불리는 Γ는프로그램에나타나는이름들의타입을가진테이블이다. 타입판단 Γ E : τ 은타입환경 Γ에서식 E가제대로실행되고만일끝난다면타입 τ의값을계산한다, 는사실을뜻한다. 규칙들을하나하나보자. 각식의구조에따라하나씩주어져있다. Γ E : τ Γ skip : unit Γ E : τ Γ(x) = τ loc Γ x := E : τ

108 기계중심의언어 Γ E 1 : τ 1 Γ E 2 : τ 2 Γ E 1 ; E 2 : τ 2 Γ E : bool Γ E 1 : τ Γ E 2 : τ Γ if E then E 1 else E 2 : τ Γ E 1 : bool Γ E 2 : τ Γ while E 1 do E 2 : unit Γ E 1 : int Γ E 2 : int Γ{x int loc} E : τ Γ for x := E 1 to E 2 do E : unit Γ E 1 : τ 1 Γ{x τ 1 } E 2 : τ Γ let x := E 1 in E 2 : τ Γ{f τ 1 τ 2 }{x τ 1 } E 1 : τ 2 Γ{f τ 1 τ 2 } E : τ Γ let proc f(x) = E 1 in E : τ Γ(f) = τ 1 τ 2 Γ E : τ 1 Γ f (E) : τ 2 Γ(x) = int loc Γ read x : int Γ E : τ Γ write E : τ Γ n : int Γ(x)τ loc Γ x : τ Γ E 1 : int Γ E 2 : int Γ E 1 + E 2 : int Γ E : int Γ - E : int Γ E 1 : int Γ E 2 : int Γ E 1 < E 2 : bool Γ E : bool Γ not E : bool

4.5 언어키우기 III: K 109 Γ {} : {} Γ E 1 : τ 1 Γ E 2 : τ 2 Γ {x := E 1, y := E 2 } : {x τ 1 loc, y τ 2 loc} Γ E : τ τ(x) = τ loc Γ E.x : τ Γ E 1 : τ Γ E 2 : τ τ(x) = τ loc Γ E 1.x := E 2 : τ Γ E : τ Γ malloc E : τ loc Γ &x : Γ(x) Γ E : τ Γ &E.x : τ(x) Γ E : τ loc Γ *E : τ Γ E 1 : τ loc Γ E 2 : τ Γ *E 1 := E 2 : τ 위의타입시스템을곱씹어보자. 구현을어떻게할지는다음절에서살필것이다. 순수한논리시스템으로서바라보자. 프로그램의구석구석이어떤타입을갖는다고판단될수있는지. 위의타입시스템은한가지재미있는사실이있다. 프로그래머가타입에대해서프로그램텍스트안에써넣은것이전혀없다. 4.5.5 K- 타입시스템의논리적문제 그럴듯하지만아쉬운면이있다. 두가지문제가있다. 안전 sound 하지도않고 완전 complete 하지도않다.

110 기계중심의언어 4.5.5.1 타입검증규칙이안전하지않다 위의타입시스템은믿을만하지않다 unsound. 위의타입시스템이문제없다고 판단한프로그램이실행중에타입오류로멈출수있다. 오류검증이믿을수 없는것이다. 이문제는지금까지 상식의수준에서 키워온언어인 K-에서는해결할수없다. 언어를디자인할때부터, 이문제를염두에두고잘디자인해가야해결할수있는문제이다. 5장에서이과정을밟아갈것이다. 어떻게범용의언어가이문제를해결한편리한타입시스템을가질수있는지겪게될것이다. 이타입시스템이안전하지않은경우는다음과같다 :

4.5 언어키우기 III: K 111 타입시스템을안전하게만들어갈수는있다. 그렇게되면적어도세가지로결론나게될것이다. 안전하게되기위해서 K-를주무르게된다. 가지치고. 그렇게되면더이상 K-라는언어의모습이아닐것이다. 비슷한이야긴데, 다른한결론은, 안전한타입시스템을고안하고구현할수있게되면그타입시스템을통과하는 K- 프로그램은매우소수가될것이다. 그러한 K- 프로그램은 K- 언어의제한된기능만가지고작성된프로그램들이될것이다. 또다른결론은, 안전하게되기위해서매우정교한타입시스템을고안하게될것이고, 그정교함이극에달해서아마도지금의기계로는구현될수없는것이될것이다. 다음 5장에서타입시스템의안전성을염두에두고프로그래밍언어를디자인해가면서달성한성과를살펴볼것이다. 어떻게실용적인범용의언어가이문제를해결한편리한타입시스템을갖추게되었는지알아보자. 프로그래밍언어분야의빛나는성과이다.

112 기계중심의언어 4.5.5.2 타입검증규칙이완전하지않다 K- 타입규칙의두번째문제는, 제대로도는프로그램중에서위의타입시스템을통과하는것은일부분incomplete이다. 잘돌프로그램을모두타입검증할수있는게아니다. 제대로타입오류없이잘돌프로그램을, 위의타입시스템은타입이없다고판단할수있다. 타입시스템이사용하는그물이너무촘촘한것이다. 메모리주소의타입이변할수가없다. 메모리주소에처음으로보관되는초기값의타입이그주소가저장할수있는값들의타입으로고정된다. 변수는항상그초기값과같은타입의값만보관할수있는것이다. 그렇지않은프로그램은타입검증이실패한다. 이문제를해결할수있는좋은방안이뭘까?

4.5 언어키우기 III: K 113 어떤프로시져는인자값의타입에상관없이실행될수있는프로시져들이있다. 이러한프로시져는다양한타입의인자를받으면서아무문제실행될수있다. 이러한프로시져는위의타입시스템에서는타입검증을통과할수없다. 이문제를해결할수있는좋은방안이뭘까? 레코드타입관련해서도타입검증이너무까다롭다. 다음의문제가있다. 복합적인데이타를표현하는데쓰이는레코드의타입이유연하지않다. 복합적인데이타는주로재귀적으로정의되는데이타들이다 ( 예, 리스트나나무구조 ). 리스트가리스트를품고있을것이고, 나무가나무를품고있을것이다. 이런구조를레코드로구현하다보면, C 에서처럼, 레코드의한필드가그재귀를품는고리가된다 ( 예, 리스트노드의 next 필드나나무구조노드의 sub-tree 필드 ). 문제는, 그필드의타입이하나의레코드타입으로정해져서는않된다. 그필드는초기에는빈레코드를가질것이다. 재귀적으로품고있는것이없는것이다. 재귀의깊이가 0인레코드이다. 그러다가실행중에그빈레코드필드가다른레코드를품게될것이다. 재귀구조를품게되는것이다. 예를들어, lst := {val := 0, next := {}}; lst.next := {val := 100, next := {}} 위의 lst의 next 필드의타입은빈레코드타입으로고정될수없다. 초기에빈레코드를가지게되었지만곧이어그필드가다른타입의레코드를가지게되므로. 그렇다고두번째지정문때문에레코드타입 {val int, next {}} 으로도고정될수없다. 초기의빈레코드와타입이맞지않을뿐더러 lst.next.next를통해서또다른레코드가빈필드를바꿔칠수있기때문이다. 이문제를해결할수있는좋은방안이뭘까?

114 기계중심의언어 타입시스템의안전성soundness을개의치않는다면, 위의문제를해결하는방법은쉽게내어놓을수있다. 사실이렇게고안된방법들이현재의대부분의프로그래밍언어에적용되었다. 그흔적을따라가볼것이다. 세번째문제를다음과같이해결하자. 우선, 프로그래머가타입을정의하고이름을지을수있도록하자. 그리고그이름이타입정의에서재귀적으로사용될수있도록하자. 그러면재귀데이타를구현하는레코드에서고리역할을하는필드의타입에이름을사용하면, 그필드가품고있을재귀의깊이를타입에드러내지않게된다. 예를들어 type list = {int val, list next} 라고정의된 list 타입은레코드를뜻한다, 정수를가지는 val 필드와재귀적으로 list를품을수있는 next 필드. 재귀고리에보관되는리스트의깊이는표현될필요가없다. 프로그램에서쓰는타입과타입정의는다음과같은문법을따르도록하자. t int bool unit t loc tid type name T type tid = {t x, t y} type declaration P T E program 타입이름들의유효범위는프로그램전체가되도록했다. 타입이름들이정의되는곳은프로그램의처음부분뿐이다. 타입이름의유효범위가다른이름들같이일부분으로제한되게하는것도가능하겠지만. 그리고, 빈레코드식은임의의타입으로결정될수있다고타입규칙을정의한다. Γ {} : {}

4.5 언어키우기 III: K 115 대신에 Γ {} : τ 로. 빈레코드를초기에가지게되는 list 레코드의 next필드는 list타입이되는것으로판단되는것이다. 이렇게되면, 위에서살펴본프로그램 lst := {val := 0, next := {}}; lst.next := {val := 100, next := {}} 에서 lst의타입은 list loc으로판단할수있고, 두번째줄의지정문도타입검증을통과한다. lst.next도 list loc이므로. 위의해결책으로부터배우는중요한아이디어는이름을사용한다는것이다. 타입에이름을붙이고그이름으로속내용을감춘다. 재귀적인구조를구현하는레코드는재귀고리역할을하는필드가있다. 임의의깊이로레코드를품을수있는그필드의타입. 변화무쌍한재귀의깊이를타입에표현하지않기위해서이름을사용하는것이다. 그러나, 위의해결책이어설픈이유는, 타입시스템이안전하지않은문제가해결되지않았기때문이다. 타입시스템의안전성soundness을포기하고이렇게고안된방법들이현재의대부분의프로그래밍언어에적용되었다. 5장에서는제대로된해결책을논의할것이다. 타입시스템의안전성soundness을보장하면서위의문제들을해결해간결과들. 프로그래밍언어의타입시스템연구의핵심을보게될것이다. 안전하면서최대한많이타입오류없이실행될프로그램들을검증해주는시스템을만들고자한노력의결과들. 이과정을살펴볼것이다. 4.5.6 K- 타입시스템의구현문제 한편, 위와같이고안한 K- 타입시스템을어떻게구현할것인가? 구현한타입시스템은 K-프로그램을받아서예 / 아니오를출력한다. 정의한증명규칙

116 기계중심의언어 에따라서그프로그램의구석구석타입이제대로되었는지증명해낼수있으면 예, 아니면 아니오. 그러한증명기를어떻게구현할수있을까? K- 타입규칙들은의미규칙과는다른양상이있다. 타입검증기구현은 K- 의미규칙을보고실행기interpreter를구현할때와같이간단하지는않다. 구현의문제를간편하게넘어가는방법은, 프로그래머가타입검증을돕는코멘트를프로그램택스트에포함시키도록강제하는것이다. 이와같은방식으로구성된언어가 C, C++, Pascal, Java등의언어들이다. 이과정을그대로 K-에서밟아갈것이다. K- 타입시스템의구현이간단치않은이유를살펴보자. 우선, 구현전략을생각해보자. 타입판단 Γ E : τ 의증명을구현하는타입검증함수의입력은두가지가될것이다 : 프로그램식 E 와 Γ. 주어진두개의입력에대해서타입검증함수는위의타입판단에해당하는 τ가있는지를찾게된다. 타입환경 Γ는프로그램에나타나는이름들의타입들에대해서알려진 ( 가정하게된 ) 내용이다. 이것을가지고프로그램텍스트 E가타입 τ를가질수있는지타입규칙에준해서알아보는것이다. 프로그램전체에대해서는시작 Γ는물론비어있을것이다. 타입검증함수가프로그램의부분들에대해서재귀적으로호출되면서 Γ에정보가쌓이게될것이다. 우리의타입시스템에서구현이어려운이유는다음의규칙에서드러난다 : Γ{f τ 1 τ 2 }{x τ 1 } E 1 : τ 2 Γ{f τ 1 τ 2 } E : τ Γ let proc f(x) = E 1 in E : τ 결론 ( 분모 ) 이가능하려면조건 ( 분자부분에있는 ) 판단들이사실이어야한다. 즉, 프로시져몸통 E 1 이타입 τ 2 를가진다는것이확인되야한다. 조건판단들이사실인지를확인하는것은, 다시타입검증함수를재귀호출하는것이다.

4.5 언어키우기 III: K 117 이때, 타입검증함수에입력으로줄타입환경 Γ{f τ 1 τ 2 }{x τ 1 } 은이미우리가알아내야할 τ 1 과 τ 2 가쓰인다. 그두타입들이프로시저의타 입을구성하기때문이다. 당황스럽다. 출력으로알아내야할것을입력으로 넣어줘야한다? 가능하지않다. 어떻게해야, 위와같이서로물고무는상황을타입검증함수에서구현할수있을까? 프그래머에게책임을맡기자. 프로그래머가타입을명시하도록하자. 타입검증은그힌트에기초해서하자. 프로시져정의에서프로그래머가인자의타입과결과타입을명시하도록하고, 타입검증은그것을가정한상태에서프로시져몸통을타입검증한다. 이렇게 : Γ{f τ 1 τ 2 }{x τ 1 } E 1 : τ 2 Γ{f τ 1 τ 2 } E : τ Γ let proc f(τ 1 x):τ 2 = E 1 in E : τ 이렇게되면구현은쉽다. K- 실행기 interpreter 의구현과같이간편하다. 타입 검증규칙에따라서재귀호출을부르면된다. 프로시져결과의타입을구성하 는 τ 1 과 τ 2 는프로그램텍스트에서프로그래머가명시해놓은것을쓰면된다. 이제지금까지확장되어온 K- 언어를살짜확장해서, 타입을프로그래머 가프로그램텍스트에포함시키도록하자. 프로시져와변수선언에서그변수

118 기계중심의언어 의타입을프로그래머가명시하도록한다. K 라는언어라고하자. E. let t x := E in E let proc f(t x):t = E in E t int bool unit t loc tid type name T type tid = {t x, t y} type declaration P T E program 이제다음과같이프로그램하고타입검증이통과될것이다. 아무튼위와같이확장된 K 언어의타입검증규칙은다음과같다. 타입환 경 type environment 은프로그램에나타나는이름들 ( 변수, 프로시져이름, 레코드

T : T 1 : 1 1 T 2 : 2 4.5 언어키우기 III: K 119 필드 ) 의타입에관한것이었으나, 이제부터는타입이름들의속내용 ( 타입 ) 에 대한환경도필요해진다. TypeId Γ Id fin Type TypeId fin Type Type τ int bool unit tid 변수의타입환경 타입이름의타입환경 τ loc location type tid {} {x τ, y τ} record type τ τ procedure type Γ, P : τ T :, E : τ, T E : τ T 1 T 2 : 2 type tid = {t 1 x 1, t 2 x 2 } : {tid {x 1 t 1 loc, x 2 t 2 loc}} x 1 x 2 Γ, E : τ Γ, E : τ (tid){x τ loc} Γ, {x := E} : tid Γ, {} : τ Γ{f τ 1 τ 2 }{x τ 1 }, E 1 : τ 2 Γ{f τ 1 τ 2 }, E : τ Γ, let proc f(τ 1 x):τ 2 = E 1 in E : τ

120 기계중심의언어 4.5.7 이름공간, 같은타입 프로그래밍언어의두가지이슈를논의하고이장을마치자. 이름공간 name space 과같은타입 type equivalence 의정의에대해서. 우선이름공간에대해서. K 언어에서는많은것에이름을지을수있다. 메모리주소 ( 변수 ), 레코드의필드, 프로그램코드 ( 프로시져 ), 타입. 타입이름 은프로그램전체가유효범위 scope 였고, 변수이름과프로시져의이름은유효 범위 scope 를한정할수있었다. K 에서는같은이름을타입이름이나변수이름으로사용해도프로그램텍 스트에서문제없이구분할수있다. 한이름이프로그램텍스트에서타입이 름으로쓰이는지변수이름으로쓰이는지구분된다. 타입이름이었으면그속 내용은타입이름환경 TypeId fin Type

4.6 정리 121 를참조하면되고, 변수이름이었으면변수의타입환경 Γ Id fin Type 를참조하면된다. 이런경우, 타입이름과메모리주소의이름은다른이름공간name space을가진다고한다. TypeId와 Id로구분되는. 한편, K 언어에서변수이름과프로시져이름은같은이름공간name space Id을공유한다. 이름이변수로쓰였는지프로시져로쓰였는지를구분할수있지만. 모두변수의타입환경을참조한다. 같은타입이란무엇인가? 타입에이름을붙일때, 그내용이같더라도다른이름을붙일수있다 : type a = {int x; int y} type b = {int y; int x} 내용은같지만이름이다르면다른타입인것으로정의할수도있고 (name equivalence), 내용만같다면같은타입이라고정의할수도있겠다 (structural equivalence). K 언어의타입시스템은타입이름이같아야같은타입인것으로정의한셈이다. 4.6 정리 이장에서는상식선에서프로그래밍언어를디자인했던과정을따라가보았다. 현재대부분의널리쓰이는명령형프로그래밍언어들이만들어진과정이었기도하다. 그대표적인경우가 C라는언어이다. 어떻게프로그래밍언어를디자인해야하는지, 무엇이문제일지가드러나지않은상태에서, 주어진디지탈컴퓨터를편하게사용하기위한도구로서프로그래밍언어를디자인했던과거. 이렇게언어를만들었던과정은당시로서는매우상식적이지만현재에서바라보면아쉬움이많다. 현재의프로그래밍언어기술에기대어보면그러한

122 기계중심의언어 솜씨는어설프다. 이과정을되밟아오면서어떤문제들이있는지살펴보았다. 그리고, 그과정에서도지금까지살아남은중요한개념들을살펴보았다. 디지탈컴퓨터라는기계, 폰노인만기계Von Neuman machine, 보편만능의기계universal machine, 프로그램 메모리주소에이름붙이기, 이름의유효범위scope, 이름의실체를결정해주는환경environment, 자유로운이름free name과묶여있는이름bound name, 설탕구조syntactic sugar 명령문에이름붙이기, 프로시져procedure 호출, 재귀호출recursive call, 프로시져호출이이름의유효범위에미치는영향, 동적 / 정적으로결정되는이름의유효범위dynamic/static scoping 메모리를뭉치로다루기, 데이타로서의메모리주소 메모리관리, 메모리재활용 garbage collection 프로그램의오류를미리검증하기, 타입오류, 타입시스템, 타입시스템 의안전성 soundness 과완전성 completeness, 타입에이름붙이기

5 장 값중심의언어 프로그래밍언어를제대로디자인해보자. 디지탈컴퓨터와거리를두자. 기계를편리하게사용하려고언어를디자인하는게아니다. 더높은눈높이를가지자. 소프트웨어의문제를해결해주는프로그래밍언어를디자인해보자. 작성한프로그램에오류가있는지를미리자동으로검증할수있도록하고싶다. 그리고그검증이안전하다는것을보장하고싶다. 다른차원의눈높이에서고안된언어. 그결과는월등한수준에서기계를편리하게사용할수있게해준다. 기계의편리한사용, 그슬로건을직접쫓아다니면서는달성할수없었던결과. 좋은소식은과감히 ( 혹은무심하게 ) 다른차원으로발길을돌리면서만나게된다. 이렇게디자인된언어는공허하지않다. 기계중심의언어들만큼효율적으로실행되고있고, 광범위한상용소프트웨어작성에널리사용되고있다. 제 2세대자동오류검증기술이프로그래밍언어에단단히갖추어진덕이다. 5.1 언어의모델 프로그래밍언어는사실, 컴퓨터라는기계가세상에나오기전부터이미있었다. 프로그래밍언어가컴퓨터를돌리기위해만들어진게아니고, 컴퓨터가프로그래밍언어를돌리기위해만들어졌다고할수있다. 역사적으로프로

124 값중심의언어 그래밍언어가먼저라고할수있기때문이다. 1930-40년대에이미논리학자와수학자들은기계적으로계산가능한것이무엇인지를고민하기시작했다. 괴델 (Gödel) 은부분재귀함수Partial Recursive Function 꼴로정의되는함수들을기계적으로계산가능한것들이라고정의했다. 처치 (Church) 는람다계산법Lambda Calculus으로계산될수있는것들이라고정의했고. 튜링 (Turing) 은튜링기계Turing Machine가실행할수있는것들이라고정의했다. 그런데, 세가지가모두같은정의였다. 부분재귀함수는람다계산법으로계산될수있고, 람다함수는튜링기계로실행할수있고, 튜링기계가실행하는함수는부분재귀함수꼴로정의할수있다. 그러고나니사람들은기계적으로계산가능한함수가그게다가아닐까믿

5.1 언어의모델 125 고있다. 세사람이독자적으로정의한것들이결국다르지않은것으로미루 어. 이것을 Turing-Church Thesis 라고부른다. 이셋중에서람다계산법 Lambda Calculus 이언어의모습을가지고있다. 문 법 syntax 이있고의미정의 semantics 가있다. 5.1.1 람다계산법 Lambda Calculus 람다계산법Lambda Calculus이라는언어를기초로프로그래밍언어를디자인해가면든든하다. 그언어의표현력이완전하기때문이다. 기계적으로계산가능한모든것이 ( 컴퓨터로돌릴수있는모든프로그램이 ) 바로그언어로작성되는것이라고여겨지고있으니. 이렇게빠뜨림없이기계적인계산의모든것을표현할수있는언어를 Turing-complete 하다 고한다. 겠다. 앞으로람다계산법 Lambda Calculus 을언어이름으로간단히 람다 라고부르 람다의문법구조 syntax 는간단하다 : Exp E x variable λx.e abstraction E E application x는이름이다. λx.e는함수를뜻한다. x는함수의인자고 E는함수의몸통이다. x의유효범위는 E이다. λx.e는 E에나타나는 x를 묶어bind준다 고한다. E 1 E 2 는함수를적용하는식이다. E 1 은계산하면함수 λx.e가되야하고 E 2 는그함수의인자 x의실체가된다.

126 값중심의언어 람다의의미구조 semantics 도간단하다. 사용할표기법을우선익히자. Notation 3 E 의자유변수 free variable 들 FV (E) 은 E 에서 λ- 식으로묶여있지 않은변수들이다. FV (x) = {x} FV (λx.e) = FV (E) \ {x} FV (E 1 E 2 ) = FV (E 1 ) FV (E 2 ) Notation 4 치환 substitution 은변수를다른것으로바꿔주는연산이다. 치환

5.1 언어의모델 127 S 는변수 x i 를 Y i 로바꾸는아이템 x i Y i 들의집합이다. {x 1 Y 1,, x n Y n } 모든 x i 들은달랴야한다. Supp(S) (support set of S) 는 S 가바꾸는변수들 {x S(x) x} 이다. 변수 x A 를 Y B 로바꿔주는치환들의집합을 A fin B 로표현한다. 변수를람다식으로바꾸는치환 S Id fin Exp 에대해서, FV (S) 는바꿔들 어갈식들의자유변수들의합집합이다 : FV (S) = 1 i n FV (E i ) Notation 5 치환 S 를람다식 E 에적용하는것을 S E 로쓰는데다음과같이 정의된다 : S x = E x if x E S otherwise S (λx.e) = λy.(s {x y} E) (new y) S (E 1 E 2 ) = (S E 1 )(S E 2 ) 위에서 new y 란나타난적이없는변수 y 라는뜻이다 : y {x} FV (λx.e) FV (S). Notation 6 두개의치환 S, T 를나란히 S T 라고쓰면, T 로바꾸고나서 S 로

128 값중심의언어 바꾸는치환을뜻한다 : S T = {x S (T (x)) x Supp(T )} {x S(x) x Supp(T ) \ Supp(S)} Notation 7 문맥구조 context C 는빈칸 [] 을딱하나품고있는람다식이다. Context C [] C E E C λx.c 빈칸을품은람다식을강조하기위해 C[] 라고쓰고, 그빈칸에들어있는 ( 다 시써야할 ) 람다식 E 까지드러내어 C[E] 라고표현한다. 모든람다식은 C[E] 꼴로표현되는데, 그람다식의부품으로 E 가있다는것을뜻한다.

5.1 언어의모델 129 다음의계산규칙으로람다식을바꿔쓰는것이계산과정이다. 계산규칙은 3 개 다. (β-reduction) (λx.e 1 ) E 2 {x E 2 }E 1 (α-reduction) x FV (λx.e) λx.e λx.{x x }E E 1 E 2 C[E 1 ] C[E 2 ] α- 연산 α-reduction 은람다함수의인자이름을바꿔주기만한다. 의미있는계산 은아니다. 의미있는계산과정은오직하나다. β- 연산 β-reduction 규칙이다. 람다식에 서 β- 연산가능한부분을찾아다시쓰고, 다시그결과에서 β- 연산가능한부

130 값중심의언어 분을찾아서다시쓰고. 이과정이계산과정이다. 람다식에서 β- 연산가능한 부분 (λx.e)e 1 을레덱스 redex(reducible expression) 라고부른다. 람다계산과정은끝나지않고영원히계속될수도있다. 끝나는때는, β-연산가능한부분 ( 레덱스redex) 이더이상없을때이다. 그런람다식을정상식normal term이라고한다. 정상식normal term으로계산을끝낼수있는람다식을정상식normal term을가지고있는람다식이라고한다. 위의 3 가지계산규칙들이유일한바꿔쓰기과정을정의하지는않는다. 람 다식에서바꿔쓰기하는순서가여러가지가있을수있다. 레덱스 redex 가여러 곳에있을수있기때문이다. 어느레덱스 redex 부터바꾸느냐에따라계산이달라진다. 계산순서에따라, 정상식 normal term 을가진 ( 끝날수있는 ) 람다식이그정상식으로끝나지못하 고영원히계산을계속할수도있다. 그러나, 람다식이계산이끝난다면, 그결과는오직한가지만가진다. 계산순서가다르게진행되왔을수도있겠으나, 끝난다면모두하나의정상식normal term으로끝맺음된다. Church-Rosser Theorem 혹은 Confluence Theorem 이이것을보장한다.

5.1 언어의모델 131 정상식 normal term 을가진람다식이라면, 어떤순서로계산을해야항상그 정상식에도달할수있을까? 자칫순서를함부로하면정상식에도달못하고 영원히떠돌수있다. 정상순서normal-order reduction로계산하면된다. 레덱스redex가여럿있을때, 그중에제일왼쪽제일위의레덱스redex를계산해가는것이다. 이순서로계산하면정상식normal term이있는람다식은항상그정상식에도달한다.

132 값중심의언어 5.1.2 람다로프로그램하기 위와같이정의된람다언어로프로그램을한다? 기계적으로계산가능한모 든함수들을작성할수있을까? 정상순서 normal-order reduction 로계산되는람다를가지고자연수와참 / 거짓 을다루는연산들을다음과같이정의할수있다.

5.1 언어의모델 133 하지만기계적으로계산가능한모든함수를람다로짤수있으려면재귀 함수가프로그램될수있어야한다. 다음과같이재귀함수도정의할수있다.

134 값중심의언어 이처럼람다의놀랄만한능력이간단한문법과계산방식에서나온다. 모든계산가능한함수들을람다로흉내낼수있다. 람다로표현하고람다의계산법으로실행하면흉내내는함수의결과에해당하는람다표현식이등장한다.

5.2 언어키우기 0: M0 135 5.2 언어키우기 0: M0 람다를프로그래밍언어로바라보자. λx.e 는함수정의로본다. 그런데그함수의이름은없다. 인자가 x이고몸통이 E인함수이다. E 1 E 2 는함수를적용하는식이다. 람다에서계산과프로그램에서의실행은조금다르다. 람다에서계산의끝은식의모든구석구석에레덱스redex가없는경우다. 함수식 λx.e의몸통식 E에도레덱스가있다면몸통식은계산이된다. 그러나프로그램으로서 λx.e는최종값이다. 자체로는실행될부품이더이상없는. 몸통 E의실행은그함수가호출될때비로소시작된다. 프로그램

136 값중심의언어 에서최종값 λx.e 를기준식 canonical term 이라고부른다. 앞으로기준식 canonical term 이값이므로종종 v( value ) 로표기하겠다. 5.2.1 소극적인실행 lazy evaluation 과적극적인실행 eager evaluation 실행하면서함수는자체로값이다. 실행할부품이더이상없다. 함수의몸통은그함수가호출될때에비로소실행될뿐이다. 그런데함수가호출될때 E 1 E 2, 인자식 E 2 은언제실행해주기로할까? 두가지선택이있다. 일단몸통을실행하면서인자값이필요할때에인자식을실행하기. 혹은, 몸통을실행하기전에인자식을실행해서인자값을구한후에몸통을실행하기. 첫번째경우를소극적인실행lazy evaluation, normal-order evaluation 혹은식전

5.2 언어키우기 0: M0 137 달호출 call-by-name, call-by-need 이라고하고, 두번째경우를적극적인실행 eager evaluation 혹은값전달호출 call-by-value 이라고한다. 프로그래밍언어로서람다의소극적인실행lazy evaluation, normal-order evaluation과적극적인실행eager evaluation을정의하는규칙은아래와같다. 두번째규칙이두실행방식의차이를보여준다. 첫번째규칙은함수가더이상실행될

138 값중심의언어 부품이없는값임을표현하고있다. lazy evaluation eager evaluation λx.e N λx.e λx.e E λx.e E 1 N λx.e {x E 2 }E N v E 1 E 2 N v E 1 E λx.e E 2 E v {x v}e N v E 1 E 2 E v 소극적인실행과적극적인실행은장단점이있다. 소극적으로실행하면적 극적인경우보다빨리계산되는경우가있고, 그반대의경우도있다. 아래를 소극적으로실행하면 (λx.7)((λx.x x)(λx.x x)) N 7 이지만, 적극적으로실행하면영원히돈다. E E. (λx.7)((λx.x x)(λx.x x)) (λx.7)((λx.x x)(λx.x x)) 한편, 아래를소극적으로실행하면 (λx.(x x))e N (E E) N E 를두번실행해야하겠지만, 적극적으로실행하면한번만실행하면된다. (λx.(x x))e E (λx.(x x))v E (v v) E.

5.2 언어키우기 0: M0 139 5.2.2 시작언어 : 값은오직함수 람다언어의문법으로시작하자. E x variable λx.e function E E application 이언어에서이름지을수있는것은값뿐이다. 이름을 변수 라고하자. 변수 x의유효범위scope는그이름을묶은함수 λx.e의몸통 E이다. 각변수가무슨값을뜻하는지는, 그변수를묶은함수가호출될때전달되는인자값이그변수가뜻하는값이된다. 의미정의는프로그램텍스트를변화시키지않으면서정의하자. 기계중심언어의의미구조를정의했을때와같은스타일이다. 식 E의의미판단 σ E v 은환경 σ에서식 E는값 v를계산한다, 는뜻이다. 환경environment은변수가뜻하는값을결정해준다. 의미정의에서환경을따로가지는이유는, 프로그램식을변경시키지않기때문이다. 변수는그대로프로그램에남아있는다. 예전같이프로그램이름이텍스트에서해당값으로바꿔써지는방식이아니다. 값은정수와함수뿐이다. 함수값을클로져closure라고하는데, 함수 λx.e 텍스트자체와그함수가정의될때static scoping의환경이다. 환경의역할은 λx.e에서자유로운변수들의값을결정해준다. σ Env = Id fin Val v Val = Closure λx.e, σ Closure = Exp Env 의미규칙들은다음과같다. 적극적인실행 eager evaluation 규칙을가진다.

140 값중심의언어 σ E v σ(x) = v σ x v σ λx.e λx.e, σ σ E 1 λx.e, σ σ E 2 v σ {x v} E v σ E 1 E 2 v 5.3 언어키우기 I: M1 M0 를가지고모든프로그램을짤수있지만불편하다. M0 에없었던것들은 모두설탕구조 syntactic sugar 지만, 프로그래밍의편의를위해첨가하자.

5.3 언어키우기 I: M1 141 5.3.1 다른값 : 정수, 참 / 거짓 정수, 참 / 거짓, 재귀함수 rec f λx.e, 조건식 if E E E, 그리고덧셈식 E + E 과동치식 E = E. ( 덧셈과동치뿐아니라뺄셈곱셈또는그리고등이모두유용하겠지만간략한논의를위해생략한다.) E. n integer true false let x = E in E if E E E rec f λx.e E + E E = E 설탕을녹여서모두 M0언어로표현할수있겠으나, 그자체로그대로놔두자. 특히 let x = E 1 in E 2 는다음의설탕이다 : (λx.e 2 ) E 1 이제값들은세종류가있다 : 함수값과정수그리고참 / 거짓. v Val = Closure + Z + B z Z the integer set b B = {true, false} σ Env = Id fin Val 프로그램의모든식들은값을계산한다. 의미규칙들은 σ E v σ n n

142 값중심의언어 σ true true σ false false σ E 1 v 1 σ{x v 1 } E 2 v σ let x = E 1 in E 2 v σ E 1 true σ E 2 v σ if E 1 E 2 E 3 v σ E 1 false σ E 3 v σ if E 1 E 2 E 3 v σ rec f λx.e rec f λx.e, σ σ E 1 z 1 σ E 2 z 2 σ E 1 + E 2 z 1 + z 2 σ E 1 v 1 σ E 2 v 2 σ E 1 = E 2 v 1 = v 2 그리고함수의호출식의의미규칙에재귀함수의경우가필요하다. σ E 1 rec f λx.e, σ σ E 2 v σ {f rec f λx.e, σ }{x v} E v σ E 1 E 2 v z 1 + z 2 는정수에서정의된덧셈이다. v 1 = v 2 는동치인지아닌지를계산한다. 이때 v i 들은모두정수거나참 / 거짓값이어야한다. 함수값들인경우동치를판단할수없다. 일반적으로두함수를보고같은인자에대해서같은결과를항상내놓는함수인지는기계적으로판단불가능하다. 가능하다면그것을이용해서멈춰요문제Halting Problem를푸는프로그램을정의할수있기때문이다. 5.4 언어키우기 II: M2 5.4.1 구조가있는값 : 쌍 pair 구조를가진데이타를프로그램하기쉽게하자. 쌍을만들고사용하는방식을

5.4 언어키우기 II: M2 143 제공하자. 이것들도설탕이지만첨가하자. E. (E,E) E.1 E.2 이제값들은세가지종류가있다 : 함수값, 정수, 참 / 거짓, 혹은두값의쌍. v Val = Closure + Z + B + Pair v, v Pair = Val Val σ Env = Id fin Val ( 잠깐, 위의 Val 집합의정의가이상하다. Val 이자기자신을가지고정의되었 다 : Val = Val Val. 그런집합 Val 은물론존재한다. 공집합도아닌. 심 지어는 X = X fin X를만족하는공집합이아닌집합 X도존재한다.) 의미규칙은다음이첨가된다. σ E v σ E 1 v 1 σ E 2 v 2 σ (E 1,E 2 ) v 1, v 2 σ E v 1, v 2 σ E.1 v 1 σ E v 1, v 2 σ E.2 v 2 쌍을만들고쓸수있도록하는위의것들은모두설탕이다. 어떻게녹일 수있을까? 어떻게같은일을하는프로그램을 M0 가지고만들수있을까? 다 음정의 E 대로 E 를녹일수있다 : (E 1,E 2 ) = λm.(m E 1 ) E 2 E.1 = E(λx.λy.x) E.2 = E(λx.λy.y)

144 값중심의언어 쌍만있으면임의의구조물을만들수있다. 리스트도표현할수있고, 나무구 조도표현할수있고, 그래프도표현할수있고, 함수나테이블도표현할수있 다. Example 26 예를들어, 리스트를구현해보자. 어떤리스트라도두가지만있으면만들수있다 : 빈리스트와리스트앞에하나덧붙여새로운리스트를만드는방법. 이두개를각각 nil과 link라고하자. nil은 0으로정의하자. ( 리스트의원소로 0이사용되지않는다고가정한다 ). link는다음의함수로정의하자 : λx.λlst.(x,lst) 그러면 link 1 nil 은 1 하나있는리스트 [1] 를, link 1 (link 2 nil) 은 [1, 2] 인리스트를만든다. 사용하는방법으로는리스트가비어있는지판단하는방법 isnil? 과리스트의처음원소와나머지원소를계산하는함수들 head와 tail만있으면된다. 다음과같이각각정의하면된다. isnil? head tail λlst.(lst = nil) λlst.(lst.1) λlst.(lst.2) Example 27 또다른예로, 두갈래나무구조 binary tree 를구현해보자. 만드는 방법은세가지 : empty, leaf, node. 사용하는방법은세가지 : isempty?, left, right. 다음과같이정의할수있다. empty leaf node 0 λx.x λlt.λrt.(link lt rt) isempty? left right λt.(t = empty) λt.(t.1) λt.(t.2)

5.5 언어키우기 III: M3 145 5.5 언어키우기 III: M3 5.5.1 메모리주소값 : 명령형언어의모습 컴퓨터메모리를사용하는명령형언어의모습 imperative features 도있으면편리 하다. 설탕이지만첨가한다. 프로그래밍편의를위해서. E. malloc E!E E := E E ; E 새로운메모리주소를할당받고, 메모리주소에저장된값을읽고, 메모리주소에값을쓰게된다. 메모리를가지면서, 프로그램실행순서에따라서다른결과를계산하게될수있다. 주소에쓰고나서읽느냐, 읽고나서쓰느냐에따라. 이제값의공간에는메모리주소가포함된다 : v Val = Closure + Z + B + Pair + Loc l Loc an infinite coutable set σ Env = Id fin Val 메모리주소가값이되면서, 프로그램식의의미판단에는메모리가필요하다. 메모리에는프로그램의식들이계산되면서일어난반응들이계속쌓여간다. 의미판단 σ, M E v, M 은식 E가환경 σ와메모리 M에서 v를계산하고결과메모리는 M 이다.

146 값중심의언어 메모리는주소에서값으로가는유한함수다. M Memory = Loc fin Val 의미규칙은다음과같다. σ, M E v, M σ, M E n, M σ, M malloc E l, M n > 0, {l, l + 1,, l + n 1} Dom M σ, M E l, M σ, M!E M (l), M σ, M E 1 l, M 1 σ, M 1 E 2 v 2, M 2 σ, M E 1 := E 2 v 2, M 2 {l v 2 } l Dom M 2 σ, M E 1 M 1 σ, M 1 E 2 M 2 σ, M E 1 ; E 2 M 2 다른모든식들의의미규칙에도메모리반응이쌓여가는것이표현되야할 것이다. 예를들어, σ, M E 1 λx.e, σ, M 1 σ E 2, M 1 v, M 2 σ {x v}, M 2 E v, M 3 σ, M E 1 E 2 v, M 3 Exercise 2 메모리를다루는것들이모두설탕일수있다. 어떻게 M0 로그설 탕을녹일수있을까?

5.6 언어키우기 III: M3 147 M3 의문법을다시정리하면 : E x variable λx.e function E E application n integer true false boolean let x = E in E if E E E rec f λx.e E + E E = E (E,E) E.1 E.2 malloc E!E E := E E ; E 모든것이첫 3 개만이면충분한것들이지만, 프로그래밍의편의 ( 혹은프로그 래밍파라다임, 혹은상위의프로그래밍 ) 을위해서설탕으로제공되었다. 이 제더필요한것들이있다면비슷하게설탕으로첨가해갈수있을것이다. Exercise 3 반복문 while E do E 도설탕이다. 우선 M3 로녹일수있다. M3 는모두 M0 로녹을수있었으므로, 결국에는 M0 로녹게된다.

148 값중심의언어 5.6 오류검증의문제 M3는유용하지만, 실행되서는안될프로그램들이있다. 실행중에타입이맞지않아서실행을멈추게되는경우를가진프로그램들이다. M3 프로그램은다섯종류의값들이있고각각분별력있게흘러다녀야한다. 다섯종류는함수, 정수, 참 / 거짓, 쌍, 메모리주소이다. 함수적용식 E 1 E 2 에서식 E 1 의결과값은함수여야한다. 덧셈식 E 1 + E 2 의두부품식들의결과는정수여야한다. 조건식 if E 1 E 2 E 3 의 E 1 의결과는참또는거짓이어야한다. 쌍에서첫번째값을뜻하는식 E.1에서 E의결과값은쌍이어야한다. 메모리에쓰는식 E 1 := E 2 에서 E 1 의결과값은메모리주소여야한다. M3 프로그램이위와같은타입의조건을실행중에항상만족하는지를미리자동으로검증하는것이가능했으면한다. 또한그검증방법이믿을만했

5.6 오류검증의문제 149 으면한다. 미리 static 안전 sound 하게검증하는그러한타입시스템이 M3 에대해서는가 능해진다. 5.6.1 정적타입시스템 static type system 정적타입시스템static type system은말이되는프로그램인지를프로그램텍스트만으로판단하는한방법이다. 실행중에확인하는것이아니라, 실행전에미리확인하는시스템이다. 정적타입시스템은정적의미구조static semantics라고부르기도한다. 이에반해, 지금까지의의미정의는프로그램실행에대한것이므로동적의미구조dynamtic semantics라고한다.

150 값중심의언어 프로그램이말이되는지를미리검증하는방법들은점점정교해져가고있는데, 정적타입시스템은두번째로정교한방법이라고할수있다. 첫번째방법은문법검증이다. 제대로생긴프로그램인지를확인하는방법이다. 문법검증이확인하는문법규칙은간단한귀납규칙들이다 : 부품이제대로생긴프로그램이기만하면그것들을가지고어떻게어떻게하면제대로생긴프로그램이된다, 는식이다. 간단한 이유는조건이간단해서다. 부품이제대로생긴프로그램이기만하면된다. 이렇게조건이간단하다보니, 말이되지않는프로그램을모두걸러내지못하는경우가많다. Example 28 프로그램식 E의문법규칙이다음과같다고하자 : E n 정수 s 스트링 E + E 이때 2+ a 는문법규칙에맞는다. 2와 a 는제대로생긴것들이고, 그것들을가지고 + 식을만들었으므로. 하지만말이되지않는프로그램이다. 정수와스트링은더할수없다. 대개의문법규칙들이요구하는조건은너무간단하다. 말이되는프로그램을판단하기에는. 문맥을생각하지않는규칙들이기때문이다. 고려해야할문맥은이런것이다 : + 식은두개의부품식들이모두정수식이어야한다는. 이러한문맥에대한조건을대개의 문법규칙 에는표현하지않는다. 표현하고정교하게다듬으면그것은우리가 문법규칙 의영역에서 정적타입시스템 의영역으로은근슬쩍넘어가게되는셈이다. 정적타입시스템 에서는어떤문맥을고려하는가? 프로그램의겉모습만을따지는문맥이아니라, 한단계더파고들어서, 텍스트가가지는속내용을문맥으로고려해야한다. 정적타입시스템은타입을문맥으로고려한다. 예를들어, x+1 이말이되는프로그램이려면변수 x는정수값을가진변수여야한다. 타입시스템은 x가정수값을가지는상황에서만말이된다고판단한다. 타입은서로다른종류의값들에붙이는이름이다.

5.6 오류검증의문제 151 타입시스템은타입에맞는값들이분별있게계산되는프로그램인지를판단해준다. 프로그램의실행은일종의계산이고그계산중에값들은분별있게흘러다닌다. 더하기계산에는숫자들이, 결혼이라는계산에는남자와여자가, 라면끓이기계산에는라면과물과불이, 수력발전계산에는물과터빈이, 등등. 숫자더하기에남자와여자가들어가면안되고, 수력발전에불과자동차가들어가면안된다. 이분별은더욱정교할수도있다. 결혼이라는계산에는나이차가 20년이하인남자와여자가, 라면끓이기계산에는라면하나, 물 500cc 안팎, 가스레인지불정도크기의화력이들어와야한다는식의. 타입시스템은일종의정적프로그램분석 static program analysis 이다. 프로그 램이실행중에가지는어떤성질을실행하기전에예측하는것이다. 분석하고 자하는성질은, 프로그램이타입에맞게실행될것인지여부다. 대부분의프로그램분석이그렇듯이, 대부분의정적타입시스템은완전하지못하다incomplete. 타입에맞게잘실행되는프로그램이지만타입시스템에따라살펴보고결론으로 잘모르겠다 라고할수있는것이다. 그렇지만, 안전sound하다는것은보장된다. 예 라고판단된프로그램은반드시타입에맞게실행된다는것이보장된다. 아니, 보장되도록우리가타입시스템을고안하게된다. 정적타입시스템static type system은형식논리formal logic 시스템이다. 논리식의생김새, 논리식의의미 ( 참혹은거짓 ), 참인논리식을기계적으로추론하는규칙들inference rules, proof rules, 그규칙들이좋다는증명 ( 안전성과완전성증명soundness and/or completeness) 으로구성된다. 그렇게디자인이끝나면, 구현하게된다. 구현된타입시스템은대상프로그래밍언어로작성된임의의프로그램을입력으로받아타입오류가있을지없을지를검증한다. 구현되는알고리즘이디자인한타입시스템을제대로구현한것이라는사실도확인하게된다. 디자인에서구현까지단단한과정을밟는다.

152 값중심의언어 5.6.2 형식논리시스템 formal logic 리뷰 형식논리시스템을우선복습해보자. 형식논리시스템은다음의것들로구성된다 : 논리식집합의정의, 논리식 의미의정의, 참논리식집합의정의, 참논리식추론의방법, 추론방법평가하 기. 선언논리propostional logic 시스템을보자. 논리식집합은다음과같은귀납 규칙으로정의된다 : f T F f f f f f f f 논리식의정의는다음과같고 : [T ] = true [F ] = false [ f ] = not[f ] [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 ]

5.6 오류검증의문제 153 이제참인논리식들의집합을정의한다 : 즉, 쌍 ({f 1,, f n }, f)( 표기 : Γ f ) 들의집합이다. 참인식 f 1 f n f 들의집합들 : Γ 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 3 Γ {f 2 } f 3 Γ f 1 f 2 Γ f 3 Γ {f 1 } f 2 Γ f 1 f 2 Γ f 1 Γ f 1 f 2 Γ f 2 Γ {f} F Γ f Γ f Γ f Γ F 이규칙들은참인식을만드는규칙이고, 이것을논리시스템에서는추론규 칙 inference rules 혹은증명규칙 proof rules 이라고한다. 여기서살짝다른관점 : 참논리식집합을만드는과정은곧, 참논리식을유 추한증명을만드는과정이기도하다. 증명들의집합을만드는귀납규칙으로 보는것이다. 예를들어, 증명규칙 Γ f 1 Γ f 2 Γ f 1 f 2 은증명을만드는귀납규칙 Γ f 1 와 Γ f 2 의증명들을가지고 Γ f 1 f 2 의 증명을만든다.

154 값중심의언어 이렇게만들어지는증명을증명나무 proof tree 라고한다 : {p p, p} p {p p, p} p p {p p, p} p {p p, p} p {p p, p} F {p p} p 이제그러한 기계적인 ( 아무생각없는, 의미를생각하지않는 ) 증명규칙혹은추론규칙proof rules, inference rules이정말좋은가? 를따진다. 즉, 추론규칙들로만드는 {g 1,, g n } f 는어떤것들인가? 예 ) [g 1 g n f ] = true 인가? 여기, 두개의기준이있다 추론규칙의안전성 soundness: Γ f 이면 [Γ f ] = true 추론규칙의완전성 completeness: Γ f 면이 [Γ f ] = true 5.7 단순타입시스템 simple type system M0 로모든것을프로그램할수있겠으나, 값은오직함수밖에없었다. 값의 타입으로함수와정수만있는 M1 의코아만생각하자. E n x λx.e E E E + E

5.7 단순타입시스템 simple type system 155 위의의미규칙 σ E v 를사용할수도있으나, 타입시스템의안전성증명에서편리한방식을위해 서프로그램텍스트를다시써가는방식의의미정의를하자. 같은의미정의 이지만실행문맥 evaluation context 을이용해서다음과같이정의하자 : Value v n λx.e EvaluationContext C [] C E v C C + E v + C 실행문맥은적극적인실행 eager evaluation 순서에준해서다음에실행해야할부 분을결정해준다. 프로그램의실행규칙은다음과같다. E E C[E] C[E ] (λx.e)v {x v}e z 1 + z 2 z 1 + z 2 프로그램 E 의의미는위의규칙에따라서 E E 진행되는과정으로정의된다.

156 값중심의언어 5.7.1 단순타입추론규칙 이제준비는끝났다. 타입시스템을정의하자. 프로그램텍스트만을가지고타입오류없이실행되는프로그램인지를검증하는논리시스템이다. 프로그램텍스트에타입이명시된것이없다. 그래도그논리시스템은프로그램구석구석의타입이어떻게기계적으로유추될수있는지를정의한다. 그유추시스템이어떻게구현되야하는지, 과연구현될수는있는건지, 등에대해서는나중에논의하기로하자. 일단은, 그논리시스템이잘디자인되었으면좋겠다. 믿을수있는시스템이었으면좋겠다. 그런지를먼저확인한후에, 그것을충실히구현할방안을모색하겠다. 타입 τ 는프로그램식들이실행결과로가지는값들의종류들이다. 우리 언어에서는다음의것들로구분될것이다 : Type τ ι primitive type τ τ function type 논리식의생김새는 Γ E : τ 이다. Γ 는타입환경 type environment 으로변수들의알려진타입을가지고있다 : Γ Id fin Type Notation 8 타입환경 Γ 에대해서 Γ{x τ} 대신해서 Γ + x : τ 로도쓰겠다. x τ Γ 대신에 x : τ Γ 로도쓰겠다.

5.7 단순타입시스템 simple type system 157 논리식의의미는 [Γ E : τ ] = true iff σ = Γ.E 이영원히돌든가, 값을계산 E v 하면 v : τ. 이제참인논리식 ( 타입판단 ) 을유추하는규칙을정의하자. 타입추론규칙 type inference rules 이라고한다 : Γ E : τ Γ n : ι Γ(x) = τ Γ x : τ Γ + x : τ 1 E : τ 2 Γ λx.e : τ 1 τ 2 Γ E 1 : τ 1 τ 2 Γ E 2 : τ 1 Γ E 1 E 2 : τ 2 Γ E 1 : τ 1 τ 2 Γ E 2 : τ 1 Γ E 1 + E 2 : τ 2 Example 29 타입유추가성공되는과정을살짝살피면아래와같다 :.. λx.x + 1 : ι ι (λy.y) 2 : ι (λx.x + 1) ((λy.y) 2) : ι Example 30 타입유추가불가능한경우는아래와같다 :.!. λy.y : ι ι λz.z : ι λx.x + 1 : ι ι (λy.y) (λz.z) : ι (λx.x + 1) ((λy.y) (λz.z)) : ι

158 값중심의언어 위의규칙의특성을살펴보자. 식 E의생김새마다오직하나의규칙이있다. 이사실은증명규칙의성질을증명할때우리를편하게한다. 예를들어서 Γ λx.e : τ τ 이유추되었다면반드시한경우밖에는없다 : λx.e의타입유추규칙이하나밖에없으므로, 그규칙에있는조건이만족한경우밖에는없다. 즉, Γ λx.e : τ τ 이면이 Γ + x : τ E : τ Γ E E : τ 이면이 Γ E : τ τ Γ E : τ. 어떤식 E 에대해서, Γ E : τ 인 τ 가여럿가능하다. {x : ι} x : ι λx.x : ι ι {x : ι ι} x : ι ι λx.x : (ι ι) (ι ι) 문제없이실행되는프로그램이타입유추가불가능한경우가있다. 완 전 complete 하지는못한것이다.. {f : τ τ } f : τ τ. {f : τ τ } f : τ τ = τ τ {f : τ τ } f f : τ λf.f f : (τ τ ) τ

5.7 단순타입시스템 simple type system 159 5.7.2 추론규칙의안전성 우리는추론규칙의안전성 soundness 을증명할수있다. 안전성이란, 프로그램 이타입추론이성공하면그프로그램은타입오류없이실행된다는것이보장 됨, 이다. 즉, 프로그램 ( 자유변수가없는식 ) E 에대해서 E : τ 이추론될수있다면, 프로그램 E는문제없이실행되고, 끝난다면결과값이 τ 타입이라는것이다. 타입시스템의안전성을증명하는방법으로대표적인두가지를살펴보자.

160 값중심의언어 5.7.2.1 안전성증명방법 I 두개의정리를증명하는것이다. Progress Lemma: 값이나올때까지문제없이진행한다. e : τ 이고 e가값이아니면반드시 e e. Subject Reduction Lemma: 진행은타입을보존한다. e : τ 이고 e e 이면 e : τ. 위의두정리가증명되면타입유추규칙의안전성soundness이증명되는것이다. 타입유추가성공한프로그램은항상문제없이실행되는것이고, 끝난다면유한스텝만에값으로결과를내는것이므로그결과는유추한프로그램의타입을가진다. 두정리의증명과정을살펴보자. 모두귀납법으로진행되는손쉬운증명이다. Lemma 1 (Progress) E : τ 이고 E가값이아니면반드시진행 E E 한다. Proof. E : τ의증명에대한귀납법으로. ( 증명규칙이 E의구조를따라귀납하므로, E의구조에대한귀납법으로 ( By structural induction on E ) 라고해도된다.) E = E 1 E 2 인경우 : E 1 E 2 : τ이므로타입추론규칙에의해 E 1 : τ τ이고 E 2 : τ 이다. 따라서, 귀납가정에의해서, E 1 이값이아니면진행 E 1 E 1 하고, 이는곧프로그램실행 의정의에의해 E 1 E 2 E 1 E 2 과같다. 마찬가지로, E 1 이값이고 E 2 가값이아니라면진행 E 2 E 2 하고, 이는곧프로그램실행 의정의에의해 E 1 E 2 E 1 E 2 과같다. E 1 과 E 2 가모두값이라면, E 1 : τ τ일수있는값 E 1 은오직 λx.e 경우뿐이다. 따라서프로그램실행 의정의에의해반드시진행 E 1 E 2 = λx.e E 2 {v/x}e 한다.

5.7 단순타입시스템 simple type system 161 다른경우도마찬가지로증명. Lemma 2 (Subject Reduction, Preservation) E : τ 이고 E E 이면 E : τ. 1 Proof. E : τ의증명에대한귀납법으로진행한다. e = E 1 E 2 인경우 : E 1 E 2 : τ이므로타입추론규칙에의해 E 1 : τ τ이고 E 2 : τ 이다. E 1 E 2 E 이라면세가지경우밖에없다 : E 1 E 1 이라서 E 1 E 2 E 1 E 2 인경우. 귀납가정에의해 E 1 : τ τ. E 2 : τ 이므로, 타입추론규칙에의해 E 1 E 2 : τ. E 1 은값이고 E 2 E 2 이라서 E 1 E 2 E 1 E 2 인경우. 위의경우와유사. E 1 과 E 2 가모두값인경우. E 1 : τ τ인값 E 1 은타입추론규칙에의해 λx.e 밖에는없다. 즉, E 1 E 2 = (λx.e ) v 이고, (λx.e ) v {v/x}e 이다. λx.e : τ τ이라면타입추론규칙에의햇 x : τ E : τ이다. v : τ 이므로, Preservation under Substitution Lemma 에의해 {v/x}e : τ이다. 치환은타입을보존한다. Lemma 3 (Preservation under Substitution) Γ v : τ 이고 Γ + x : τ E : τ 이면 Γ {v/x}e : τ. Proof. Γ + x : τ E : τ 의증명에대한귀납법으로증명한다. E = λy.e 인경우 : 항상 y {x} FV v 인 λy.e 로간주할수있으므로 {v/x}λy.e = λy.{v/x}e. 따라서, 보일것은 Γ λy.{v/x}e : τ = let τ 1 τ 2. 가정 Γ + x : τ λy.e : τ 1 τ 2 으로부터타입추론규칙에의해 Γ + x : τ + y : τ 1 E : τ 2 이고, Γ v : τ 와 y FV (v) 으로부터 Γ + y : τ 1 v : τ 2 1 증명규칙이 e의구조를따라귀납하므로, e의구조에대한귀납법으로진행한다 고해도된다. 2 물타기Weakening Lemma 정리 ( 정의와증명이쉽다.)

162 값중심의언어 이므로, 귀납가정에의해 Γ + y : τ 1 {v/x}e : τ 2. 즉, 타입추론규칙에의해 Γ λy.{v/x}e : τ 1 τ 2. 다른경우는더욱단순한귀납. 5.7.2.2 안전성증명방법 II 다음두개만으로도타입유추시스템의안전성soundness 증명이가능하다. E error를정의한다. Subject Reduction Lemma: 진행은타입을유지한다, 를증명한다. E : τ 이고 E E 이면 E : τ 이다. 왜일까? 안전성이란, 값이아닌식 E가타입이있으면, E는문제없이진행하며끝난다면그타입의값이어야한다. 값이아닌식 E가타입이있다고하자. 잘진행하는가? 그렇다, E error 로진행할수없다. 왜냐하면, 그렇게진행한다면 Subject Reduction Lemma 에의해서모순이기때문이다. error 가타입이있어야하는데 error의타입을결정하는규칙은없기때문이다. 그리고진행이타입을항상보존하므로, 값으로진행이끝나게되면그값도같은타입을가진다. 5.7.3 추론규칙의구현 위의단순타입시스템simple type system은논리시스템으로우리가바라는바를가지고있슴을증명할수있었다. 이제는구현이다. 하지만구현이간단해보이지는않는다. 다음의규칙을보면그렇다 : Γ + x : τ 1 E : τ 2 Γ λx.e : τ 1 τ 2

5.7 단순타입시스템 simple type system 163 함수의몸통 E를타입유추하려면인자의타입 τ 1 를알고있어야한다. 그러나 τ 1 은우리가최종적으로유추해야할함수타입의일부이다. 유추해내야하는것을미리알고있어야한다. 어떻게해야하나? 유추inference를포기해야하나? 프로그래머에게함수선언마다인자타입등을프로그램텍스트에써달라고강요해야하나? 이번엔놀라운방식이있다. 타입에대한연립방정식을세우고풀어가는과정이다. 그과정이놀라운이유는두가지다. 우선, 타입을자동으로유추해주는알고리즘이기때문이다. 프로그램텍스트에타입에대해서프로그래머가아무것도명시할필요가없다. 자동으로유추가된다. 다른이유는, 타입시스템을충실히구현한알고리즘이기때문이다. 충실히? 타입시스템이유추할수있는것을그알고리즘은똑같이유추해준다. 그반대도성립한다. 알고리즘이유추해내었으면타입시스템도같은것을유추해낼수있다. 서로 iff 관계로논리시스템과구현시스템이물려있다. 5.7.3.1 연립방정식의도출 주어진프로그램 E를주욱훑으면서각부품식들의타입에대한연립방정식을도출한다. 부품식이서로엉겨있는문맥을통해서그식의값이어떤타입이되야할지에대한방정식 ( 제약사항 ) 이도출된다. 그연립방정식을풀면된다. 그연립방정식에서미지수는프로그램의각부품식마다하나씩있고, 변수마다하나씩있다. 그부품식과변수의타입을뜻하는미지수이다. Example 31 예를들어, 다음의식을생각해보자. 다음프로그램 1 + (λx.x 1) 0

164 값중심의언어 모든부품식들마다번호를붙이자. }{{} 1 + (λx. }{{} x }{{} 1 ) }{{} 0 1 6 7 }{{} 4 } 5 {{ } } 3 {{ } } {{ 2 } 0 부품식 i 가가져야하는타입 α i 와변수 x 가가져야하는타입 α x 에대한방정 식 lhs =rhs 는다음과같다 : α 0 = ι α 1 = ι α 2 = ι α 3 = α β α = α x β = α 5 α = α 4 β = α 2 α 4 = ι α 5 = α 2 α 6 = α x α 6 = α β α = α 7 β = α 2 α 7 = ι 위의방정식의해는없다. α x 는 ι 이기도해야하고 (α =α x 로부터 ) ι ι 이기 도해야하므로 (α 6 =α x 로부터 ). 타입연립방정식 u 는다음과같은모습이다 : TyEqn u τ =τ 타입방정식 u u 연립 Type τ α TyVar 타입변수 ι τ τ 타입연립방정식의해 S 를치환 substitution 으로표현하면편하다. TyVar 을

5.7 단순타입시스템 simple type system 165 Type 으로바꾸는. 즉, S TyVar fin Type 인. (A fin B는 A 에서 B로가는치환들의집합이다.) Notation 9 S = u 은 S 는방정식 u 의해 model 라는뜻이다. 다음과같이정 의된다 : Sτ 1 = Sτ 2 S = u 1 S = u 2 S = {S(α)/α}u S = τ 1 =τ 2 S = u 1 u 2 S = α.u 여기서 Sα = Sι = ι τ α if α τ S otherwise S(τ τ ) = (Sτ) (Sτ ) SΓ = {x Sτ x τ Γ} 연립방정식을세우는알고리즘 V (Γ, e, τ) 는다음과같다 : V (Γ, n, τ) = τ =ι V (Γ, x, τ) = τ =τ if x : τ Γ V (Γ, E 1 + E 2, τ) = τ =ι V (Γ, E 1, ι) V (Γ, E 2, ι) V (Γ, λx.e, τ) = τ = α 1 α 2 V (Γ + x : α 1, e, α 2 ) new α 1,α 2 V (Γ, E 1 E 2, τ) = V (Γ, E 1, α τ) V (Γ, E 2, α) new α

166 값중심의언어 V (Γ, e, τ) 는옳은가? 즉, S = V (Γ, E, τ) SΓ E : Sτ 인가? Proof. E 의구조에대한귀납법으로.

5.7 단순타입시스템 simple type system 167 λx.e 인경우 : S = V (Γ, λx.e, τ) 은 = S = τ = α 1 α 2 V (Γ + x : α 1, e, α 2 ) new α 1, α 2 S = τ = α 1 α 2 S = V (Γ + x : α 1, e, α 2 ) Sτ = Sα 1 Sα 2 SΓ + x : Sα 1 E : Sα 2 ( 귀납가정 ) Sτ = Sα 1 Sα 2 SΓ λx.e : Sα 1 Sα 2 SΓ λx.e : Sτ. 다른경우도비슷하게. 5.7.3.2 연립방정식의해우리가세우는타입연립방정식을어떻게풀수있을까? 우선연립방정식의해는우리가정의한 Type이라는집합의원소여야한다. 그집합은두가지방식으로귀납적으로유한하게만들어지는 τ들의무한한집합이다. Type τ ι primitive type τ τ function type 그해는, 동일화알고리즘unification algorithm을이용해서풀수있다. A Machine-Oriented Logic Based on the Resolution PrinciplE, J.A.Robinson, Journal of ACM, Vol.12, No.1, pp.23-41, 1965. 타입방정식들 (τ =τ ) 과해공간 (Type) 은위논문의동일화unification 알고리즘으로풀수있는클래스이다. 알고리즘 U는 T = u인 T 중에서가장일반적인해most general unifier를구해준다.

168 값중심의언어 알고리즘 U 가방정식 u 에대해서해 S 를만들어냈으면 u 의다른해 T 는항상 R 로부터나온다 : T = u 이면 T = RS 인 R 이있다. 따라서, 주어진프로그램 ( 자유변수가없는식 ) E 의타입방정식을푸는알고 리즘 U : TyEqn (TyVar fin Type) 는 U(V (, E, α)) (new α) 을실행하는것이고, U 의정의는 U(u) = unify-all(u, ). 여기서 unify-all(τ =τ, S) = (unify(τ, τ ))S unify-all(u u, S) = let T = unify-all(u, S) in unify-all(t u, T ) 이며, 동일화 unification 알고리즘 unify(τ, τ ) : TyVar fin Type

5.7 단순타입시스템 simple type system 169 의정의는 unify(ι, ι) = unify(α, τ) or unifty(τ, α) = {α τ} if α does not occur in τ unify(τ 1 τ 2, τ 1 τ 2) = let S = unify(τ 1, τ 1) S = unify(sτ 2, Sτ 2) in S S unify( ) = fail 이다. 위의알고리즘은우리의단순타입시스템 simple type system 의충실한 sound & complete 구현이다. 안전 sound: U(V (Γ, e, α)) = S 이면 SΓ E : Sα 완전 complete: U(V (Γ, e, α)) = S Γ = RSΓ τ = RSα 면이 Γ E : τ

170 값중심의언어 5.7.3.3 온라인알고리즘들 타입방정식을도출하면서그때그때풀어가는알고리즘도가능하다. M : TyEnv Exp Type (TyVar fin Type)

5.7 단순타입시스템 simple type system 171 M(Γ, n, τ) = unify(ι, τ) M(Γ, x, τ) = unify(τ, τ ) if x : τ Γ M(Γ, λx.e, τ) = let S = unify(α 1 α 2, τ) new α 1, α 2 S = M(SΓ + x : Sα 1, e, Sα 2 ) in S S M(Γ, E E, τ) = let S = M(Γ, e, α τ) new α S = M(SΓ, E, Sα) in S S M(Γ, E + E, τ) = let S = unify(ι, τ) S = M(SΓ, e, ι) S = M(S SΓ, E, ι) in S S S 위의알고리즘도단순타입시스템 simple type system 의충실한 sound & complete 구 현이다. 안전sound: M(Γ, e, α) = S 이면 SΓ E : Sα M(Γ, e, α) = S 완전complete: Γ = RSΓ 면이 Γ E : τ τ = RSα 혹은, 약간다르게. W : TyEnv Exp Type (TyVar fin Type)

172 값중심의언어 W (Γ, n) = (ι, ) W (Γ, x) = (τ, ) if x τ Γ W (Γ, λx.e) = let (τ, S) = W (Γ + x : α, e) new α in (Sα τ, S) W (Γ, E E ) = let (τ, S) = W (Γ, e) (τ, S ) = W (SΓ, E ) S = unify(τ α, S τ) new α in (S S S, S α) W (Γ, E + E ) = let (τ, S) = W (Γ, e) S = unify(τ, ι) (τ, S ) = W (S SΓ, E ) S = unify(τ, ι) in (ι, S S S S) 위의알고리즘도단순타입시스템 simple type system 의충실한 sound & complete 구 현이다. 안전sound: W (Γ, e) = (τ, S) 이면 SΓ E : τ W (Γ, e) = (τ, S) 완전complete: Γ = RSΓ 면이 Γ E : τ τ = Rτ 5.7.4 안전한그러나경직된 단순타입시스템이안전하기는하지만아쉬움이많다. 완전하지못하다. 타입시스템을통과한 ( 타입유추에성공한 ) 프로그램은실행중에타입오류가발생하지않는다는것이보장된다. 하지만, 타입오류없이잘실행될수있는모든프로그램이단순타입시스템을통과하는것은

5.7 단순타입시스템 simple type system 173 아니다. 안전sound하지만빠뜨리는프로그램들이있는incomplete 것이다. 빠뜨리는게특히많다. 유연하지못하다. 인자타입에상관없이실행되는함수들이많이있다. 그런함수들이단순타입시스템을통과하면서는하나의타입으로고정된다. 다양한타입의인자에적용되는경우가프로그램에있다면단순타입시스템을통과할수없다. 다음에예들이있다. Example 32 다음의프로그램을보자. 단순타입시스템을통과할수없는, 하지만잘실행될수있는프로그램이다. (* polymorphic functions *) let I = \x.x const = \n.10 in I I; const 1 + const true end Example 33 다음의프로그램도단순타입시스템에서는타입유추가불가능 한경우다. 하지만문제없이실행되는프로그램이다. (* S K I combinators *) let I = \x.x K = \x.(\y.x) S = \x.(\y.(\z.(x z)(y z))) in S (K (S I)) (S (K K) I) 1 (\x.x+1) end Example 34 쌍을다루는언어로단순타입시스템이확장된다고해도, 타입 시스템을통과하지못하는유용한프로그램을쉽게만나게된다.

174 값중심의언어 (* polymorphic swap *) let swap = \order_pair. if order_pair.1 order_pair.2 then order_pair.2 else (order_pair.2.2, order_pair.2.1) in swap(\pair.(pair.1 + 1 = pair.2), (1,2)); swap(\pair.(pair.1 or pair.2), (true, false)) end 5.7.5 M3 로확장하기 5.7.5.1 재귀함수 재귀함수는 Y 컴비네이터 Y combinator 를통해서표현할수있었다. Y 컴비네 이터는 λf.(λx.f (x x))(λx.f (x x)) 이고, 그핵심에는자신을인자로받는함수의적용 x x 이있다. 단순타입시스템에서는함수가자신을인자로받는식은타입유추가될 수없다 : }{{} x }{{} x 1 2 }{{} 0 에서각부품식 i 가가져야하는타입 α i 를따져보면 α 1 = α x α 1 = α β α 2 = α x α 2 = α 이되는데, 결국 α β =α를만족하는타입을 Type에서는찾을수없다. 동일화unification 알고리즘은위의양변을같게만드는 α와 β를찾는것에실패한다. 따라서, 단순타입시스템이갖추어진언어에서는재귀함수를 Y 컴비네이

5.7 단순타입시스템 simple type system 175 터로표현해서는타입시스템을통과할수없다. 재귀함수 rec f λx.e 는더이상설탕이아니다. 타입유추규칙은간단하다 : Γ + f : τ 1 τ 2 λx.e : τ 1 τ 2 Γ rec f λx.e : τ 1 τ 2 Exercise 4 안전성soundness 증명도위의경우에대해서기존의얼개 (Progress Lemma와 Subject Reduction Lemma) 안에추가하면된다. Exercise 5 오프라인알고리즘과온라인알고리즘은어떻게확장될수있을