결과를 값이 아니라 정보로 비교한다🔗

§2.2에서 같은 풀기 방정식을 만족하는 함수가 둘 이상 생겼다. 이 중 계산의 뜻으로 삼을 함수를 고르려면 후보를 비교할 기준이 필요하다.

SigmaBot V = Flat (State V)에는 평평한 순서(flat order)를 준다. Flat은 종료 결과와 바닥을 갖는 전용 귀납 타입이다.

일반 Option Nat에서는 some 1 ≤ some 2가 성립한다. Flat Nat에서는 서로 다른 두 종료 결과가 어느 방향으로도 비교되지 않는다. 관찰 함수 observe는 toOption으로 결과를 꺼내므로 반환 타입 Option Int를 유지한다.

none   ⊑ none
none   ⊑ some σ
some σ ⊑ some σ

서로 다른 두 종료 상태는 비교하지 않는다. some σ ⊑ some σ'이면 σ = σ'다. 이 순서는 “더 큰 수”나 “더 좋은 상태”를 말하지 않는다. none보다 some σ가 위인 이유는 계산 결과에 관한 정보가 하나 늘었기 때문이다.

상태 변환 함수의 순서는 이 순서를 입력마다 적용한다.

f ⊑ g  ↔  ∀ σ, f σ ⊑ g σ

따라서 g가 f보다 위라는 말은, f가 이미 내던 종료 결과를 바꾸지 않으면서 f가 none이던 입력 중 일부에서 결과를 더 낼 수 있다는 뜻이다.

사슬은 유한 근사를 차례로 놓은 것이다🔗

계산을 0단계, 1단계, 2단계로 점점 더 오래 허용하면 정보가 줄지 않는 열을 얻는다. 이런 증가 열을 사슬(chain)이라 부른다.

seq n은 n번째 근사이고 mono는 나중 근사가 앞선 근사의 정보를 잃지 않는다는 증거다. 이 정의가 요구하는 것은 가산 열 하나다. 임의의 유향 집합을 쓰는 더 일반적인 도메인 이론과는 범위가 다르다.

사슬 전체를 하나의 값으로 합칠 때는 최소 상한(least upper bound)을 쓴다.

상계(upper bound)

사슬의 모든 항보다 위에 있는 값이다.

최소 상한

모든 상계보다 아래에 있는 상계다. 사슬이 쌓아 온 정보만 합치고, 갑자기 새 정보를 보태지 않은 값이다.

프리도메인은 모든 사슬의 극한을 제공한다🔗

Predomain은 각 사슬에 최소 상한을 골라 주고, 그 선택이 실제 최소 상한임을 증명으로 묶는다.

이 저장소의 Domain α는 프리도메인에 최소원 ⊥이 추가된 경우다. Lean에서는 Predomain α와 OrderBot α를 함께 요구하는 축약 이름으로 둔다. 최소 고정점의 유한 근사를 시작하려면 아무 종료 정보도 없는 ⊥이 필요하다.

Mathlib에는 이미 더 일반적인 순서론 구조가 있지만, 이 절에서는 Reynolds의 정의와 증명을 따라가기 위해 작은 Chain과 Predomain을 직접 만든다. 라이브러리 대응물을 가져와 정리를 한 줄로 끝내면 §2.3의 학습 대상이 사라진다.

연속성은 극한에서 정보가 갑자기 생기지 않게 한다🔗

단조 함수는 두 근사 사이의 순서를 보존한다. 연속 함수는 여기서 더 나아가, 사슬을 끝까지 합친 뒤 함수를 적용한 값이 각 근사에 함수를 적용해 합친 값과 맞도록 한다.

이 정의는 등식 하나를 직접 쓰지 않는다. f c.lub가 f를 사슬의 각 항에 적용해 얻은 값들의 최소 상한이라고 말한다. 공역 전체에 Predomain 인스턴스를 요구하지 않고도 해당 상의 극한 보존을 표현하기 위해서다.

현재 정의에서는 연속성으로부터 단조성을 증명한다. x ⊑ y일 때 x, y, y, …라는 사슬을 만들면, 그 극한은 y다. 연속성이 이 사슬의 상에 대해 f x ⊑ f y를 준다.

명제 2.1은 연속성 증명에서 확인할 방향을 줄여 준다.

단조성만으로 충분하지 않은 이유는 무한한 극한에서만 새 정보를 내는 함수가 있기 때문이다.

단조지만 연속이 아닌 함수🔗

자연수의 유한 시작 구간을 하나씩 늘리는 사슬을 생각한다.

∅ ⊆ {0} ⊆ {0, 1} ⊆ {0, 1, 2} ⊆ ⋯

