프로그래밍 언어 의미론: 구문, 바인딩, 람다 계산, 평가 전략

타입 검사·추론·다형성·건전성은 타입 시스템에, 컴파일러·VM·인터프리터 구현 방식은 프로그램이 실행되기까지에 있다.

구문과 의미론

문법에 맞는 프로그램도 실행 중에 실패한다. int[] a = new int[3]; a[5] = 1;(범위 초과), 10 / n에서 n = 0, null.length(), 끝나지 않는 while (true)는 모두 구문상 완벽하다. 구문은 모양만, 의미론은 동작을 정한다. 둘 사이에서 일부 의미 오류를 실행 전에 걸러 내는 것이 타입 시스템이다.

구체 구문과 추상 구문 트리

구체 구문(concrete syntax) 은 사람이 쓰는 문자열 그대로이고, 괄호·세미콜론·공백 같은 표기용 기호가 들어 있다. 추상 구문 트리(AST) 는 의미에 필요한 구조만 남긴 트리다. 파서가 구체 구문을 AST로 바꾼다.

1 + 2 * 3          (1 + 2) * 3
 
    +                   *
   / \                 / \
  1   *               +   3
     / \             / \
    2   3           1   2

• 연산자 우선순위와 결합 방향은 트리의 모양으로 바뀐다. 우선순위가 높은 연산이 트리의 더 깊은 곳(먼저 계산되는 곳)에 놓인다.
• 괄호는 AST에 노드로 남지 않는다. 괄호의 역할은 트리 모양을 바꾸는 것뿐이고, 모양이 정해진 뒤에는 필요 없다.
• 우선순위를 다루는 파싱 기법은 프랫 파싱에 있다.

의미론을 정의하는 세 방식

작은 단계와 큰 단계 연산 의미론

타입 건전성의 진행·보존 정리가 작은 단계 의미론 위에서 정의되는 이유가 중간 상태와 「막힘」을 표현할 수 있기 때문이다.

변수, 바인딩, 스코프

바인딩(binding) 은 이름을 무언가(값, 메모리 위치, 함수)에 연결하는 것이다. 식 안의 변수는 둘 중 하나다.

• 바인딩된 변수(bound variable): 그 식 안의 바인더(함수 매개변수, let)가 도입한 변수. λx. x + y의 x.
• 자유 변수(free variable): 식 안에 바인더가 없어 바깥 환경에서 의미를 얻는 변수. 위 식의 y.

자유 변수의 뜻을 어디서 찾느냐가 스코프 규칙이다.

x = 1
def f(): return x
def g():
    x = 2
    return f()
g()   # 렉시컬 스코프: 1 (f가 정의된 곳의 x)
      # 동적 스코프:   2 (f를 부른 g의 x)

렉시컬 스코프는 코드만 읽고 이름이 무엇을 가리키는지 알 수 있어 추론과 컴파일이 쉽다. 동적 스코프는 호출 경로마다 의미가 달라진다.

클로저

클로저(closure)는 함수 코드와, 그 함수의 자유 변수를 정의 시점의 바인딩으로 묶은 환경의 쌍이다. 렉시컬 스코프를 지키면서 함수를 값으로 넘기려면, 함수가 만들어진 곳의 변수를 함수와 함께 가지고 다녀야 하기 때문이다.

반복문 안에서 만든 클로저들이 같은 변수를 캡처하면 모두 마지막 값을 본다. JavaScript의 var 반복문, Go 1.21까지의 for 반복 변수가 이 함정이었고, let과 Go 1.22는 반복마다 새 변수를 만들어 해결했다. JavaScript에서 클로저가 실행 컨텍스트로 구현되는 방식은 실행 컨텍스트에 있다.

람다 계산

람다 계산(lambda calculus) 은 함수 정의와 적용만으로 계산을 표현하는 최소 형식 체계다(Church, 1930년대). 함수형 언어의 이론적 기반이다. 식은 세 가지뿐이다.

(λx. x + 1) 4  →β  4 + 1  →  5
(λf. λx. f (f x)) (λy. y * 2) 3  →β  (λx. (λy. y*2) ((λy. y*2) x)) 3  →β ... →  12

