while 한 바퀴를 함수로 떼어 낸다🔗

반복문의 전체 뜻을 바로 재귀 정의하지 않고, 반복을 한 번 펼치는 연산자 F를 먼저 만든다. w를 “남은 반복의 뜻”이라고 놓으면 한 바퀴는 다음처럼 쓸 수 있다.

조건 b와 본체의 뜻 s를 고정하면 whileF b s는 함수에서 함수로 가는 연산자다.

F : (State V → SigmaBot V) → (State V → SigmaBot V)

전체 반복 의미 w가 풀기 방정식을 만족한다는 말은 F w = w, 곧 w가 F의 고정점이라는 말과 같다. §2.2에서 확인했듯 고정점은 여러 개일 수 있다.

아래에서 시작해 유한 근사를 늘린다🔗

후보 의미 공간의 최소원 ⊥은 모든 입력에서 none을 내는 함수다. 이 값에는 종료 정보가 하나도 없다. 여기에 F를 반복 적용한다.

⊥ ⊑ F(⊥) ⊑ F²(⊥) ⊑ F³(⊥) ⊑ ⋯

0번째 근사는 어떤 반복도 끝났다고 말하지 않는다. 다음 근사는 한 번 펼쳐 확인할 수 있는 종료를, 그다음 근사는 두 번 펼쳐 확인할 수 있는 종료를 추가한다. F가 단조이면 앞 근사의 종료 결과가 뒤에서 사라지지 않는다.

fix F hF는 이 사슬의 최소 상한으로 정의된다. 어느 유한 단계에서 확인한 종료 정보도 포함하되, 사슬에 없던 종료 정보를 따로 보태지 않는 값이다.

연속성이 극한을 고정점으로 만든다🔗

사슬의 극한에 F를 적용한 값을 계산하려면 F를 극한 안으로 옮겨야 한다.

F (⨆ₙ Fⁿ(⊥)) = ⨆ₙ Fⁿ⁺¹(⊥)

왼쪽에서 첫 등식을 허용하는 가정이 연속성이다. 오른쪽 사슬은 원래 사슬에서 맨 앞의 ⊥만 뺀 사슬이고, ⊥은 모든 항 아래에 있으므로 극한이 바뀌지 않는다.

여기서 단조성만 가정하면 반복 사슬은 만들 수 있지만 F를 극한 안으로 옮길 수 없다. §2.3의 단조지만 연속이 아닌 반례가 이 단계에서 연속성이 필요한 이유를 보여 준다.

그 고정점이 모든 다른 해보다 아래에 있다🔗

F x ⊑ x인 값을 전고정점(pre-fixed point)이라 부른다. x가 고정점이면 당연히 전고정점이다. 반복 사슬의 모든 항이 x 아래에 있음을 자연수 귀납으로 보이면, 그 극한도 x 아래에 있다.

최소라는 말은 “실행 시간이 가장 짧다”거나 “결과 상태의 정수가 가장 작다”는 뜻이 아니다. 정보 순서에서 아래라는 뜻이다. 최소 고정점은 유한 근사로 확인할 수 없는 입력에 임의의 종료 결과를 붙이지 않는다. §2.2의 decrFake가 탈락하는 이유가 여기에 있다.

Scott 귀납법은 유한 근사의 성질을 극한으로 넘긴다🔗

최소 고정점에 관한 성질 P를 증명할 때는 세 조건을 확인한다.

1. P ⊥ — 아무 정보도 없는 근사에서 성립한다.

2. P x → P (F x) — 한 단계를 더 펼쳐도 보존된다.

3. 사슬의 모든 항에서 P가 성립하면 극한에서도 성립한다.

세 번째 조건을 허용 가능성(admissibility)이라 부른다.

일반적인 구조적 귀납법은 구문 트리의 생성자를 따라간다. Scott 귀납법은 의미의 유한 근사를 따라간다. while의 의미는 구문 재귀만으로 만들어지지 않으므로 두 귀납법의 역할도 다르다.

최소 고정점으로 Comm.eval을 완성한다🔗

whileF가 연속이라는 정리를 증명한 뒤, wh 절에서 그 최소 고정점을 택한다.

Comm.eval_isSemantics는 이 정의가 §2.2의 여섯 방정식을 모두 만족한다고 증명한다. Comm.eval_while_least는 같은 본체와 조건에 대한 다른 풀기 방정식의 해보다 이 의미가 아래에 있음을 증명한다. 존재, 방정식 만족, 최소성이 서로 다른 정리로 나뉘어 있다.

Comm.eval은 noncomputable이다. 평평한 사슬에서 언젠가 종료 결과가 나타나는지를 일반적으로 계산할 수 없기 때문이다. 증명에 쓸 뜻과 실제로 돌릴 해석기를 분리해야 한다.

실제 명령을 펼쳐 wₙ을 만든다🔗

Reynolds pp. 36–37은 의미 함수의 반복에 대응하는 명령 구문도 만든다. 먼저 항상 발산하는 명령을 놓고, 다음 단계마다 조건과 본체 한 번을 앞에 붙인다.

w₀는 조건을 보기도 전에 발산한다. w₁은 조건이 처음부터 거짓일 때만 종료한다. 본체를 한 번 실행하고 종료하는 입력은 w₂부터 결과를 갖는다. 각 명령을 해석하면 구문의 한 단계가 정확히 F의 한 번 적용이 된다.

Comm.approxChain은 이 의미들을 사슬로 묶는다. Comm.eval_while_eq_approx_lub가 그 사슬의 극한과 while의 의미를 연결한다. 본체에 또 while이 있어도 이 대응은 같다. 다만 본체의 뜻은 완전한 c.eval이므로, 중첩 반복까지 연료를 제한하는 Comm.run n과는 단계별로 구별해야 한다.

