48 문법의 증명 — 글이 나무를 하나로 정한다

먼저 알아야 할 것

3장 겉모습 · 이름이 열고 점이 닫으며, 개행은 공백이다

8장 식 · 전위 표기에는 우선순위가 없다

39장 수학 도구상자 · 집합과 관계 — “같다” 를 무엇으로 정하나

돌아보기

3장에서 poly 의 return 은 두 줄에 걸쳐 있었지만 한 폼이었다. 무엇이 그 폼을 닫았고, 개행은 무슨 일을 했는가?

답. 둘째 줄 끝의 마침표가 닫았다. 개행은 스페이스와 똑같은 공백이라 아무것도 닫지 않았다. 그래서 줄을 어디서 나누어도 뜻이 같았다. 이 장은 그런 표면의 성질이 왜 증명의 대상이 되는지를 다룬다.

이 장의 필요성과 맥락

여기까지의 증명은 의미였다 — 프로그램이 무엇을 하는가. 이 장은 표면이다 — 프로그램이 어떻게 생겼는가. 문법에 증명이 필요한 까닭은 실제로 겪은 일 때문이다. 파서가 . 로 폼을 조각내고 뒤 단계가 말없이 다시 붙이고 있었다 — 두 층이 서로 다른 문법을 믿었고, 그 차이가 결함으로 나왔다. “한 뜻에 한 표기” 라는 원칙이 겉모습의 취향으로 남지 않으려면, 두 표기가 같은 나무를 만든다는 것을 기계가 지켜야 한다.

이 장이 끝나면

나무를 글로 찍는 함수와 글을 나무로 읽는 작은 기계를 알게 된다. 찍은 글을 읽으면 그 나무가 나온다는 정리, 괄호가 꾸밈이라는 정리, 점의 수가 검사합이라는 정리, end 가 폼을 닫지 않는다는 정리, 블록의 결합법칙을 예제로 확인한다. 같은 뜻이 증명돼도 철자를 두지 않은 개행 닫기, 언어에서 뺀 규칙과 함께 뺀 정리, 그리고 이 정리가 실제 처리기에 대해 말하지 않는 것도 보게 된다.

이 장에서 답할 질문

이 정리가 있으면 실제 파서가 옳다고 믿어도 되는가?
C 에 우선순위 규칙이 수십 줄인데, 이 장의 증명은 왜 이렇게 짧은가?

48.1 글과 나무#

증명하려는 것을 말하려면 두 가지를 정해야 한다. 나무는 프로그램의 구조다. 폼은 이름 하나와 인자들이고, 인자는 잎(리터럴)이거나 폼이거나 블록이다. 변수 a. 는 인자가 없는 폼이다. 글은 토큰의 열이다 — 잎, 여는 이름, 점, do, end, 괄호. 나무를 글로 찍는 함수 print 는 폼을 “이름, 인자들, 점” 으로, 블록을 “do, 폼들, end” 로 찍는다.

글을 나무로 읽는 쪽은 작은 기계다. 열린 것들을 쌓아 두는 더미 하나를 갖고, 토큰마다 한 가지 일을 한다. 이름을 만나면 폼을 연다. 점을 만나면 더미 맨 위의 폼을 닫는다 — 맨 위가 폼이 아니면 실패한다. do 는 블록을 열고, end 는 맨 위가 블록일 때만 그것을 닫는다. 이 기계에는 인자 수의 표가 없다. 이 장의 정리들은 모두 이 기계에 대한 것이다.

48.2 읽기는 하나로 정해진다#

examples/ch48/closers.low

module closers .
rem run: one_line 4
rem run: spread 4

fn one_line input x u64 . output u64 .
  requires le x. 1000 . .
do
  return add mul x. x. . add x. 1 . . .
end .

rem 인자를 여러 줄에 늘어놓아도 표시가 필요 없다 --- 개행은 공백이다
fn spread input x u64 . output u64 .
  requires le x. 1000 . .
do
  return add
    mul x. x. .
    add x.
         1 . . .