여러 인자 함수는 함수를 돌려주는 함수로 표현한다(λx. λy. x + y). 이것이 커링의 기원이다.

알파 변환, 베타 축약, 변수 포획

• 알파 변환(α-conversion): 바인딩된 변수의 이름을 일관되게 바꿔도 의미가 같다. λx. x와 λy. y는 같은 함수다.
• 베타 축약(β-reduction): 적용 (λx. e) a를 본문 e의 x를 a로 치환한 식으로 바꾼다. 계산의 한 단계다.
• 변수 포획(variable capture): 치환할 인자 안의 자유 변수가 본문의 바인더에 잘못 걸리는 현상이다.

(λx. λy. x) y
잘못된 치환:  λy. y         ← 인자의 자유 변수 y가 안쪽 λy에 붙잡혀 항등 함수가 됐다
올바른 치환:  먼저 α 변환 λx. λz. x  →  λz. y   ← 「y를 돌려주는 상수 함수」

포획을 허용하면 이름을 바꿨을 뿐인 같은 함수가 다른 결과를 낸다. 그래서 치환은 포획 회피 치환(capture-avoiding substitution) 으로 정의하고, 충돌하는 바인더를 먼저 알파 변환한다. 컴파일러는 이름 대신 바인더까지의 거리를 쓰는 드 브라윈 인덱스(de Bruijn index)로 이 문제를 아예 없애기도 한다. 같은 문제가 매크로 전개에서도 생긴다(아래 「위생적 매크로」).

함수를 값으로 다루기

고차 함수는 일급 함수가 있어야 쓸 수 있다. 커링한 함수에 앞쪽 인자만 넘기면 부분 적용이 되므로 둘은 함께 쓰이지만, 커링은 형태 변환이고 부분 적용은 인자 고정이다. 순수 함수·불변성 같은 함수형 프로그래밍의 원리는 프로그래밍 패러다임에, JavaScript 구현은 함수형 프로그래밍에 있다.

평가 전략

인자를 언제 평가하느냐에 따른 구분이다.

f(x, y) = if x > 0 then x + x else 0
f(3, loop())
  값에 의한 호출:   loop()를 먼저 평가 → 끝나지 않는다
  이름·필요:        y를 쓰지 않으므로 3 + 3 = 6
f(expensive(), 0)
  이름에 의한 호출: expensive()를 비교 1번 + 덧셈 2번 = 3번 평가
  필요에 의한 호출: 1번 평가하고 재사용

엄격한 언어도 &&, ||, if의 단락 평가, Python 제너레이터, Java 스트림처럼 일부를 지연 평가한다.

값·참조·공유에 의한 전달

인자를 어떻게 넘기느냐의 구분은 함수 안의 대입이 호출자에게 보이느냐로 갈린다.

void swap(a, b) { t = a; a = b; b = t; }
참조에 의한 호출: 호출자의 두 변수가 실제로 바뀐다
값·공유에 의한 호출: 아무 일도 없다. 그래서 Java로는 swap을 짤 수 없다

「객체 참조를 값으로 전달」하는 Java·Python 방식은 엄밀히는 값에 의한 호출이다. 복사되는 값이 참조일 뿐이다. 이를 따로 공유에 의한 호출이라 부른다(CLU, 1974). Java의 예는 Java 언어 기본에 있다. C는 값에 의한 호출만 있고, 포인터를 값으로 넘겨 참조 전달을 흉내 낸다.

값과 참조 두 가지로는 모든 언어를 설명할 수 없다. 공유에 의한 호출 외에도, 이름·필요에 의한 호출(평가 시점이 다르다), 복사-복원(copy-in copy-out, value-result)(값을 복사해 넘기고 반환 시 호출자 변수에 다시 쓴다. Ada in out, Fortran 일부 구현. 별칭이 있을 때 참조 전달과 결과가 다르다), Rust의 이동(move)(소유권을 넘겨 호출자가 더는 못 쓴다)과 &·&mut 빌림이 있다.

환경, 저장소, 별칭

명령형 언어의 의미론은 두 사상을 나눈다.