이 사슬의 극한은 자연수 전체다. f s = (s = ℕ)로 두면 각 유한 근사에서 f s는 거짓이고, 극한에서만 참이다.

Reynolds는 수직 자연수 ℕ⊤을 사용한다. 이 저장소는 Mathlib의 완비 격자 인스턴스를 활용할 수 있는 Set ℕ으로 같은 구조의 반례를 옮겼다. 유한 근사에서는 보이지 않던 정보가 극한에서만 생긴다는 논점은 같다.

Flat 사슬의 극한🔗

평평한 Flat α 사슬은 계속 none으로 남거나, 어느 시점에 some a가 나온 뒤 그 값으로 고정된다. 서로 다른 두 some 값은 비교되지 않으므로, 증가 사슬 안에서 종료 결과가 다른 값으로 바뀔 수 없다.

flatPredomain은 이 관찰을 프리도메인 인스턴스로 만든다. “언젠가 some a가 나오는가”는 일반적으로 판정할 수 없어서 극한 선택에 Classical.choice를 쓴다. 이 정의가 noncomputable인 것은 실행기의 결함이 아니다. 임의의 계산이 언젠가 끝나는지를 극한 함수가 계산해 준다면 정지 문제를 풀 수 있기 때문이다.

Monotone.continuous_of_lub_mem 정리는 평평한 정의역에서 단조 함수가 연속임을 보인다. 평평한 사슬의 극한은 새 값이 아니라 사슬이 실제로 지나간 값이므로, 극한에서 갑자기 생길 정보가 없다.

바닥을 더한 함수는 어떻게 합성하는가🔗

값을 바꾸는 함수 f : α → β를 계산 결과에 적용하려면 Flat.map f를 쓴다. 바닥 입력은 바닥으로, Flat.some a는 Flat.some (f a)로 간다. 반면 g : α → D의 공역이 이미 바닥을 갖고 있다면 결과에 바닥을 또 더할 필요가 없다.

g : State V → Flat (State V)로 놓으면 sourceLift g가 앞서 쓴 liftBot g다. 이 둘은 함수 타입부터 다르다. Flat.map g의 결과는 Flat (Flat (State V))지만, sourceLift g의 결과는 Flat (State V)다.

Reynolds 명제 2.4(p. 35)의 다섯 항을 Domain/LiftingLaws.lean에서 직접 증명한다.

• (a) 바닥에서 바닥, 값에서 Flat.some (f a)를 내는 확장은 Flat.map f 하나다.

• (b) 바닥에서 바닥, 값에서 g a를 내는 확장은 sourceLift g 하나다.

• (c) Flat.map (g ∘ f) = Flat.map g ∘ Flat.map f

• (d) sourceLift (g ∘ f) = sourceLift g ∘ Flat.map f

• (e) h ⊥ = ⊥이면 sourceLift (h ∘ g) = h ∘ sourceLift g

(e)의 가설은 값 입력에서는 필요하지 않다. 바닥 입력에서 왼쪽은 바닥이고 오른쪽은 h ⊥다. h를 언제나 Flat.some 1을 내는 함수로 잡으면 두 값이 달라진다. 파일의 nonstrict_counterexample은 이 반례를 확인한다.

책과의 차이: 책의 입력 P는 임의의 프리도메인이다. 이 실습은 이산 집합의 Flat 리프팅에 한정한다. 공역 D는 평평할 필요가 없으며, 순서와 바닥을 갖추면 sourceLift_continuous가 연속성을 보인다. 기존의 비이산 순서를 보존하는 일반 P⊥ 구성과 리프팅 모나드의 법칙은 별도 후속 실습이다.

상태 변환 함수의 극한은 입력마다 잰다🔗

while의 후보 의미는 함수 State V → SigmaBot V다. 최소 고정점 정리를 이 함수들 사이에서 쓰려면 함수 공간 자체에도 사슬의 극한이 있어야 한다.

(⨆ₙ fₙ) σ는 입력 σ 하나를 고정한 뒤 결과들의 평평한 사슬을 합친 값이다. 어떤 입력에서는 3단계에 종료 결과가 나타나고, 다른 입력에서는 100단계에 나타나도 된다. 함수 공간의 극한은 그 차이를 입력마다 보존한다.

명제 2.2는 연속 함수들만 모은 공간도 프리도메인임을, 명제 2.3은 항등·상수·합성으로 연속 함수를 조립할 수 있음을 보인다. 2장의 while에는 전체 함수 공간의 점별 극한이 직접 쓰이고, 연속 함수 공간은 이후 고차 함수의 타입 의미에서 다시 필요해진다.