합산 반복문의 근사를 손으로 계산한다🔗

책 pp. 37–38의 예제는 while x ≠ 0 do (x := x - 1; y := y + x)다. 처음 x = 3, y = 10이면 본체는 (2,12), (1,13), (0,13) 순서로 상태를 바꾼다. 그 뒤 조건이 거짓인지 확인하는 검사까지 필요하다.

• w₀, w₁, w₂, w₃의 결과는 Flat.none이다.

• w₄ 이후에는 x = 0, y = 13인 같은 종료 상태를 얻는다.

SumApproximation.lean의 sumApprox n은 이 본체의 계산을 직접 적은 함수다. sumApprox_eq_approx_eval이 그 값과 실제 명령 wₙ의 의미를 연결한다. 연습 sumApprox_eq에서는 모든 정수 상태에 대해 다음 식을 증명한다.

Fⁿ(⊥)(σ) = if 0 ≤ σ(x) < n
           then some (σ[x := 0][y := σ(y) + σ(x)·(σ(x)−1)/2])
           else none

핵심은 n에 대한 귀납이다. x ≠ 0에서 한 번 감소한 입력의 조건 0 ≤ x−1 < n은 0 ≤ x < n+1과 같다. 결과 상태의 합산값도 같아야 하며, 그 부분은 triangle_step과 sumResult_step이 완성 자료로 제공한다. 학생은 상태를 바꾸어 귀납 가설을 적용하고, 종료 검사 횟수의 경계를 증명한다.

x ≥ 0이면 어느 유한 단계부터 결과가 같아진다. x < 0이면 모든 단계가 바닥이다. sumLoop_eval_of_approx는 이 두 사슬의 최소 상계를 계산한다. 마지막 정리는 실제로 증명한 유한 근사식을 사용하므로, 추가 가설 없이 반복문 전체의 뜻을 준다.

직접 확인할 입력은 x = 0, x = 3, x = -1이다. 각각 처음 검사에서 종료, 세 번 본체 실행 뒤 종료, 영원히 0에서 멀어지는 경우를 보여 준다. x, y 이외의 변수도 하나 넣어 sumResult가 그 변수의 값을 보존하는지 확인해 보자.

연료 해석기는 유한 근사를 실행한다🔗

Comm.run c n σ는 반복을 펼칠 수 있는 연료 n을 받는다. 반복이 아닌 절은 연료를 소비하지 않고, while을 한 번 펼칠 때 남은 반복에 넘길 연료를 하나 줄인다.

연료가 부족해 none이 나왔다고 해서 프로그램이 발산한다고 결론 내릴 수는 없다. while x > 0 do x := x - 1을 x = 5에서 실행하면 연료 5로는 마지막 조건 검사를 마치지 못하지만, 연료 6에서는 x = 0인 상태를 얻는다. 반대로 while tt do skip은 어떤 유한 연료에서도 none이다.

Comm.run_le_succ는 연료를 늘릴 때 정보를 잃지 않는다는 정리다. 한 번 some σ'이 나오면 더 큰 연료에서도 같은 some σ'이 나온다. 평평한 순서에서는 종료 결과를 다른 값으로 바꾸는 것이 허용되지 않기 때문이다.

적합성은 증명용 의미와 실행용 의미를 잇는다🔗

표시적 의미에서 종료 결과를 증명해도 해석기가 재현하지 못한다면 실행과 동떨어진 뜻이다. 반대로 해석기가 낸 결과가 표시적 의미와 다르면 테스트를 정리의 근거로 옮길 수 없다.

정리의 오른쪽은 “어떤 유한 연료에서 같은 종료 결과가 나온다”다. 따라서 run으로 확인한 종료 결과는 eval의 결과이고, eval에서 얻은 종료 결과도 충분한 연료로 실행된다. 이 진술은 eval σ = none과 “모든 연료에서 run이 none” 사이의 동치를 직접 적은 정리는 아니다. 현재 적합성 정리가 옮기는 범위는 some인 종료 결과다.

직접 해 보기와 연습 범위🔗

현재 §2.2~§2.4 본문 파일에는 채점 대상이 20개 있다.

• Semantics.lean — 불 식과 단언의 일치, 리프팅과 bind, 풀기 방정식의 비유일성

• Domain.lean — 연속이면 단조, 명제 2.1, 단조지만 연속이 아닌 반례

• Domain/Lifting.lean — 평평한 도메인의 연속성, 명제 2.4

• Domain/LiftingLaws.lean — 명제 2.4(a–e)의 이산 입력 특수화, 다섯 독립 연습

• Domain/FunctionSpace.lean — 명제 2.2와 2.3

• Fixpoint.lean — 고정점, 최소성, Scott 귀납법

• Eval.lean — 연속성 계산 연습 2.4

• SumApproximation.lean — 책 pp. 37–38의 유한 근사 닫힌 꼴

Approximation.lean의 구문·의미 대응, 합산 예제의 극한 계산, Interpreter.lean의 연료 단조성과 적합성은 완성 자료로 읽는다.

Reynolds/Exercises/Ch02/에서 sorry를 채운 뒤 다음 명령으로 상태를 확인한다.

lake exe grade --chapter 2

§2.5~§2.8과 책 연습 2.1~2.10의 실습은 뒤의 파일로 이어진다. “§2.2” 같은 식별자는 해당 절의 형식화를 익히기 위해 저장소가 둔 연습이고, “Prop 2.1”과 “Ex 2.4”는 책의 번호다. discrete가 붙은 명제 2.4 연습은 책의 일반 명제를 이산 입력에 특수화했다는 표시다.