둘을 나누는 이유는 별칭(aliasing), 즉 이름 둘이 같은 위치를 가리키는 상황을 설명하기 위해서다.

int x = 1;
int& y = x;    // 환경: x ↦ ℓ1, y ↦ ℓ1      저장소: ℓ1 ↦ 1
y = 5;         // 저장소만 바뀐다: ℓ1 ↦ 5   → x를 읽어도 5

이름에서 바로 값으로 가는 사상 하나로는 「y에 대입했는데 왜 x가 바뀌나」를 표현할 수 없다. 별칭은 참조 전달, 포인터, 같은 객체를 가리키는 두 참조에서 생기고, 컴파일러 최적화(값을 레지스터에 두어도 되는가)와 프로그램 추론을 어렵게 한다. Rust의 「가변 참조는 하나만」 규칙과 C의 restrict는 별칭이 없음을 보장해 이 문제를 줄인다.

순수성과 참조 투명성

순수 함수(pure function) 는 같은 입력에 항상 같은 출력을 내고, 부수 효과(전역 상태 변경, 입출력, 예외로 인한 제어 이동)가 없는 함수다. 참조 투명성(referential transparency) 은 식을 그 결과값으로 바꿔 써도 프로그램의 의미가 변하지 않는 성질이다. 순수 함수 호출은 참조 투명하다.

부수 효과가 있으면 이 치환이 깨진다.

let a = counter.next()     // 부수 효과: 내부 상태를 1 올린다
a + a        ≠    counter.next() + counter.next()    // 1+1 과 1+2
print("hi"); print("hi")   ≠    let p = print("hi"); p; p   // 출력 횟수가 다르다

그래서 공통 부분식 제거, 호출 결과 캐시(메모이제이션), 평가 순서 변경, 지연 평가, 병렬화 같은 변환은 식이 순수할 때만 안전하다.

연속과 CPS

연속(continuation) 은 「이 식의 값이 나온 뒤에 프로그램이 할 나머지 계산 전부」다. print(f(x) + 1)에서 f(x)의 연속은 「결과에 1을 더해 출력하라」다. 연속 전달 방식(CPS) 은 함수가 값을 반환하는 대신 나머지 계산을 인자 k로 받아 결과를 넘기는 방식이다.

직접 방식:  add1(x) = x + 1          print(add1(f(x)))
CPS:        add1(x, k) = k(x + 1)    f(x, v => add1(v, w => print(w)))

CPS에서는 모든 호출이 꼬리 호출이 되고 「다음에 할 일」이 값으로 드러나, 예외·제너레이터·async/await·백트래킹을 같은 장치로 구현할 수 있다. 컴파일러의 중간 표현으로도 쓴다. Scheme은 call/cc로 현재 연속을 일급 값으로 잡는다. 비동기 코드와 코루틴에서의 쓰임은 동시성 모델의 「컨티뉴에이션과 CPS」에 있다.

프로그램 동치와 검증

무엇을 관찰하느냐에 따른 동치

두 프로그램이 같은지는 무엇을 관찰하는가에 따라 달라진다. 반환값만 보면 같아도 다음을 관찰하면 다르다.

이론에서는 문맥 동치(contextual equivalence) 를 쓴다. 어떤 프로그램 문맥 C[·]에 넣어도 관찰 결과(종료 여부와 최종 값)가 같으면 두 식은 동치다. 최적화는 이 동치를 지키는 변환이어야 한다.

Hoare 논리

Hoare 트리플 {P} S {Q}는 「사전 조건 P가 참인 상태에서 S를 실행해 끝나면 사후 조건 Q가 참이다」를 뜻한다.

{ i = 0 ∧ s = 0 }
while i < n:          불변식 I:  s = 0 + 1 + ... + (i-1)  ∧  i ≤ n
    s = s + i
    i = i + 1
{ s = n(n-1)/2 }      I ∧ ¬(i < n)  ⇒  i = n  ⇒  사후 조건

