컨티뉴에이션의 개념을 도입하고, 이를 표기적 의미론으로 정식화한다. 레이블과 점프가 있는 명령형 언어의 의미론을 컨티뉴에이션으로 정의하고, 함수형 언어에 대한 CPS(Continuation-Passing Style) 변환을 콜바이밸류와 콜바이네임 모두에 대해 제시한다. 이어서 CPS 변환의 형태적 특징, 평가 전략에 대한 무관성 정리, 의미 보존 성질을 설명한다.
프로그램 지점의 컨티뉴에이션. 프로그램의 실행 중 한 지점을 생각하자. 이 프로그램에서 그 지점의 컨티뉴에이션(continuation) 이란, 전체 프로그램 실행을 완료하기 위해 그 지점에 도달한 뒤에 남아 있는 계산의 순서를 말한다.
대개 컨티뉴에이션은 프로그래밍 언어 안에서 명령문이나 함수로 표현될 수 있다(아래 예시 참조). 컨티뉴에이션은 또한 아래 6.3절에서 보듯 의미론적 객체로도 나타낼 수 있다.
문장 기반 언어에서의 컨티뉴에이션 예시. 구조적 제어를 가진 Algol 스타일의 명령형 언어로 작성된 다음 네 프로그램을 보자:
p 1 = s 1(a); s 2
p 2 = if be then(b) s 1 else(c) s 2; s 3
p 3 = while be do(d) s(e)
p 4 = for i := 1 to 10 do(f) s
프로그램 지점은 (a), (b) 등으로 표기하며, (a)s처럼 s라는 명령의 시작을 나타내거나 s(b)처럼 s의 끝을 나타낸다.
프로그램 p 1에서, (a)의 컨티뉴에이션은 명령 s 2이다. s 1의 끝에 도달하면, s 1; s 2라는 순서는 s 2를 실행하여 프로그램의 끝에 도달한다.
p 2에서, (b)의 컨티뉴에이션은 s 1; s 3이고, (c)의 컨티뉴에이션은 s 2; s 3이다. 조건문의 then 분기 s 1을 실행한 뒤에는 s 3을 여전히 실행해야 한다. else 분기 s 2도 마찬가지다.
p 3에서, (d)의 컨티뉴에이션은 s; while be do s 이다. 반복문의 본문 s를 실행한 다음, be가 거짓이 될 때까지 while 루프를 다시 실행해야 하기 때문이다. 같은 이유로, (e)의 컨티뉴에이션은 루프 while be do s 이다.
p 4에서, (f)의 컨티뉴에이션은 s; while i ≠ 10 do(i := i + 1; s)이다. 횟수 지정 루프의 본문 s를 실행한 다음, i가 상한 10에 도달할 때까지 i를 증가시키며 본문을 다시 실행해야 한다.
부분식의 컨티뉴에이션. 함수형 언어에서는 프로그램이 표현식이므로, 프로그램 지점은 보통 부분식 평가의 끝을 표시한다. 따라서 프로그램 p의 부분식 e의 컨티뉴에이션을 다음과 같은 함수로 생각할 수 있다.
value of e ↦ value of p
이 함수는 p를 평가하여 그 값을 산출하기 위해, e의 값을 얻은 뒤에 남아 있는 계산을 포착한다.
식 기반 언어에서의 컨티뉴에이션 예시. 왼쪽에서 오른쪽으로 평가하는 산술식 언어와 다음 프로그램을 생각하자.
p = (1 + 2) × (3 + 4)
p에서 1의 컨티뉴에이션은 함수 λ v. (v + 2) × (3 + 4)이다. 직관적으로, 1을 값 v로 평가한 뒤에는 “플러스 2”를 평가하고, 이어서 “times 3 + 4”를 평가해야 한다.
p에서 1+2의 컨티뉴에이션은 함수 λ v. v × (3 + 4)이다. 1+2를 평가한 뒤에는 “times 3 + 4”만 계산하면 된다.
p에서 3+4의 컨티뉴에이션은 λ v. 3 × v이지, λ v. (1+2) × v가 아니다. 평가가 왼쪽에서 오른쪽으로 진행되므로, 3+4를 평가하기 전에 1+2를 먼저 평가한다. 따라서 3+4를 v로 평가할 무렵에는 이미 1+2를 3으로 평가한 상태이며, 남은 계산은 3 × v뿐이다.
컨티뉴에이션은 평가 전략에 의존한다는 점에 유의하자. 만약 오른쪽에서 왼쪽으로 평가한다면, p에서 1+2의 컨티뉴에이션은 λ v. v × 7이 되고, 3+4의 컨티뉴에이션은 λ v. (1 + 2) × v가 된다.
컨티뉴에이션과 점프. 컨티뉴에이션의 개념은 점프(goto, break, return, 예외 던지기 등)와 다른 명령(대입, 조건문 등)의 차이를 이해하는 데 도움이 된다.
시작 지점 (a)와 끝 지점 (b)을 가진 명령 (a) s (b)를 생각하자. s가 점프를 포함하지 않는다면, (a)의 컨티뉴에이션은 항상 s에 이어 (b)의 컨티뉴에이션이 온다. 하지만 s가 점프일 경우는 다르다:
예를 들어, 다음에서 (a)의 컨티뉴에이션은
while be do(if be′ then(a) break; s 1); s 2
바로 s 2이지, s 1; while …; s 2가 아니다.
표기적 의미론(denotational semantics)은 Christopher Strachey, Dana Scott, Christopher Wadsworth 등 여러 연구자들에 의해 1960년대 후반에 도입되었으며, 프로그램의 의미를 수학적으로 정밀하게 정의하는 방법이다. 표기적 의미론은 프로그래밍 언어의 각 구문 요소(표현식, 명령문, 함수, …)에 수학적 객체를 조합적으로 대응시킨다.
예를 들어, 변수들을 포함하는 정수 산술식 e의 의미는 저장소(store)에서 정수로 가는 함수로 정의할 수 있다. 여기서 저장소는 변수에 정수를 대응시킨다:
⟦ e ⟧ : Store → Int where Store = Variable →fin Int
이 의미 함수는 e의 구조에 대한 귀납과 경우분석으로 정의된다. 예를 들어:
⟦ c ⟧σ = c (c가 상수일 때)
⟦ x ⟧σ = σ(x) (x가 변수일 때)
⟦ e 1 + e 2 ⟧σ = (⟦ e 1 ⟧σ + ⟦ e 2 ⟧σ) mod 2 32
⟦ e 1 * e 2 ⟧σ = (⟦ e 1 ⟧σ × ⟦ e 2 ⟧σ) mod 2 32
이 예시는 32비트 부호 없는 산술을 사용하므로, 모든 산술 연산은 2 32로 나눈 나머지로 계산된다.
명령문 s의 표기적 의미론은 1차 근사로 저장소 변환기(store transformer) 이다. 즉, s 실행 “전”의 저장소를 s 실행 “후”의 저장소로 사상하는 함수이다.
⟦ s ⟧ : Store → Store
예컨대 대입 x := x + 1을 보자. 저장소 σ에서 시작해, σ′ = σ [x ↦ (σ(x) + 1) mod 2 32]라는 저장소에서 종료한다. 즉, x를 (σ(x) + 1) mod 2 32(초기 x 값에 1을 더한 값)로, 다른 모든 변수 y를 σ(y)로 사상하는 저장소이다.
명령문의 의미론은 또한 발산(divergence), 즉 while true 같은 무한 루프처럼 종료하지 않는 명령도 고려해야 한다. 발산을 나타내기 위해 ⊥(바텀)를 쓴다. 따라서 의미 함수의 형태는 다음과 같다.
⟦ s ⟧ : Store → Store + { ⊥ }
산술식: e ::= 0 ∣ 1 ∣ 2 ∣ … 상수
∣ x 변수
∣ e 1 + e 2 ∣ e 1 × e 2 합, 곱
불리언 식: be ::= true ∣ false 상수
∣ e 1 = e 2 ∣ e 1 < e 2 비교
∣ not e ∣ e 1 and e 2 부정, 논리곱
명령문: s ::= skip 아무 것도 하지 않음
∣ x := e 대입
∣ s 1; s 2 순차
∣ if be then s 1 else s 2 조건
∣ while be do s 일반 루프
∣ begin s 1; L: s 2 end 블록 범위 레이블 선언
∣ goto L 레이블로 점프그림 6.1: IMP 장난감 명령형 언어: 추상 구문.
그림 6.1의 IMP 장난감 언어를 보자. 구조적 명령문에 대한 표기적 의미론은 다음과 같다:
⟦ skip ⟧σ = σ
⟦ x := e ⟧σ = σ [x ↦ ⟦ e ⟧σ]
⟦ s 1; s 2 ⟧σ = ⎧ ⎨ ⎩ ⊥ if ⟦ s 1 ⟧σ = ⊥; ⟦ s 2 ⟧(⟦ s 1 ⟧σ) otherwise
⟦ if be then s 1 else s 2 ⟧σ = ⎧ ⎨ ⎩ ⟦ s 1 ⟧σ if ⟦ be ⟧σ = true; ⟦ s 2 ⟧σ if ⟦ be ⟧σ = false
⟦ while be do s ⟧ = lfp(λ d. λ σ. if ⟦ be ⟧σ then d(⟦ s ⟧σ) else σ)
while의 경우, lfp는 주어진 연산자의 최소 고정점을 의미하며, 정렬은 모든 σ에 대해 ⊥ < σ 이다. 이 정의는 while 루프의 의미가 루프가 종료하지 않을 때 그리고 그때에만 ⊥가 되고, 다음 전개 방정식을 만족하도록 보장한다.
⟦ while be do s ⟧ = ⟦ if be then (s; while be do s) else skip ⟧
6.1절의 끝에서, goto L 명령을 레이블 L의 컨티뉴에이션을 호출하는 것으로 생각할 수 있다고 언급했다. 이 방향의 첫 단계로, 이제 명령문의 표기적 의미론에서 컨티뉴에이션을 명시적으로 도입한다. 이른바 직접 스타일(direct style) 의 의미 함수
⟦ s ⟧ : Store → Res
대신, 이른바 컨티뉴에이션 전달 스타일(continuation-passing style) 로 쓰자.
⟦ s ⟧ : Store → (Store → Res) ◥ 컨티뉴에이션 ◣ → Res
여기서 Res는 Store + {⊥}로, 즉 실행의 결과를 의미한다. 최종 상태이거나 발산이다.
의미론의 형태는 ⟦ s ⟧σ k로 쓴다. 여기서 σ는 s 실행 “전”의 상태이고, k는 s의 컨티뉴에이션의 의미(함수)로서, s 실행 “후”의 상태를 인자로 받아 프로그램 전체 실행이 끝났을 때의 상태를 반환한다. 다시 말해, ⟦ s ⟧는 s 실행 “후”의 상태를 계산하여 k에 전달하고, k는 프로그램 전체 실행의 끝 상태를 산출한다. ⟦ s ⟧의 정의는 다음과 같다:
⟦ skip ⟧σ k = k(σ)
⟦ x := e ⟧σ k = k(σ [x ↦ ⟦ e ⟧σ])
⟦ s 1; s 2 ⟧σ k = ⟦ s 1 ⟧(λ σ′. ⟦ s 2 ⟧σ′ k)
⟦ if be then s 1 else s 2 ⟧σ = ⎧ ⎨ ⎩ ⟦ s 1 ⟧σ k if ⟦ be ⟧σ = true; ⟦ s 2 ⟧σ k if ⟦ be ⟧σ = false
⟦ while be do s ⟧σ k = k′(σ) where k′ = lfp(λ k′. λ σ′. if ⟦ be ⟧σ′ then ⟦ s ⟧σ′ k′ else k(σ′))
skip과 대입 같은 기본 명령들의 경우, 의미 함수는 단지 명령 실행 후의 저장소를 계산하여 컨티뉴에이션 k에 전달한다.
순차의 경우, ⟦ s 1; s 2 ⟧σ k는 초기 저장소 σ와 컨티뉴에이션 λ σ′. ⟦ s 2 ⟧σ′ k로 s 1의 의미를 계산한다. 이는 s 1의 끝 저장소를 s 2의 초기 저장소로 두고, 컨티뉴에이션은 k로 두어 s 2의 의미를 계산하는 함수다. σ에서 시작한 s 1이 발산하는 경우는 따로 처리할 필요가 없다. ⟦ s 1 ⟧σ k′가 ⊥를 산출하고, 이 경우 컨티뉴에이션 k′를 호출하지 않도록 구성하기 때문이다.
if-then-else 조건문은 해당 분기(then이나 else)로 재귀하고, 같은 초기 저장소와 같은 컨티뉴에이션을 넘긴다.
while be do s 루프에서는, 루프 본문 s의 의미에 be가 거짓이 될 때까지 루프를 재실행하는 컨티뉴에이션을 줘야 한다. 이를 위해 최소 고정점을 이용하여 컨티뉴에이션 k′를 정의하는데, 다음을 만족한다:
k′(σ′) = ⎧ ⎨ ⎩ k(σ′) if ⟦ e ⟧σ′ = false; ⟦ s ⟧σ′ k′ if ⟦ e ⟧σ′ = true
그런 다음 루프 시작 저장소 σ에 k′를 적용한다. 루프가 종료하지 않으면 최소 고정점은 ⊥를 낸다. 루프가 종료하면, 최종 저장소 σ′가 초기 컨티뉴에이션 k로 전달된다.
이제 명령문의 표기적 의미론이 그 명령의 컨티뉴에이션에 접근할 수 있게 되었으므로, 이를 확장하여 레이블과 goto 점프를 다룰 수 있다. 이를 위해 의미 함수에 하나의 매개변수를 더 추가한다. 즉, 레이블에 컨티뉴에이션을 대응시키는 환경 ρ이다. goto L은 현재 컨티뉴에이션 k 대신, ρ에서 L에 대응된 컨티뉴에이션 ρ(L)을 호출한다.
보다 정확히, 의미 함수의 타입은 이제 다음과 같다.
⟦ s ⟧ : Env → Store → (Store → Res) ◥ 컨티뉴에이션 ◣ → Res
여기서 Res = Store + {⊥}는 이전과 같고, Env = Label →fin (Store → Res) 이다.
기본 명령, 순차, 조건, 루프에 대해서는 표기적 의미론이 본질적으로 변하지 않는다. 단지 환경 매개변수 ρ를 추가로 받고, 이를 하위 명령으로 전달한다.
⟦ skip ⟧ρ σ k = k(σ)
⟦ x := e ⟧ρ σ k = k(σ [x ↦ ⟦ e ⟧σ])
⟦ s 1; s 2 ⟧ρ σ k = ⟦ s 1 ⟧ρ σ (λ σ′. ⟦ s 2 ⟧ρ σ′ k)
⟦ if be then s 1 else s 2 ⟧ρ σ = ⎧ ⎨ ⎩ ⟦ s 1 ⟧ρ σ k if ⟦ be ⟧σ = true; ⟦ s 2 ⟧ρ σ k if ⟦ be ⟧σ = false
⟦ while be do s ⟧ρ σ k = k′(σ) where k′ = lfp(λ k′. λ σ′. if ⟦ be ⟧σ′ then ⟦ s ⟧ρ σ′ k′ else k(σ′))
goto 문은 현재 컨티뉴에이션 k를 무시한다. 대신 ρ에 저장된 L의 컨티뉴에이션을 다시 시작한다.
begin…end 블록 안의 레이블 L 정의는 L의 컨티뉴에이션을 환경에 L에 대응시키고, 이 확장된 환경에서 블록의 의미를 계산한다.
⟦ begin s 1; L: s 2 end ⟧ρ σ k = ⟦ s 1; s 2 ⟧ρ′ σ k where ρ′ = ρ [L ↦ k′] and k′ = λ σ′. ⟦ s 2 ⟧ρ′ σ′ k
확장된 환경 ρ′와 그에 대응하는 컨티뉴에이션 k′ 사이의 상호 재귀에 주목하라(보다 형식적으로는 최소 고정점으로 쓸 수 있다). 이는 s 2 안에 L로 점프가 있을 수 있음을 반영하며, 이런 루프의 의미는 필연적으로 최소 고정점을 수반한다.
표기적 의미론에서, 컨티뉴에이션은 수학적 객체로 표현된다. IMP 같은 단순한 언어에서는 (집합론의) 함수로, 함수나 지연 계산을 일급 값으로 다루는 더 풍부한 언어에서는 Scott 영역의 연속 함수로 표현된다. 다른 한편으로, 자유 변수를 가진 함수가 일급 값인 프로그래밍 언어에서는 컨티뉴에이션을 언어 자체의 함수로 표현할 수 있다. 이러한 컨티뉴에이션의 구체화 방식을 CPS 변환 이라 하며, CPS는 Continuation-Passing Style 의 약자다. CPS 변환은 다양한 용도가 있다. 7장에서 보듯 고급 함수형 프로그래밍 관용구를 지원하고, 8장에서 보듯 함수형 언어에서 점프에 상응하는 제어 연산자의 의미를 부여한다. 또한 아래에서 설명하듯 함수형 언어가 따르는 평가 전략을 명시하는 데에도 쓰인다.
CPS 변환의 형태. 표현식 e의 변환은 컨티뉴에이션에서 프로그램의 최종 값으로 가는 함수다:
(value of e → final value) ◥ 컨티뉴에이션 ◣ → final value
좀 더 구체적으로, e의 변환은 함수 λ k …이며,
예를 들어, 상수 c의 변환은 λ k . k c이다. c는 이미 값이므로 컨티뉴에이션에 곧바로 전달할 수 있다.
이 변환은 CPS(컨티뉴에이션 전달 스타일)의 함수를 만든다. 즉, 호출자에게 값을 반환하지 않고, 항상 추가 인자로 주어진 컨티뉴에이션을 호출하며 종료한다. CPS 변환 후 표현식의 값을 얻는 유일한 방법은 변환된 표현식을 항등 컨티뉴에이션 λ x . x에 적용하는 것이다.
CPS 변환은 비형식(untyped) 언어와 정적 타입 언어 모두에 잘 적용된다. 다만 타입에 미치는 효과를 살펴보는 것이 흥미롭다. 예컨대 표현식 e가 기초 타입 int라면, 그 변환의 타입은 (int → R) → R이다. 여기서 R은 “결과 타입”, 즉 전체 프로그램의 타입이고, int → R은 int 타입의 값을 기대하는 컨티뉴에이션의 타입이다(일반적인 경우는 13.2절 참조).
콜바이밸류에 대한 CPS 변환. 5.4절에서 소개한 함수형 언어 FUN을 생각하자. 평가 전략으로 콜바이밸류(call by value)를 가정하자. 즉, 함수 인자는 함수에 전달되기 전에 값으로 환원된다. 여기에 대응하는 CPS 변환 𝒞는 다음과 같이 표현식의 구조에 대한 재귀와 경우분석으로 정의된다:
𝒞(c) = λ k . k c
𝒞(x) = λ k . k x
𝒞(λ x . e) = λ k . k(λ x . 𝒞(e))
𝒞(e 1 e 2) = λ k . 𝒞(e 1)(λ v 1 . 𝒞(e 2)(λ v 2 . v 1 v 2 k))
𝒞(if e 1 then e 2 else e 3) = λ k . 𝒞(e 1)(λ v 1 . if v 1 then 𝒞(e 2) k else 𝒞(e 3) k)
콜바이밸류에서는 변수는 값에 바인드된다. 따라서 변수는 상수처럼 변환한다. 변수 x의 변환은 λ k . k x이다.
함수 추상 λ x . e 역시 값이므로 컨티뉴에이션 k에 곧바로 전달할 수 있다. 다만 함수의 본문 e는 변환되어, 두 인자(매개변수 x와 호출의 컨티뉴에이션 k)를 받는 함수 λ x . λ k …가 되어야 한다.
조건식 if e 1 then e 2 else e 3에서는 e 1의 불리언 값이 필요하다. 따라서 변환 결과는 𝒞(e 1)을 호출하고, e 1의 값을 v 1에 바인드하는 컨티뉴에이션 λ v 1 …을 넘긴다. 이어서 v 1 = true면 𝒞(e 2) k를, v 1 = false면 𝒞(e 3) k를 호출한다.
함수 적용 e 1 e 2도 유사하다. 어느 함수를 호출할지 알기 위해 e 1의 값이 필요하고, 콜바이밸류이므로 e 2의 값도 필요하다. 따라서 변환은 𝒞(e 1)을 호출하여 e 1의 값을 v 1에 바인드하는 컨티뉴에이션 λ v 1 …을 넘기고, 이어서 𝒞(e 2)을 호출하여 e 2의 값을 v 2에 바인드하는 컨티뉴에이션 λ v 2 …을 넘긴 뒤, 마지막으로 실제 적용 v 1 v 2 k를 수행하며, 적용의 컨티뉴에이션 k를 함수에 전달한다.
행정적 축약. 위 CPS 변환은 명백히 중복된 계산을 포함하고, 우리가 손으로 쓸 식보다 장황한 항들을 만든다. 예를 들어, f와 x가 변수인 적용 f x의 경우, 다음을 얻는다.
𝒞(f x) = λ k. (λ k 1. k 1 f) (λ v 1. (λ k 2. k 2 x) (λ v 2. v 1 v 2 k))
기대하는 변환 λ k . f x k 대신에 말이다.
이러한 장황함은 CPS 변환 결과에 대해 이른바 행정적 축약(administrative reductions) →adm 을 수행함으로써 피할 수 있다. 이 축약은 변환이 도입한 “행정적 적(redex)”을 제거하는 β-축약이다. 특히 다음을 갖는다.
(λ k. k a)(λ x. e) →adm (λ x. e) a →adm e [x := a]
단, a가 아톰(atom): 변수 또는 값(상수나 λ-추상)일 때.
또는 Danvy et al. (2007)의 원패스(one-pass) CPS 변환을 사용하면, 행정적 적이 없는 항을 직접 생성할 수 있다. 이 원패스 변환은 아톰 a에 대한 Ψ(a)와, 컨티뉴에이션을 나타내는 아톰 k를 인자로 받는 일반 표현식 e에 대한 𝒞 1(e, k) 두 함수로 정의된다. 아톰이 아닌 “진지한(serious)” 표현식을 s로 표기한다.
Ψ(c) = c
Ψ(x) = x
Ψ(λ x . e) = λ x. λ k. 𝒞 1(e, k)
𝒞 1(a, k) = k Ψ(a)
𝒞 1(a 1 a 2, k) = Ψ(a 1) Ψ(a 2) k
𝒞 1(a 1 s 2, k) = 𝒞 1(s 2, λ v 2. Ψ(a 1) v 2 k)
𝒞 1(s 1 a 2, k) = 𝒞 1(s 1, λ v 1. v 1 Ψ(a 2) k)
𝒞 1(s 1 s 2, k) = 𝒞 1(s 1, λ v 1. 𝒞 1(s 2, λ v 2. v 1 v 2 k))
𝒞 1(if a then e 1 else e 2, k) = if Ψ(a) then 𝒞 1(e 1, k) else 𝒞 1(e 2, k)
𝒞 1(if s then e 1 else e 2, k) = 𝒞 1(s, λ v. if v then 𝒞 1(e 1, k) else 𝒞 1(e 2, k))
콜바이밸류 CPS 변환 예시. 아래 예시에서 f, g, h, x, y는 변수이다. 결과는 =adm 기호가 시사하듯, 행정적 축약 후의 형태로 적는다. 다음을 얻는다:
𝒞(f(g x)) =adm λ k. g x (λ v. f v k)
CPS 변환이 평가 순서를 어떻게 명시하는지 보라. 먼저 인자 g x를 계산하여 v에 바인드하고, 그 다음 f를 v에 적용한다. 같은 맥락에서,
𝒞(f(if y then g x else h x)) =adm λ k. (λ k′. if y then g x k′ else h x k′) (λ v. f v k)
여기서는 중간 컨티뉴에이션 λ v. f v k를 변수 k′에 바인드하여, 불리언 y에 따라 g와 h의 호출에 사용한다.
좀 더 현실적인 예로, FUN 언어가 let rec 형태의 재귀 함수 정의를 지원한다고 하자. 다음은 팩토리얼 함수와 그 CPS 변환이다:
𝒞(let rec fact = λ n. if n=0 then 1 else n × fact(n−1)) =adm let rec fact = λ n. λ k. if n=0 then k 1 else fact(n−1)(λ v. k(n × v))
원래 함수와 달리, 변환된 함수는 꼬리 재귀임에 주목하라. else 분기는 인자 n−1과 컨티뉴에이션을 직접 fact에 넘겨 호출한다. 이 컨티뉴에이션은 결과에 n을 곱한 뒤, 원래 컨티뉴에이션 k에 전달한다.
콜바이네임에 대한 CPS 변환. 콜바이밸류의 대안으로, FUN 프로그램을 콜바이네임(call by name)으로 평가할 수 있다. 함수 적용의 인자 e는 평가되지 않은 채 함수에 전달되어 매개변수 x에 바인드된다. x의 값이 필요할 때에만 인자 e가 평가된다. 더구나 평가의 공유가 없어서, x가 필요할 때마다 e는 다시 평가된다. 이러한 평가 전략의 변화는 콜바이네임 CPS 변환 𝒩에 반영된다:
𝒩(c) = λ k. k c
𝒩(x) = x
𝒩(λ x . e) = λ k. k(λ x . 𝒩(e))
𝒩(e 1 e 2) = λ k . 𝒩(e 1)(λ v 1 . v 1 𝒩(e 2) k)
𝒩(if e 1 then e 2 else e 3) = λ k . e 1(λ v 1 . if v 1 then 𝒩(e 2) k else 𝒩(e 3) k)
각 경우는 콜바이밸류 변환 𝒞의 경우와 유사하나, 변수와 함수 적용의 경우가 다르다. 함수 적용 e 1 e 2의 경우 인자 e 2는 평가하지 않는다. 대신 그 CPS 변환 𝒩(e 2)를 함수에 전달한다. 이는 e 2의 평가를 지연시키는데, CPS 변환은 컨티뉴에이션 k를 기다렸다가 e 2의 평가를 진행하는 함수 λ k …이기 때문이다.
함수 인자가 CPS 변환된 항으로 전달되므로, 모든 변수도 CPS 변환된 항에 바인드된다. 따라서 변수 x의 변환은 그냥 x이다. 이를 콜바이밸류 번역과 비교하라. 콜바이밸류에서는 변수 x가 값에 바인드되므로, 그 CPS 변환 λ k. k x는 컨티뉴에이션 k를 받아 즉시 값 x에 적용한다. 콜바이네임에서는 변수 x가 CPS 변환된 항에 바인드되므로, x의 값을 얻으려면 컨티뉴에이션 k에 적용해야 한다. 따라서 x의 CPS 번역은 λ k. x k이고, 이는 x로 단순화될 수 있다.
콜바이네임 CPS 변환 예시. 변수 f와 x에 대한 함수 적용 f x는 다음이 된다.
𝒩(f x) =adm λ k. f (λ v. v x k)
f는 변수이지만 임의의 계산을 나타내므로, 값 v를 얻기 위해 먼저 평가되어야 한다. 인자 x는 이미 CPS 변환된 항이므로 그대로 전달된다.
더 복잡한 적용 f(g x)를 생각하자. CPS 변환은 다음과 같다.
𝒩(f(g x)) =adm λ k. f (λ v. v (λ k′. g (λ v′. v′ x k′)) k)
여기서도 f는 그 값 v를 회복하기 위해 컨티뉴에이션에 적용된다. 인자 g x는 평가되지 않은 채로, CPS 변환된 형태로 v에 전달된다.
CPS 항의 형태. CPS 변환이 만들어 내는 항은 다음 문법으로 묘사되는 특정한 형태를 가진다:
아톰: a ::= x ∣ c ∣ λ v . b ∣ λ x . λ k . b
함수 본문: b ::= a ∣ a 1 a 2 ∣ a 1 a 2 a 3
하나의 인자(컨티뉴에이션)를 받는 함수와 두 인자(CPS 변환된 함수)를 받는 함수가 있으며, 이들의 본문은 한두 개의 인자에 대한 함수 적용으로 이뤄진다. 이 적용에서 함수 부분과 인자 부분은 아톰, 즉 변수, 상수, 함수 추상이다.
두 인자 적용 a 1 a 2 a 3을 단일 적용으로 간주하고 커리드된 두 적용 (a 1 a 2) a 3로 보지 않는다는 전제하에, CPS 함수 안에서의 함수 적용은 항상 꼬리 위치에 있다. 결과적으로, CPS 변환된 항은 호출 스택 없이도 평가할 수 있다. 함수 호출에 전달되는 컨티뉴에이션이 스택 기반 평가자에서의 스택 프레임 역할을 하기 때문이다.
임의의 소스 항 e에 대해, CPS 변환 𝒞(e)와 𝒩(e)는 아톰이며, 초기 컨티뉴에이션에 대한 적용 𝒞(e)(λ x . x)과 𝒩(e)(λ x . x)은 함수 본문이다. 원패스 최적화된 CPS 변환에서는, k가 아톰일 때 𝒞 1(e, k)는 함수 본문이다.
평가 전략에 대한 무관성. Plotkin (1975) 등이 CPS 변환을 형식적으로 연구한 동기 중 하나는, 콜바이네임과 콜바이밸류 같은 평가 전략을 원하는 연산적 의미론에 의존하지 않고, 변환된 항 안에서 명시적으로 드러내기 위함이었다. 실제로 다음 결과(Plotkin이 “무관성(indifference) 성질”이라 부른다)가 성립한다.
정리 1(무관성) CPS로 변환된 프로그램은 콜바이네임, 콜바이밸류, 그리고 임의의 약 축약 전략에서 동일하게 평가된다.
이 결과가 닫힌(closed) 함수 본문 b에 대해 성립함을 보이자. b는 a 1 또는 a 1 a 2 또는 a 1 a 2 a 3의 형태이며, 여기서 a i는 닫힌 아톰, 즉 값이다. 따라서 a i 안에서는 어떤 약 축약도 일어날 수 없고, b의 맨 위에서만 축약이 일어날 수 있다:
(λ v . b′) a 2 → b′ [v := a 2]
(λ x . λ k . b′) a 2 a 3 → (λ k . b′ [x := a 2]) a 3 → b′ [x := a 2, k := a 3]
인자들이 값이므로, 이러한 베타 축약은 콜바이네임과 콜바이밸류 모두에서 유효하다. 아톰은 변수에 아톰을 치환해도 안정적이므로, 축약의 결과는 닫힌 함수 본문이다.
이는 닫힌 함수 본문에 대해 가능한 약 축약 수열이 오직 하나임을 보여 준다. 이제 e가 닫힌 소스 항이라면, 그 CPS 변환을 초기 컨티뉴에이션에 적용한 𝒞(e)(λ x . x) 또는 𝒩(e)(λ x . x)은 닫힌 함수 본문이다. 바라는 결과가 따른다.
의미 보존. Plotkin (1975)의 또 다른 중요한 결과는 CPS 변환이 프로그램의 의미를 보존한다는 것이다. 즉, 표현식 e의 콜바이밸류 CPS 변환 𝒞(e)를 초기 컨티뉴에이션 λ x . x에 적용한 결과는 원래 표현식 e를 콜바이밸류 의미론으로 평가한 결과와 동일하다. 이 결과는 콜바이네임에도 성립한다.
정리 2(CPS 변환은 의미를 보존한다.) 모든 항 e와 상수 c에 대해,
위 명제에서, →v 는 콜바이밸류 축약, →n 은 콜바이네임 축약, → 는 고정된 전략 없이 하는 약 축약이다.
먼저 Danvy et al. (2007)의 원패스 최적화 콜바이밸류 CPS 변환에 대해 의미 보존의 증명 개요를 제시한다. 이는 행정적 축약의 일부 어려움을 피한다. 먼저 소스 수준 콜바이밸류 축약이 CPS 변환의 약 축약에 의해 시뮬레이션됨을 보인다. 즉, e →v e′이면 임의의 컨티뉴에이션 k에 대해 𝒞 1(e, k) →+ 𝒞 1(e′, k)이다. 이는 머리(head) 축약 (λ x . e) v →v e [x := v]의 경우 성립한다. 왜냐하면
𝒞 1((λ x . e) v, k) = (λ x . λ k′ . 𝒞 1(e, k′)) Ψ(v) k
→ (λ k′ . 𝒞 1(e, k′) [x := Ψ(v)]) k
→ 𝒞 1(e, k′) [x := Ψ(v), k′ := k]
= 𝒞 1(e [x := v], k)
이 결과는 문맥 C[e] →v C[e′] 아래의 축약으로도 C의 구조에 대한 귀납과 경우분석으로 확장된다.
또한 막힌(stuck) 소스 항, 즉 값이 아니고 축약도 불가능한 항(c v처럼 상수를 함수로 적용한 경우 등)에 대해서도 유사한 결과가 성립한다. e가 막혀 있으면, 𝒞 1(e, k)도 막혀 있다.
이제 모든 것을 합치면 세 경우가 있다:
성질 (1)은 e →v* c 이면 𝒞 1(e, λ x . x) →* c 임을 증명한다. 역은 무관성 정리를 이용한다. 만약 𝒞 1(e, λ x. x)가 c로 축약된다면, 다른 어떤 값으로도 축약될 수 없고, 발산하거나 잘못될 수도 없다. 따라서 e →v* c 여야만 한다. 그렇지 않으면 (1), (2), (3) 중 하나가 거짓이 된다.
위 개략 증명은 표준 콜바이밸류 CPS 변환 𝒞(e)에는 곧장 적용되지 않는다. 일반적으로 e →v e′가 𝒞(e) k →+ 𝒞(e′) k를 함의하지 않기 때문이다. 이 문제를 피하기 위해, Plotkin (1975)는 콜론 번역(colon translation) e : k를 정의한다. 이는 𝒞(e) k에서 적절히 선택된 행정적 적 일부를 축약한 것이다. 우리는 𝒞(e) k →* e : k 이고, e →v e′이면 e : k →+ e′ : k 임을 갖는다. 이 성질들을 이용해 위 (1), (2), (3)에 상응하는 성질을 보일 수 있고, 결론에 이른다.
Nielson and Nielson (2007)의 교과서는 IMP 같은 1차 언어에 대한 연산적/표기적 의미론을 잘 소개한다. Winskel (1993)의 교과서는 더 나아가, FUN 같은 고차 언어에 표기적 의미론을 부여하는 데 필요한 영역 이론의 요소들을 포함한다.
Reynolds (1993)는 컨티뉴에이션 개념의 역사적 고찰을 제공하며, Algol 60의 점프에 의미를 부여하기 위한 시도와, 함수형 언어의 구현 기법으로서 여러 차례 재발견된 과정을 보여 준다.
Friedman and Wand (2008)의 5, 6장은 함수형 언어의 컨티뉴에이션과 CPS 변환에 대한 좋은 입문서다. Danvy and Filinski (1992)는 CPS 변환을 심도 있게 연구한다.
