39 수학 도구상자

39.1 여섯 가지 도구#

39.2 집합과 관계#

집합은 모음이다 — {0, 1, 2}. 관계는 짝의 목록이다. “작다” 관계는 {(0,1), (0,2), (1,2)} 처럼 순서쌍의 모음이다. 프로그램 이야기에서는 타입의 집합 {u8, u16, u32, u64, i8, …} 위에 “안전하게 넓혀진다” 관계를 둔다. 그 관계를 ⊑ 로 적고 “왼쪽이 오른쪽에 값이 변하지 않고 들어간다” 로 읽는다. 부등호 ≤ 와 닮았지만 수의 크기가 아니라 담을 수 있는가를 말한다.

39.3 부분 순서 — 비교할 수 없는 쌍#

수는 언제나 비교된다. 3 과 5 가운데 하나는 크다. 타입은 그렇지 않다. u8 ⊑ u16 ⊑ u32 ⊑ u64 이고 i8 ⊑ i16 ⊑ i32 ⊑ i64 이지만, u32 와 i32 는 어느 쪽도 상대를 다 담지 못한다. u32 는 40억까지 담고 i32 는 음수를 담는다. 어느 쪽이 크다고 말할 수 없다는 사실을 정직하게 담는 구조가 부분 순서다.

이 셋이 증명되어야 “안전한 넓히기” 라는 말이 뜻을 갖는다. 추이성이 깨지면 u8 → u16 과 u16 → u32 는 허락하면서 u8 → u32 는 막는 언어가 된다. 사용자는 왜 안 되는지 영영 알 수 없다. 이 셋은 40장에서 실제 타입에 대해 증명된다.

39.4 격자와 join — 합칠 때 무엇을 고르나#

두 값을 한 연산에 넣으면 처리기는 둘을 다 담는 타입에서 계산해야 한다. 후보는 여럿이지만 가장 작은 것을 고르는 것이 맞다. 그 “가장 작은 공통 상위” 를 join 이라 하고 ⊔ 로 적는다. 임의의 두 원소가 늘 join 을 갖는 부분 순서를 격자라 한다.

module widening .
rem run: wider 200 60000
rem trap: wider 255 65535

rem u8 과 u16 을 더하면 둘을 다 담는 가장 작은 타입(u16)에서 계산된다
fn wider input a u8 . input b u16 . output u32 . do
  return add a b .
end

$ lowentc --run wider wider.low 200 60000
wider(200, 60000) = 60200
$ lowentc --run wider wider.low 255 65535
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

u8 ⊔ u16 = u16 이다. 그래서 출력 타입이 u32 여도 덧셈은 u16 에서 일어나고, 255 + 65535 는 u16 을 넘쳐 멈춘다. join 은 피연산자에서 정해지지, 결과를 받을 자리에서 정해지지 않는다.

부호가 섞이면 직관과 달라진다. u8 ⊔ i8 은 i8 이 아니라 i16 이다 — u8 의 255 와 i8 의 −128 을 함께 담으려면 폭이 더 넓어야 한다. 사람은 이런 자리에서 틀린다. Lowent 는 이 넓히기를 대신 고르지 않고 적게 한다.

module sign_join .
rem expect: E-TYPE-SIGN

rem u8 과 i8 을 둘 다 담는 타입은 i16 이다. 처리기는 그 넓히기를 대신 고르지 않는다
fn mix input a u8 . input b i8 . output i16 . do
  return add a b .
end

$ lowentc --check sign_join.low
sign_join.low:6:0 E-TYPE-SIGN: sign mismatch: no value-preserving widening exists (widen both to a strictly wider signed type, or bitcast_sign)

진단이 말하는 “strictly wider signed type” 이 바로 u8 ⊔ i8 = i16 이다. 둘을 모두 i16 으로 넓혀 적으면 받아들여진다.

39.5 단조 함수와 고정점 — 분석은 왜 멈추는가#

단조 함수는 입력이 커지면 출력이 작아지지 않는 함수다. 고정점은 f(x) = x 인 점, 곧 한 번 더 적용해도 변하지 않는 점이다.

처리기가 반복을 분석할 때 이 두 개념이 일한다. 분석기는 반복에 들어올 때 변수의 범위를 모른다. 그래서 좁게 시작해 되풀이하며 넓힌다.

1 바퀴 뒤: i ∈ [0, 0]
2 바퀴 뒤: i ∈ [0, 1]
3 바퀴 뒤: i ∈ [0, 2]      … 이대로면 끝나지 않는다