end .

실행 결과

$ lowentc --run one_line closers.low 4
one_line(4) = 21
$ lowentc --run spread closers.low 4
spread(4) = 21

one_line 은 안쪽 폼 둘이 저마다 제 점으로 닫히고, 마지막 점이 바깥 폼을 닫는다. spread 는 같은 폼을 네 줄에 늘어놓았는데 아무 표시가 필요 없다. 개행은 토큰이 아니기 때문이다. 두 op 의 답이 같다.

 return add mul x. x. . add x. 1 . . .      return add
                                                mul x. x. .
                                                add x.
                                                     1 . . .
 둘 다 같은 나무가 된다:
                 add
            ┌─────┴─────┐
           mul         add
          ┌─┴─┐       ┌─┴─┐
          x   x       x   1

수학. 정리 G1(LowentBlock.v 의 parse_print)

forall ts, parse (prints ts) = Some (map erase ts). 나무들을 찍은 글을 읽으면 바로 그 나무들이 나온다(erase 는 꾸밈인 괄호를 걷어 낸다). 따름정리 form_ends_at_its_stop 은 폼 하나에 대해 같은 말을 한다 — 인자가 몇 개든 읽기가 같다. 폼의 끝을 정하는 것은 점이지 인자 수가 아니다.

이 정리가 1.8 판의 설계 결정을 받친다. 1.7 판까지는 op 마다 받는 인자 수가 폼의 끝을 정했고, 그래서 글을 읽으려면 그 op 의 선언을 알아야 했다. 지금은 글만으로 나무가 정해진다. 편집기도 서식기도 선언을 읽지 않고 같은 나무를 얻는다.

수학. 정리 G2(parens_are_decoration)

forall t rest st, run (print (Group t) ++ rest) st = run (print t ++ rest) st. 폼을 괄호로 싸도, 어느 자리에서든 기계는 같은 상태에 이른다. 괄호는 뜻을 바꾸지 않는다.

수학. 정리 G3(one_text_one_tree)

prints ts = prints us -> map erase ts = map erase us. 두 나무가 같은 글이 되면, 괄호를 뺀 두 나무는 같다. 한 글에 두 뜻이 없다.

48.3 점의 수는 검사합이다#

수학. 정리 G4(stops_match_opens · missing_stop_is_refused · extra_stop_is_refused)

찍은 글에서 여는 이름의 수와 점의 수는 같다. 폼을 닫는 점이 빠진 글은 읽기가 실패하고(E-DOT-MISSING), 닫힌 것 뒤에 점을 하나 더 적은 글도 실패한다(E-CLOSER-EXTRA).

수학. 정리 G5(end_does_not_close_a_form)

블록 안에 열린 폼이 남은 채 end 가 오면 읽기가 실패한다. do … end 는 짝인 괄호라서 end 는 자기 do 만 닫고, 안에 열린 폼을 대신 닫아 주지 않는다. 블록을 가진 폼은 end 뒤의 점으로 닫힌다(while c. do … end .).

점 하나를 빠뜨린 실수가 파일의 나머지를 조용히 삼키지 못하는 까닭이 G5 다. 열린 폼은 블록의 end 를 넘지 못하므로 실수는 그 블록 안에서 멈춘다.

48.4 블록은 결합적이다#

문장을 이어 붙이는 일에는 두 성질이 있다. 이어 붙이는 방식이 묶는 순서와 무관하고(결합법칙), 빈 블록은 아무것도 아니다(항등원 — 덧셈에서 0 이 하는 일). 이 둘을 갖는 구조를 모노이드라 한다. 목록을 이어 붙이는 것이 대표적인 모노이드이고, 프로그램의 문장 나열이 정확히 그 구조다.

두 표기가 “같은지” 를 말하려면 기준이 필요하다. 각 나무를 평평한 문장 나열로 보내는 함수 denote 를 두고, 결과가 같으면 같다고 한다.

수학. 정리 G6(block_assoc · nested_block_flattens · empty_block_is_nothing)

