프로그래밍 언어를 다루기 시작할 때 우리는 보통 "문자열"부터 떠올린다. 그러나 의미론을 이야기하는 자리에서 문자열은 너무 거칠고 모호하다. 괄호 짝이 맞는지, 공백이 어디에 있는지 같은 표면적 사건은 의미와 무관하다. 우리에게 필요한 것은 표현이 가지는 구조 그 자체이며, 이를 정제해 다루는 도구가 추상 구문이다.
구체 구문(concrete syntax)이 시각적 표기법이라면, 추상 구문(abstract syntax)은 의미를 운반하는 골격이다. 우리는 표현을 트리로 본다. 각 노드는 어떤 연산자를 들고 있고, 그 아래로 정해진 개수의 자식이 매달려 있다. 즉, 표현은 "이 연산자가 그 아래에 무엇을 거느리는가"라는 정보의 재귀적 누적물이다.
이러한 트리를 형식화하기 위해 우리는 분류(sort)와 연산자 시그니처를 정한다. 분류 σ에 속한 표현 e가 있다고 할 때, 그것은 단일 변수이거나, 어떤 연산자 o를 머리에 두고 정해진 분류의 인자들 e₁, …, eₖ를 받은 형태이다.
변수는 표현의 "구멍"이다. 그 자리에 무엇을 끼워 넣을지 아직 정해지지 않았다는 표시이며, 다른 어떤 노드와도 다르게 다루어야 한다. 추상 구문 트리가 갖는 가치는, 바로 이 변수와 그 변수를 구속(bind)하는 연산자가 트리 구조 안에서 명확히 분간된다는 점에 있다.
이름이 같은 두 변수가 사실은 서로 다른 구속자에 묶여 있다면 그것은 우연한 동명이인일 뿐이다. 우리는 이 차이를 구문 차원에서 제대로 잡아내기 위해 α-동치라는 동등 관계를 도입한다. 즉, λx.x와 λy.y는 — 어떤 텍스트 편집기로 보아도 다르지만 — 추상 구문의 시선에서 같은 것이다.
이러한 직관을 정식화한 것이 구속 트리(ABT)다. ABT에서 한 연산자는 자식마다 "여기에서 새로 묶는 변수의 개수"를 선언한다. 예컨대 람다 추상은 한 자식 위치에서 변수 하나를 묶는다고 명시한다. 트리 위의 자유 변수와 묶인 변수는 이 선언에 따라 산출되며, 치환과 α-변환 같은 조작은 모두 이 골격 위에서 정의된다.
한 줄 요약: 추상 구문이란, "괄호와 공백을 잊고 나면 무엇이 남는가"에 대한 깔끔한 답이다.
추상 구문은 의미론의 무대이다. 동작 의미와 정적 의미는 모두 이 트리 위에서 진행되는 귀납적 해설이다. 트리가 잘 정의되어야 그 위의 정의들이 잘 정의될 수 있다. 그러므로 우리는 다음 장에서 "잘 정의된 귀납"이라는 도구를 다듬는다.
언어를 다루는 우리는 끊임없이 "어떤 대상이 이 모임에 속하는가?"라는 질문을 던진다. 자연수가 그렇고, 잘 형성된 표현이 그렇고, 타입 판단이 그렇다. 이 모임을 정의하는 가장 깔끔한 도구가 귀납이다. 구체적으로는 규칙의 무리로 무엇이 그 모임에 들어갈 자격을 가지는가를 단계적으로 명시한다.
판단(judgment)이란 "이 대상은 이러이러하다"라는 진술의 형식이다. 가령 "n nat"이라는 판단은 n이 자연수임을 주장한다. 우리는 이 판단이 성립할 수 있는 조건들을 추론 규칙으로 풀어낸다.
zero natn natsucc(n) nat규칙은 윗줄에 전제(premise), 가운데 가로선, 아래에 결론(conclusion)을 둔 그림표로 적는다. 전제가 없는 규칙은 공리(axiom)에 해당한다.
한 판단이 성립한다는 사실은 막연한 선언이 아니라 도출 트리로 뒷받침된다. 트리의 잎은 공리이고, 가지는 규칙의 적용이다. 즉 "succ(succ(zero)) nat"이 참이라는 말은, 그 뿌리에 해당 판단이 놓이고 두 번의 succ-규칙과 한 번의 zero-공리로 짜인 트리가 실제로 존재한다는 말이다. 도출이 있어야 판단이 있다. 그 반대 또한 우리가 강제로 그렇게 약속한 결과다.
귀납적 정의가 명시하는 모임은, 모든 규칙에 대해 닫혀 있는(closed) 모임 가운데 가장 작은 것이다. 이 "가장 작음"이 결정적이다. 그것은 우리에게 두 가지 무기를 제공한다. 첫째, 규칙 귀납(rule induction): 어떤 성질 P가 규칙들에 대해 보존된다면, 그 모임의 모든 원소는 P를 가진다. 둘째, 재귀적 정의: 함수의 값을 규칙별로 지정해도 일관된 정의를 얻을 수 있다.
예를 들어 자연수 위의 덧셈은 다음의 두 절(節)로 정의된다. add(zero, m) = m, add(succ(n), m) = succ(add(n, m)). 정의가 잘 끝남(termination)은 첫 인자에 대한 규칙 귀납으로 즉시 정당화된다.
이런 형식주의가 답답해 보일 때가 있다. "그냥 자연수잖아!" 그러나 우리가 다룰 대상은 곧 자연수에 그치지 않는다. 타입을 가지는 표현, 환경에 따라 평가되는 항, 효과를 추적하는 판단. 이 모든 것이 같은 골격으로 정의된다. 한 번 잘 다듬어 둔 귀납적 정의의 도구는, 이후 장에서 거의 무한히 재활용될 것이다.
규칙 귀납은 형식론자의 만능 드라이버다. 어디 하나 꽉 안 조여진 곳을 발견했다면, 십중팔구 이 도구로 풀린다.
앞 장의 판단은 모두 "닫혀 있는" 진술이었다. 그러나 실제 언어를 다룰 때 우리는 "만약 x가 자연수라면 x + 1도 자연수다"처럼, 자유 변수에 대한 가정을 짊어진 판단을 다루어야 한다. 이런 판단을 가정적 판단(hypothetical judgment)이라 부른다. 또한 임의의 변수 이름을 한꺼번에 다루기 위한 일반적 판단(general judgment)도 함께 등장한다.
유한한 가정의 묶음을 컨텍스트 Γ라고 적는다. 변수와 그에 따르는 분류 또는 타입의 쌍이 콤마로 이어진 목록이다. 가정적 판단은 다음의 모양을 가진다.
Γ ⊢ J
해석은 단순하다. 컨텍스트 안의 가정들이 모두 성립한다고 받아들인다면, 결론 J도 성립한다는 뜻이다. 이때 Γ가 비면 우리는 닫힌 판단으로 돌아온다. 즉 · ⊢ J는 J 그 자체와 같다.
가정적 판단은 그 자체가 다시 추론 규칙으로 빚어진다. 가장 기본적인 것은 가정 규칙이다.
(x:τ) ∈ ΓΓ ⊢ x : τ그리고 컨텍스트의 동작에 관한 구조 규칙(structural rules)이 있다. 약화(weakening)는 새로운 가정을 더 추가해도 기존의 도출은 여전히 유효함을 말한다. 교환(exchange)은 가정의 순서를 뒤섞을 수 있음을, 수축(contraction)은 동일한 가정이 여러 번 나오면 한 번으로 줄여도 좋음을 말한다. 마지막으로 절단(substitution)은 가장 무거운 규칙이다. Γ ⊢ d : τ이고 Γ, x:τ ⊢ J라면 Γ ⊢ [d/x]J가 성립한다. 즉 가정 자리에 실제 도출을 끼워 넣을 수 있다.
한편 우리는 종종 어떤 변수 이름이 무엇이든 상관없는 진술을 다룬다. 이를테면 "임의의 변수 x에 대해 x = x"가 그렇다. 이런 판단을 일반적 판단이라 부르며, ∀-처럼 양화의 형식을 띈다. 형식적으로는 도출이 변수 이름의 선택과 무관하게 동일한 형태를 띄는 것을 보장한다. 일반적 판단과 가정적 판단을 함께 다루면 우리는 거의 모든 언어 정의에 필요한 표현력을 얻는다.
가정 규칙·약화·절단이라는 세 축은 그저 편의를 위한 장식이 아니다. 이들은 의미론이 합성적으로 이루어질 수 있게 만든다. 부분에 대한 의미가 정해지면, 그것을 가정으로 받아들인 더 큰 표현의 의미가 자동으로 정해진다는 보장이 절단 규칙이다. 이후 4장 이후의 타입 시스템은 사실상 이 세 가지 위에서 연주되는 변주곡일 뿐이다.
절단 정리(cut elimination)가 증명론의 만년 베스트셀러인 이유: 모든 어려운 일이 결국은 그 한 줄로 환원되기 때문이다.
정적 의미론은 프로그램이 실행되기 전에, 즉 한 줄도 돌리기 전에 그 프로그램에 대해 무엇을 단언할 수 있는가를 다룬다. 이 단언의 핵심 도구가 타입이며, 타입 시스템은 표현이 어떤 타입을 가지는지를 형식적으로 결정한다. 이 장에서는 작은 표현 언어 E를 도입하고, 그 위에 타입을 부여하는 규칙을 세운다.
언어 E는 두 가지 분류를 가진다. 타입 τ와 표현 e이다. 타입은 자연수 타입 num과 문자열 타입 str 정도로 두자. 표현은 변수 x, 수치 리터럴 num[n], 문자열 리터럴 str[s], 덧셈 plus(e₁; e₂), 이어붙임 cat(e₁; e₂), 길이 len(e), 그리고 지역 정의 let(e₁; x.e₂)로 충분하다. 마지막 항은 "값을 묶고 그 변수의 사정거리 안에서 본문을 평가"하는 구속자이다.
타입 부여 판단은 다음의 모양이다.
Γ ⊢ e : τ
Γ는 변수의 타입 가정 묶음이다. 규칙은 표현의 모양을 따라간다.
(x:τ) ∈ ΓΓ ⊢ x : τΓ ⊢ e₁ : num Γ ⊢ e₂ : numΓ ⊢ plus(e₁; e₂) : numΓ ⊢ e : strΓ ⊢ len(e) : numΓ ⊢ e₁ : τ₁ Γ, x:τ₁ ⊢ e₂ : τ₂Γ ⊢ let(e₁; x.e₂) : τ₂타입 부여 판단에 대해 약화·교환·치환이 모두 성립한다. 특히 치환 보조정리(substitution lemma)는 "Γ ⊢ d : τ이고 Γ, x:τ ⊢ e : σ이면 Γ ⊢ [d/x]e : σ"이라 말한다. 또한 표현 한 개에 대해 타입은 유일하게 결정된다. 즉 Γ ⊢ e : τ이고 Γ ⊢ e : τ'이면 τ = τ'이다. 이 유일성은 후속 장에서 보존 정리를 증명할 때 결정적으로 쓰인다.
타입 시스템은 일종의 보수적 검열관이다. 의심스러우면 통과시키지 않는 쪽이 안전하다.
아직 우리는 e가 실행되면 무슨 일이 일어나는지 정의하지 않았다. 정적 의미론은 그것 없이도 의미가 있다. "plus(num[3]; str["네"])" 같은 표현은 어떤 실행을 정의하기도 전에 거부할 수 있고, 거부해야 한다. 다음 장에서 우리는 동작을 정의하고, 그 다음 장에서 두 의미론이 서로 어긋나지 않음을 증명할 것이다.
정적 의미론이 "이 표현은 합당한가?"를 다루었다면, 동적 의미론은 "이 표현이 실행되면 무슨 일이 벌어지는가?"를 다룬다. 우리는 표현을 한 단계씩 변형하는 작은 단계 의미론(small-step semantics)을 채택한다. 이는 추상 기계 위에서 한 발자국씩 움직이는 그림과 잘 어울린다.
먼저 어떤 표현이 더 이상 줄어들지 않는 "최종 상태"인가를 규정해야 한다. 이를 값 판단 e val이라 적는다. 우리의 작은 언어에서는 수치 리터럴 num[n]과 문자열 리터럴 str[s]가 값이다.
num[n] val다음으로 한 걸음 진행 판단 e ↦ e'을 정의한다. "표현 e는 한 단계 뒤 e'가 된다"는 의미이다. 두 종류의 규칙이 있다. 어딘가에 묻혀 있는 부분식부터 우선 평가하라는 합동 규칙(congruence)과, 진짜로 일을 해내는 지시 규칙(instruction)이다.
e₁ ↦ e₁'plus(e₁; e₂) ↦ plus(e₁'; e₂)e₁ val e₂ ↦ e₂'plus(e₁; e₂) ↦ plus(e₁; e₂')plus(num[m]; num[n]) ↦ num[m+n]let(e₁; x.e₂)는 두 가지 자연스러운 해석을 갖는다. 이름 호출(call-by-name)이라면 e₁을 그대로 본문에 치환하고, 값 호출(call-by-value)이라면 e₁을 먼저 값으로 만든 뒤 치환한다. 우리는 후자를 채택한다.
e₁ vallet(e₁; x.e₂) ↦ [e₁/x]e₂이렇게 정의된 진행 관계는 결정적(deterministic)이다. 즉 임의의 e에 대해 한 단계 뒤로 가는 결과는 많아야 하나이다. 합동 규칙들이 평가 순서를 한 가지로 못박기 때문이다. 또한 우리는 정상화되거나 막혀 있는(stuck) 두 가지 종착점을 상상할 수 있다. 값에 도달하면 정상 종료, 그러나 어떤 규칙도 적용되지 않고 값도 아닌 상태에 갇히면 그것이 막힘이다.
막힘은 컴퓨터과학의 미아(迷兒)다. 이 아이를 만들지 않는 것이 타입 시스템의 가장 절박한 약속이다.
그렇다면 "잘 타이핑된 프로그램은 결코 막히지 않는다"는 약속이 정말 지켜지는가? 이 한 문장이 다음 장의 주제다.
정적 의미론과 동적 의미론을 따로 정의해 두었으면, 둘이 서로 잘 어울리는지를 점검할 차례다. 어울림의 표준은 두 정리로 요약된다. 진행(progress)과 보존(preservation). 이 두 정리를 함께 일컬어 "타입 안전성(type safety)"이라 부르며, 그 의미는 "잘 타이핑된 프로그램은 막히지 않는다"이다.
편의를 위해 모든 판단은 닫힌 표현 위에서, 즉 · ⊢ e : τ의 형태로 둔다. 두 정리는 다음과 같다.
보존. · ⊢ e : τ이고 e ↦ e'이면, · ⊢ e' : τ이다.
진행. · ⊢ e : τ이면, e val이거나 어떤 e'에 대해 e ↦ e'이다.
요컨대 한 걸음을 걸어도 타입은 변치 않으며(보존), 막히지 않는다(진행). 두 정리를 합치면 잘 타이핑된 프로그램은 영원히 막히지 않거나 끝내 값에 도달함을 얻는다.
두 정리 모두 규칙 귀납의 표준 응용이다. 보존 정리는 e ↦ e'의 도출에 대한 귀납으로 진행한다. 합동 규칙들에서는 부분식의 타입이 보존된다는 가설을 가져다 그대로 쓰면 된다. 지시 규칙에서는 종종 별도의 보조정리가 필요하다. 가장 자주 쓰이는 것이 치환 보조정리이다. 예컨대 let(v; x.e₂) ↦ [v/x]e₂의 경우, · ⊢ v : τ₁과 x:τ₁ ⊢ e₂ : τ₂로부터 · ⊢ [v/x]e₂ : τ₂를 끌어내는 것이 핵심이다.
진행 정리는 타입 부여의 도출에 대한 귀납으로 진행한다. 변수의 경우는 Γ가 비어 있다는 가정에 의해 비어 있는 케이스이고, 리터럴은 곧바로 값이며, 합성적 표현들에서는 부분식이 값인 경우와 그렇지 않은 경우로 나누어 합동 규칙 또는 지시 규칙을 적용하면 된다.
진행 증명을 매끈하게 만드는 도구가 표준 형식 보조정리(canonical forms lemma)이다. "닫힌 값 v가 num이면 v는 어떤 n에 대해 num[n] 모양이다"와 같이, 타입에 따라 값의 모양을 좁혀준다. 이 보조정리는 타입 시스템을 작성한 사람이 의도한 것이 실제로 동적으로도 성립하는지 확인하는 정직한 거울이다.
진행 정리가 한 번 깨지면, 그것은 거의 항상 표준 형식 보조정리의 어딘가가 어긋났다는 신호다.
타입 안전성은 단지 깔끔한 정리가 아니다. 그것은 언어 설계자가 사용자에게 거는 계약이다. "내가 통과시킨 프로그램은 결코 정의되지 않은 행동에 빠지지 않는다." 이 계약을 지키지 못하는 시스템은 — 아무리 표현력이 풍부해 보이더라도 — 전제로부터 다시 살펴볼 필요가 있다. 다음 장에서는 진행을 한꺼번에 보지 않고, 시작에서 끝까지 한 번에 평가하는 또 다른 시각을 도입한다.
앞 장까지의 동적 의미론은 한 발씩 옮기는 카메라였다. 그러나 어떤 분석에서는 한 발씩 보는 일이 오히려 시야를 흐린다. 우리는 종종 "이 표현은 어떤 값으로 평가되는가?"만을 단번에 묻고 답하고 싶다. 이런 시각이 평가 동역학(evaluation dynamics), 흔히 대형 단계 의미론(big-step semantics)이라 불린다.
평가 판단은 다음의 모양을 가진다.
e ⇓ v
의미는 단순하다. 표현 e는 평가되어 값 v가 된다. 규칙은 다시 표현의 모양을 따라간다.
num[n] ⇓ num[n]e₁ ⇓ num[m] e₂ ⇓ num[n]plus(e₁; e₂) ⇓ num[m+n]e₁ ⇓ v₁ [v₁/x]e₂ ⇓ v₂let(e₁; x.e₂) ⇓ v₂여기에는 "한 걸음" 같은 개념이 없다. 부분식이 값에 도달했다는 가설들을 모아, 전체가 어떤 값에 도달하는지를 한꺼번에 결론짓는다.
두 의미론은 같은 언어를 다루는 한, 같은 결과를 내야 한다. 형식적으로 다음의 등가가 성립한다.
e ⇓ v ⇔ e ↦* v이고 v val
여기서 ↦*는 한 걸음의 반사·이행적 폐포이다. 한쪽 방향(⇒)은 ⇓의 도출에 대한 귀납으로, 다른 쪽 방향(⇐)은 ↦*의 길이에 대한 귀납으로 증명된다. 후자에서는 한 걸음을 평가에 합치는 보조정리, 즉 "e ↦ e'이고 e' ⇓ v이면 e ⇓ v"가 결정적인 역할을 한다.
대형 단계 의미론은 컴팩트하고, 합성적 추론에 자연스럽다. 그러나 그것이 잘 작동하는 곳은 종결성이 보장된 단편이다. 평가 판단은 본질적으로 "값에 도달했다"를 전제로 결론을 짓기 때문에, 발산하는(diverging) 표현이나 효과적 동작을 직접 다루기에는 어색하다. 작은 단계 의미론은 그런 문맥에서도 침착하다. 한 걸음씩만 약속하므로, 끝나지 않는 계산 자체를 무한 도출 시퀀스로 표현할 수 있다.
한쪽은 결과만 보고, 한쪽은 과정을 본다. 둘 다 필요하다 — 인생도 언어도.
이로써 우리는 정적 의미론, 동적 의미론, 그리고 둘의 정합성, 그리고 같은 동적 의미론을 다른 시각으로 보는 두 가지 방식까지 갖추었다. 다음 부에서 우리는 이 도구들 위에 함수, 합타입, 곱타입, 재귀 같은 본격적인 구문을 얹어 가며, 이 골격이 얼마나 멀리까지 견디는지 시험할 것이다.