그래서 위드닝(widening)을 쓴다. 몇 번 넓어지는 것을 보면 “계속 커지겠다” 고 보고 한 번에 위 끝까지 민다. i ∈ [0, ∞) 에 반복 조건 i < 10 을 합치면 i ∈ [0, 9] 이고, 한 바퀴 더 돌려도 [0, 9] 다. 고정점에 닿았고 분석이 끝난다.

module count_up .
rem run: ten
rem proof

fn ten output u8 . do
  var i u8 be 0 .
  var s u8 be 0 .
  while lt i 10 . do
    set s (add s i) .
    set i (add i 1) .
  end
  return s .
end

$ lowentc --run ten count_up.low
ten() = 45
$ lowentc --emit-proof count_up.low
# proven 1 certified 1
ten 14 add.i64 R-ARITH-RANGE 0 9 1 1 8 0

증명 줄이 하나다. add i 1 은 i ∈ [0, 9] 에서 더하므로 u8 을 넘지 않는다고 증명되었다(R-ARITH-RANGE 0 9). add s i 는 증명되지 않았다. 위드닝이 s 의 위 끝을 버렸기 때문이다. 실제로 s 는 45 를 넘지 않지만 분석은 그것을 모른다. 그래서 검사가 남는다 — 느릴 뿐 틀리지는 않는다.

• 고정점이 늘 있다는 것이 분석이 멈춘다는 보장이다.
• 위드닝은 넓게 잡는다. 실제보다 크게 잡으면 검사를 못 지울 뿐 틀린 답은 나오지 않는다. 이 방향이 추상해석의 핵심이다.

39.6 귀납법과 불변식 — 도미노#

수학적 귀납법은 이렇다. P(0) 이 참이고, P(n) 이 참이면 P(n+1) 도 참이다. 그러면 모든 n 에 대해 P(n) 이 참이다. 프로그램에서는 n 이 “실행한 걸음 수” 가 되고, P 를 불변식 — 실행 내내 참인 성질 — 이라 부른다.

39.7 추상해석 — 값 대신 범위로#

프로그램을 돌리지 않고 값에 대해 무언가 알아내려면 값 하나 대신 값의 집합을 다뤄야 한다. 집합을 그대로 다루면 너무 크니 간단한 근사를 쓴다. 그 대표가 구간 [lo, hi] 다.

x ∈ [0, 5],  y ∈ [10, 20]  이면
x + y ∈ [10, 25]      양 끝끼리 더한다
x × y ∈ [0, 100]      부호가 섞이면 네 곱의 최소·최대를 본다

규칙은 하나다. 추상 계산의 결과는 실제로 가능한 모든 값을 포함해야 한다. 실제로 x 가 늘 3 인데 분석이 [0, 5] 라고 답하면 손해는 있어도 안전하다(검사를 못 지운다). 실제로 x 가 7 일 수 있는데 [0, 5] 라고 답하면, 그 답으로 검사를 지운 순간 범위 밖 접근이 일어난다. 그래서 분석의 모든 규칙은 “넓게” 쪽으로 기울어 있다.

39.8 기호 표#

39.9 도구들이 맞물리는 방식#

부분 순서 ⊑           "안전하게 담긴다" 를 정의한다        (수)
   │
   ├─ join ⊔          합칠 때 타입을 고른다                (수 · 효과)
   │
격자 위의 단조 함수   반복 분석이 그 위를 오른다           (경계)
   │
고정점                분석이 멈추는 자리                   (경계 · 되풀이)
   │
추상해석의 건전성     "넓게" 틀리면 결론이 안전하다        (경계)
   │
불변식과 귀납법       실행 내내 유지됨을 보인다            (소유 · 되풀이 · 경합)

아래에서 위로 읽어도 된다. 귀납법으로 불변식을 지키고, 그 불변식이 추상해석의 건전성에서 오고, 추상해석은 격자 위에서 돌고, 격자는 부분 순서 위에 선다. 도구가 없으면 설계가 어림짐작이 된다 — join 을 손으로 적은 표는 u8 ⊔ i8 = i8 같은 줄을 섞어 255 를 −1 로 바꾸고, 위드닝 없는 반복 분석은 끝나지 않으며, 불변식 없는 차용 검사는 “이때는 되고 저때는 안 되는” 규칙 더미가 된다.