48 문법의 증명 — 어느 닫개로 닫아도 같은 나무

48.1 대수와 뜻함수#

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

두 표기가 “같은지” 를 말하려면 기준이 필요하다. 각 나무를 평평한 문장 나열로 보내는 함수 denote 를 두고, 결과가 같으면 같다고 한다. denote(do S end) = [S] = denote(S) 이므로 둘은 같다. 이것이 이 장의 유일한 기술이다 — “같다” 의 뜻을 함수로 정하고, 등식을 계산으로 확인한다.

48.2 한 문장은 한 문장짜리 블록이다#

module oneform .
rem run: bare 3
rem run: blocked 3
rem fmt

fn bare input a u64 . output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if gt a 1 . set x (add x 10) .
  return x .
end

fn blocked input a u64 . output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if gt a 1 . do
    set x (add x 10) .
  end
  return x .
end

$ lowentc --run bare oneform.low 3
bare(3) = 13
$ lowentc --run blocked oneform.low 3
blocked(3) = 13
$ lowentc --fmt oneform.low
module oneform .
fn bare .
  input a u64 .
  output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if (gt a 1) do set x (add x 10) . end
  return x .
end
fn blocked .
  input a u64 .
  output u64 .
  requires le a 1000 .
do
  var x u64 be a .
  if (gt a 1) do set x (add x 10) . end
  return x .
end

bare 는 if 의 몸에 문장 하나를 그대로 적었고, blocked 는 do … end 로 감쌌다. 답이 같고, --fmt 가 찍는 정규형도 한 글자 다르지 않다.

이 정리는 설계 결정 하나를 정당화한다. C 는 문장과 복합문을 다른 종류로 갈라 놓았다. if (c) x = 1; 과 if (c) { x = 1; } 가 문법적으로 다른 것이고, 유명한 goto fail; 함정이 그 틈에서 나왔다 — 들여쓰기는 두 줄이 if 에 속한 것처럼 보였지만 문법은 한 줄만 속하게 했다. Lowent 는 가르지 않는다.

 C       if (c)
             x = x + 10;
             y = 0;          ← 들여쓰기는 if 안처럼 보이지만 문법은 if 밖이다

 Lowent  if gt a 1 . set x (add x 10) .        문장 하나 = 문장 하나짜리 블록 (G1)
         if gt a 1 . do
           set x (add x 10) .
           set y 0 .
         end                                   몸이 길면 end 가 끝을 적는다

48.3 닫개는 같은 일을 한다#

예제로 보면 이렇다.

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

개행도 닫개로 만들 수 있고 그것도 증명된다. 그래도 두지 않는다. 개행이 닫으면 줄바꿈이 의미가 되어 긴 줄을 나누는 것만으로 프로그램이 바뀐다. 같은 뜻임이 증명된다고 그 철자를 두어야 하는 것은 아니다. 한때 쉼표·줄잇기·개행 닫기에 붙어 있던 정리들도 모두 Qed 였지만, 그 규칙들이 언어에서 빠지면서 정리도 함께 뺐다. 지금 , 와 ; 는 E-VOCAB-REMOVED 로 거절된다 — 파싱되는데 아무 효과가 없는 낱말은 조용한 함정이기 때문이다. 죽은 규칙을 모형화한 정리를 남겨 두면 증명된 문서가 없는 규칙을 말하게 된다.

이 파일의 증명은 전부 계산으로 끝난다. 값은 증명의 어려움이 아니라 명제를 골라 적었다는 데 있다. “닫개들이 같은 일을 한다” 를 적어 두면, 누가 하나를 특별 취급했을 때 증명이 깨진다. 문법은 “여기만 예외를 두면 편한데” 로 조용히 표류하는 층이고, 정리가 그 표류를 잡는다. 막는 것은 사용자의 결함이 아니라 컴파일러의 결함이다.

48.4 흔한 실수#

module mistake_noperiod .
rem expect: E-IR-ARITY

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

$ lowentc --check mistake_noperiod.low
mistake_noperiod.low:10:0 E-IR-ARITY: extra operands in expression (strict arity)

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:20 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 `.`

48.5 증명하지 않은 것#

• 실제 파서가 이 모델이라는 보장이 없다. 모델은 나무를 만드는 작은 함수들이고 실제 파서는 훨씬 크다. 대응은 단위 시험과 회귀 시험이 받친다.
• denote 는 평평한 나열이다. 위치 정보·주석·오류 복구를 모델링하지 않았다. 그러니 “같은 나무” 는 구조가 같다는 뜻이지 진단의 품질까지 같다는 뜻이 아니다.
• 어휘(토큰) 층은 별도다. 토큰이 이 모델의 닫개 셋으로 정확히 나뉘는지는 렉서 시험의 몫이다.