블록 안의 블록은 제자리에서 펼쳐도 뜻이 같고, 빈 블록은 아무것도 더하지 않는다.

개행은 이 모델의 글에 없다. 한때는 개행도 닫개였고 그 규칙의 정리도 Qed 였다. 그래도 두지 않았다. 개행이 닫으면 줄바꿈이 의미가 되어 긴 줄을 나누는 것만으로 프로그램이 바뀐다. 같은 뜻임이 증명된다고 그 철자를 두어야 하는 것은 아니다. 쉼표·줄잇기에 붙어 있던 정리들, 그리고 1.7 판의 “문장 하나는 문장 하나짜리 블록이다” · “닫개 둘이 같은 일을 한다” 도 모두 Qed 였지만, 그 규칙들이 언어에서 빠지면서 정리도 함께 뺐다. 지금 , 와 ; 는 E-VOCAB-REMOVED 로 거절된다. 죽은 규칙을 모형화한 정리를 남겨 두면 증명된 문서가 없는 규칙을 말하게 된다.

이 파일의 증명은 길지 않다. 뼈대는 나무의 모양을 따라가는 귀납 한 번이다(G1 의 보조정리). 값은 증명의 어려움이 아니라 명제를 골라 적었다는 데 있다. “읽는 기계에 인자 수의 표가 없다” 를 적어 두면, 누가 어떤 낱말 하나를 특별 취급했을 때 증명이 깨진다. 문법은 “여기만 예외를 두면 편한데” 로 조용히 표류하는 층이고, 정리가 그 표류를 잡는다. 막는 것은 사용자의 결함이 아니라 컴파일러의 결함이다.

문. 이 정리가 있으면 실제 파서가 옳다고 믿어도 되는가?

답. 아니다. 모델은 나무를 만드는 작은 함수들이고, 실제 파서는 그보다 훨씬 크다. 둘의 대응은 시험이 받친다. 그리고 두 백엔드 대조는 VM 과 네이티브를 비교하지만 둘은 같은 앞단을 지나므로, 파서가 틀리면 둘 다 똑같이 틀린다. 파서를 이 모델과 직접 대조하려던 시도는 모델이 실제 문법보다 작아서 결론을 낼 만큼의 짝을 얻지 못했다. 앞단은 이 언어의 검증에서 가장 약한 이음매다(50장).

문. C 에 우선순위 규칙이 수십 줄인데, 이 장의 증명은 왜 이렇게 짧은가?

답. 이 언어의 식은 전위 표기라 연산자 우선순위가 없다(expr 섬은 따로 다룬다, 8장). 우선순위가 없으니 “이 표기가 어떤 나무가 되는가” 에 답할 경우가 적다. 설계가 증명을 쉽게 만든 사례다. 그 대신 증명이 짧다고 값이 작은 것은 아니다 — 명제를 적어 두었다는 것 자체가 표류를 막는다.

흔한 오해. 줄을 바꾸면 문장이 끝난다

개행은 공백이다. closers.low 의 spread 는 한 폼을 네 줄에 늘어놓았는데 아무 표시도 없이 one_line 과 같은 나무가 된다. 폼을 끝내는 것은 닫개(.) 뿐이다. 그래서 마침표를 빠뜨리면 다음 줄이 앞 폼에 이어 붙어 엉뚱한 진단이 나오고, 긴 식을 여러 줄로 나누어도 뜻이 바뀌지 않는다. 개행을 닫개로 만드는 규칙도 증명은 되지만 두지 않은 까닭이 바로 이 둘째 성질이다.

48.5 흔한 실수#

반례. 줄 끝의 마침표를 빠뜨린다

examples/ch48/mistake_noperiod.low

module mistake_noperiod .
rem expect: E-DOT-MISSING

fn total input a u64 . input b u64 . output u64 .
  requires le a. 1000 . .
  requires le b. 1000 . .
do
  rem ✘ 이 줄 끝의 마침표를 빠뜨렸다
  var s u64 add a. b. .
  set s. mul s. 2 . .
  return s. .