• 반복문 불변식(loop invariant): 반복 전에 참이고, 매 반복이 지키는 명제다. 반복이 끝났을 때 「불변식 ∧ ¬조건」에서 사후 조건을 끌어낸다.
• 부분 정당성(partial correctness): 끝난다면 결과가 옳다. 불변식만으로 증명한다. 무한 루프도 부분적으로는 정당하다.
• 전체 정당성(total correctness): 반드시 끝나고 결과도 옳다. 부분 정당성에 변형식(variant), 즉 매 반복 줄어드는 0 이상의 값(위에서는 n - i)을 더해 종료를 증명한다.

메타프로그래밍과 언어 구현

매크로와 위생

C 전처리기 매크로는 텍스트 치환이라 #define SQ(x) x*x에서 SQ(a+1)이 a+1*a+1이 되고, 매크로 안에서 만든 임시 변수가 사용자 변수와 이름이 겹칠 수 있다(변수 포획). 위생적 매크로(hygienic macro) 는 이름이 정의된 문맥 정보를 식별자에 붙여 둔다. 매크로가 도입한 tmp와 사용자 코드의 tmp는 철자가 같아도 다른 바인딩으로 취급되고, 매크로 본문의 자유 변수는 매크로 정의 지점의 바인딩을 따른다. 람다 계산의 포획 회피 치환을 매크로 전개에 적용한 것이다. Scheme syntax-rules, Racket, Rust macro_rules!(지역 변수에 대해)가 위생적이다.

컴파일과 해석은 구현의 성질이다

컴파일·해석은 언어가 아니라 구현의 성질이다. 언어 명세는 의미만 정하고, 그 의미를 실행하는 방법은 구현이 고른다. C++ 인터프리터(Cling)도 있고 Python 컴파일러(Cython, Nuitka)도 있다.

한 언어 구현이 여러 방식을 함께 쓰는 것이 보통이다. HotSpot JVM은 바이트코드를 먼저 인터프리터로 실행하고, 자주 도는 메서드를 C1·C2 JIT로 단계적으로 컴파일한다(JVM 내부 구조). V8은 바이트코드 인터프리터(Ignition)로 시작해 최적화 컴파일러로 넘어간다. CPython도 소스를 바이트코드로 컴파일한 뒤 해석한다. 세 갈래의 비교는 프로그램이 실행되기까지에 있다.

의미를 보존하는 최적화

컴파일러 최적화가 의미를 보존한다는 것은 최적화 전후의 프로그램이 관찰 가능한 동작(출력, 부수 효과의 순서, 종료 여부, 최종 값)이 같다는 뜻이다. 언어가 정의하지 않은 것(C의 정의되지 않은 동작, 지정되지 않은 평가 순서)은 관찰 대상이 아니므로 컴파일러가 자유롭게 바꾼다.

멀티스레드에서는 단일 스레드 기준으로 의미를 보존한 재배치가 다른 스레드에게 보이는 순서를 바꾼다. 그래서 언어마다 메모리 모델로 허용 범위를 정한다(Java 동시성의 Java 메모리 모델).

정리

• 구문은 올바른 프로그램의 모양을, 의미론은 동작을 정한다. AST는 괄호를 버리고 우선순위를 트리 모양으로 담는다.
• 연산 의미론은 실행 규칙으로, 표시 의미론은 수학적 대상으로, 공리적 의미론은 논리 명제로 의미를 정한다.
• 렉시컬 스코프에서 클로저는 함수 코드와 정의 시점 환경의 쌍이다. 변수를 캡처하면 바뀐 값이 보이고, 값을 복사하면 보이지 않는다.
• 베타 축약은 포획 회피 치환으로 해야 하고, 같은 원리가 위생적 매크로다.
• 값·이름·필요에 의한 호출은 평가 시점, 값·참조·공유에 의한 호출은 대입이 호출자에게 보이는지의 차이다.
• 부수 효과가 있으면 참조 투명성이 깨져 최적화와 추론의 자유가 줄어든다. 동치는 관찰 대상에 따라 달라진다.

관련 노트: 타입 시스템, 프로그램이 실행되기까지, 프로그래밍 패러다임, 함수형 프로그래밍, 동시성 모델, 프랫 파싱, 실행 컨텍스트