end .

실행 결과

$ lowentc --check mistake_noperiod.low
10:3 E-DOT-MISSING: a stop `.` must close the binding — found `set` (RFC-0142: a name opens, a stop closes; a variable is written `a.`)

진단은 마침표를 빠뜨린 줄이 아니라 다음 줄을 가리킨다. 개행은 아무것도 닫지 않는다. 그래서 var 문장이 열린 채로 다음 줄의 set 을 만났고, 도구는 “바인딩을 닫는 점이 없다” 고 말한다. 줄 번호보다 한 줄 위를 먼저 본다. 이 진단이 헷갈려도 규칙은 바뀌지 않는다. 줄이 문장을 끝낸다면 긴 식을 나누는 것만으로 뜻이 바뀐다.

반례. C 처럼 ; 로 닫는다

examples/ch48/mistake_semicolon.low

module mistake_semicolon .
rem expect: E-VOCAB-REMOVED
fn twice input a u64 . output u64 .
  requires le a. 1000 . .
do
  rem ✘ C 처럼 쌍반점으로 닫는다
  return mul a. 2 . . ;
end .

실행 결과

$ lowentc --check mistake_semicolon.low
7:23 E-VOCAB-REMOVED: `;` was a THIRD spelling of the closer `.` (the lexer literally emitted a DOT for it) — one meaning, three spellings, and SPEC-002 §2.5 forbids synonyms. It only survived inside the old interpreter's second language. Write `.`

; 는 예전에 마침표의 셋째 철자였다. 한 뜻에 철자가 셋이면 읽는 사람이 차이를 찾게 되므로 뺐고, 이제 E-VOCAB-REMOVED 로 거절한다. 조용히 받아들이지 않는 것은, 파싱은 되는데 아무 뜻이 없는 낱말이 가장 찾기 어려운 함정이기 때문이다.

48.6 증명하지 않은 것#

실제 파서가 이 모델이라는 보장이 없다. 모델은 나무를 만드는 작은 함수들이고 실제 파서는 훨씬 크다. 대응은 단위 시험과 회귀 시험이 받친다.
denote 는 평평한 나열이다. 위치 정보·주석·오류 복구를 모델링하지 않았다. 그러니 “같은 나무” 는 구조가 같다는 뜻이지 진단의 품질까지 같다는 뜻이 아니다.
어휘(토큰) 층은 별도다. 붙은 점 a. 와 띄운 점 a . 가 같은 토큰 열이 되는지는 렉서 시험의 몫이다.
모델은 문법의 뼈대만 담는다. 짓는 자리의 이름(let x · input n) · 타입 · 패턴은 모델에서 잎이고, op 머리의 절 · else 사슬 · expr 섬의 중위 연산자는 모델에 없다. 그 모양은 명세의 부록 A.10 이 정한다.
1.9 판이 더한 것은 모델을 바꾸지 않는다. break 2 . 의 수는 리터럴이고 matrix 2 3 4 u32 는 타입이라 둘 다 잎이다. 인자가 모두 잎인 폼이 적은 그대로 읽힌다는 것을 정리 하나로 적어 두었다(leaf_arguments_read_back). 어느 되풀이로 가는가, 모양이 같은가는 문법의 일이 아니라서 이 증명이 말하지 않는다.

복습 정리

나무를 찍은 글을 읽으면 그 나무가 나온다(G1) — 읽는 기계에 인자 수의 표가 없으므로, 폼의 끝은 글만으로 정해진다. 괄호는 꾸밈이고(G2) 한 글에 두 뜻이 없다(G3). 점의 수는 검사합이라 하나 모자라도 하나 남아도 읽기가 실패하고(G4), end 는 폼을 닫지 않는다(G5). 블록 안의 블록은 제자리에서 펼쳐진다(G6). 개행 닫기는 증명돼도 두지 않았고, 언어에서 뺀 규칙의 정리는 함께 뺐다. 실제 처리기가 이 모델이라는 보장은 시험이 받친다.

← 이전목차로다음 →