3장: 람다 대수

새 파일

• src/names.rs
• src/normal.rs

변경된 파일

• src/eval.rs
• src/ast.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs

동기

우리 계산기는 수에 이름을 붙일 수 있습니다. 계산에 이름을 붙이고 그것을 여러 입력에 사용할 수 있다면 어떨까요? 그것이 바로 함수이며, 함수를 추가하면 놀라울 만큼 많은 것을 할 수 있게 됩니다. 람다와 적용만으로 순수 비타입 람다 대수를 표현할 수 있습니다. 처치 인코딩(Church encoding)에서 보겠지만, 데이터조차 함수로 표현할 수 있습니다 (Pierce 2002). 구문 두 가지만으로 이만큼의 표현력을 얻는다니 놀랍습니다!

제대로 짚고 넘어가야 할 세부 사항이 몇 가지 있습니다. 두 변수의 이름이 모두 x라면, 함수가 가리키는 것이 어느 쪽인지 어떻게 알 수 있겠습니까? 또 함수를 호출할 때 인자를 먼저 평가해야 하겠습니까? Rust의 답을 슬쩍 빌려 쓰는 대신, 치환과 클로저를 직접 만들어 그 답을 눈으로 확인하겠습니다.

현재의 언어

프로그램은 여전히 단일 식입니다. 람다는 매개변수를 하나 받고, 적용은 왼쪽 결합이며, 불리언이 if 식을 제어합니다. 비교는 정수 연산입니다. 아직 타입 표기는 없습니다.

let twice = \f -> \x -> f (f x) in twice (\x -> x + 1) 0

클로저는 자신의 람다가 평가된 곳에 있던 바인딩을 기억합니다. let x = 1 in let f = \y -> x + y in let x = 100 in f 2의 결과는 3입니다. 대신 호출한 쪽의 x 바인딩을 사용한다면 동적 스코프가 됩니다.

이론

비타입 문법

순수한 타입 없는 람다 대수에는 형태가 단 세 가지뿐입니다. 식은 변수, 적용, 추상 중 하나입니다. 각 세로 막대는 “또는“으로 읽으십시오.

$$\begin{array}{rlrl}e& =x& & \text{variable}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x.e& & \text{abstraction}\end{array}$$

이것이 대수의 전부입니다! 우리의 작은 언어는 모든 수와 불리언을 함수로 인코딩하지 않고도 실험할 수 있도록 몇 가지 편의 기능을 더합니다.

$$\begin{array}{rlrl}e& =\cdots & & \text{the three forms above}\\ & \mid n& & \text{integer literal}\\ & \mid \text{True}\mid \text{False}& & \text{boolean literal}\\ & \mid \text{let}x=e_1\text{in}{e}_2& & \text{local binding}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid -e& & \text{integer negation}\\ & \mid e_{1}op{e}_2& & \text{binary operation}\end{array}$$

여기서 $n$은 정수이고 $op$는 +, -, *, /, ==, <, <= 중 하나입니다. 괄호는 트리 노드를 추가하지 않고 식을 묶습니다. 파서에는 오류 복구를 위한 Error 자리 표시자도 있지만, 이는 받아들여지는 프로그램의 형태가 아닙니다. “타입 없는”이라는 말은 아직 정적 타입 검사기가 없다는 뜻이지, 이 형태들을 어떻게 조합하든 런타임에 의미가 있다는 뜻이 아닙니다.

축약과 평가

람다를 호출한다는 것은 그 매개변수를 주어진 인자로 치환한다는 뜻입니다. 이 단계를 베타 축약(beta reduction)이라고 부릅니다. \x -> x + 1을 41에 적용하면, x를 치환하여 41 + 1을 얻습니다. 여기까지는 문제가 없습니다. 미묘한 문제는 이름이 반복될 때 시작됩니다. 우리는 본문에서 매개변수의 자유 출현만 치환하며, 안쪽 바인더가 인자의 자유 이름을 포획하게 된다면 그 바인더의 이름을 바꿉니다. 바로 그 실수를 아래에서 직접 살펴보겠습니다 (Pierce 2002).

평가 순서는 다음에 어떤 축약을 수행할지 결정합니다. 정규 순서는 가장 왼쪽의 가장 바깥쪽 축약 가능한 식을 택하며, 우리의 완전 축약기는 람다 안쪽까지 계속 축약합니다. 값에 의한 호출은 먼저 함수와 그 인자를 평가한 다음 본문으로 들어갑니다. 람다 자체는 이미 값입니다.

그 차이는 함수가 영원히 실행될 인자를 무시할 때 드러납니다. 정규 순서는 그 인자를 건너뛸 수 있습니다. 값에 의한 호출은 그 인자를 계산하려다 막혀 버립니다. Y 콤비네이터는 특히 인상적인 예를 보여 줍니다. Y 조합자는 정규 순서에서는 팩토리얼을 계산하지만, 우리의 엄격한 평가기에서는 연료를 모두 소진합니다. 연료가 바닥났다는 것은 우리 실험의 한계에 도달했다는 뜻이지, 그 계산이 결코 끝나지 않음을 증명했다는 뜻이 아닙니다.

왜 드 브루인 인덱스인가?

이름은 프로그램을 읽는 데 도움이 되지만, 이름의 철자는 바인딩과는 무관합니다. \x -> x와 \answer -> answer는 같은 함수를 나타냅니다. 우리는 이 둘을 알파 동치(alpha-equivalent)라고 부릅니다. 묶인 변수의 이름을 일관되게 바꾸는 것은 아무것도 바꾸지 않습니다. 하지만 두 구문 트리를 직접 비교하면 서로 다른 문자열이 나옵니다. 이름 있는 항을 다시 쓰는 컴파일러는 무해한 이름 바꾸기와, 어떤 출현이 가리키는 바인더 자체가 바뀌는 변화를 계속 구별해야 합니다.

y가 자유 변수인 다음 열린 항의 축약을 살펴봅시다:

(\x -> \y -> x) y

x를 y로 기계적으로 바꾸면 \y -> y가 됩니다. 이는 틀렸습니다. 이 함수는 자기 매개변수와 관계없이, 인자로 주어진 자유 변수 y를 반환해야 합니다. 먼저 안쪽 매개변수의 이름을 바꾸십시오:

(\x -> \z -> x) y
→ \z -> y

이것이 우리의 치환 함수가 해결해야 하는 포획(capture) 문제입니다. 드 브루인 인덱스(De Bruijn index)는 새 이름의 철자에 의존하지 않는 바인딩 표현을 제공합니다. 각 묶인 출현을 0부터 세어 그 바인더까지의 거리로 바꾸십시오. 적용 노드나 소스 줄이 아니라, 감싸고 있는 바인더를 세십시오.

아래 예제에서는 이름 없는 람다를 λ. body로 씁니다. 여기 나오는 숫자는 정수 리터럴이 아니라 변수 인덱스입니다. 이는 설명을 위한 표기법이지, 이 장의 파서가 받는 입력 구문이 아닙니다.

더 긴 예로 \f -> \x -> f (f x) 안으로 들어가 봅시다. 첫 번째 람다에 들어가면 f를 스코프 스택에 넣습니다. 두 번째 람다에 들어가면 x를 넣습니다:

scope, nearest first:  [x, f]
index:                  0  1

f (f x)                 1 (1 0)
\f -> \x -> f (f x)     λ. λ. 1 (1 0)

f가 나타나는 두 곳 모두 인덱스가 1입니다. 적용은 바인더를 추가하지 않으므로, (f x) 안으로 들어가도 어느 인덱스도 바뀌지 않습니다. 매개변수 이름을 g와 seed로 바꾸어도 인덱스가 매겨진 트리는 정확히 똑같습니다. 알파 동치가 평범한 구조적 동등성이 된 것입니다 (Pierce 2002). 이 점은 우리의 프린터 테스트에서 유용합니다. 파싱–출력–파싱 왕복은 이름이 바뀌더라도 바인딩을 보존해야 합니다.

열린 항에는 여전히 자유 변수를 표현할 방법이 필요합니다. 우리의 Term 타입은 자유 변수를 Bound(index)와 구별하여 Free(name)으로 보관합니다. 따라서 \x -> x y는 Lam(App(Bound(0), Free("y")))가 됩니다. 재귀적이지 않은 let은 본문에서만 바인더를 도입합니다. let x = x in x에서 오른쪽의 x는 자유 변수이고 마지막 x는 바인딩된 변수입니다:

Let(Free("x"), Bound(0))

인덱스를 쓰면 이름 바꾸기는 간단해지지만, 항을 바인더 너머로 옮길 때는 여전히 주의가 필요합니다. \a -> (\x -> \b -> x) a 안에서 인자 a는 원래 위치에서 인덱스 0을 가집니다. 축약 후의 결과는 \a -> \b -> a이며, 여기서는 같은 출현이 인덱스 1이 되어야 합니다. 예전의 0을 그대로 복사하면 실수로 b를 가리키게 됩니다. 인덱스가 매겨진 항에 직접 치환하는 평가기에는 시프팅(shifting)이 필요합니다: 항이 스코프 안으로 들어가거나 밖으로 나올 때 바깥 바인더를 가리키는 참조는 조정하고, 항 내부에서 바인딩된 참조는 그대로 두는 것입니다.

여기서는 인덱스를 변환과 비교에 사용합니다. 정규 순서 축약기는 여전히 이름이 있는 트리에서 치환하고, 엄격한 평가기는 클로저를 사용합니다. 그렇게 하면 각 예제가 핵심에 집중할 수 있습니다. 이후의 Fun 패스들은 덤프를 읽기 쉽게 유지하기 위해 고유한 이름을 사용합니다. 이름 없는 항은 바인딩을 이해하는 데 유용한 도구이지, 모든 컴파일러 IR이 반드시 따라야 하는 요구 사항은 아닙니다.

S, K, I: 바인더 없는 함수

콤비네이터(combinator)는 자유 변수가 없는 람다 항입니다. 콤비네이터는 주변으로부터 어떤 바인딩도 필요로 하지 않습니다. 세 개의 작은 콤비네이터만으로도 순수한 타입 없는 람다 대수의 함수들을 표현하기에 충분합니다:

I = \x -> x
K = \x -> \y -> x
S = \f -> \g -> \x -> f x (g x)

이 대문자들은 수학적 이름입니다. 실행 가능한 테스트에서는 소문자 s, k, i를 평범한 지역 바인딩으로 사용합니다. 적용은 왼쪽으로 결합하므로 S f g a는 ((S f) g) a를 뜻합니다. 각 축약 규칙은 표시된 인자를 모두 받아야 발동할 수 있습니다.

I와 K는 쉽게 떠올릴 수 있습니다. S는 적용이 공유된 입력에 어떻게 의존할 수 있는지를 설명합니다. f, g, a가 주어지면 f a와 g a를 계산한 다음, 첫 번째 결과를 두 번째 결과에 적용합니다. f a (g a)의 괄호는 중요합니다.

두 함수 모두에 K를 골라 봅시다:

S K K a
→ K a (K a)        apply the S rule
→ a                apply the K rule

따라서 S K K는 I처럼 동작합니다. 아름답고 작은 결과입니다. 우리는 언뜻 보기에 항등 함수와는 전혀 닮지 않은 두 연산으로 항등 함수를 만들 수 있습니다. S와 K만으로 충분하지만, I를 남겨 두면 식을 읽기가 더 쉬워집니다. 이 장의 s k k (i 42) 예제를 실행해 보고 축약 과정을 따라가 보십시오.

왜 하필 이 연산들이 람다를 제거할 수 있을까요? 본문 t에 대해, x를 받아 t를 만들어 내는 콤비네이터 식을 [x]t로 씁시다. 안쪽 람다들이 변환되고 나면 세 가지 경우가 있습니다:

[x]x       = I
[x]t       = K t                  when x is not free in t
[x](p q)   = S ([x]p) ([x]q)       otherwise

본문이 매개변수 자체라면 그것을 반환합니다. 본문이 매개변수를 무시한다면 K를 사용해 매개변수를 버립니다. 그렇지 않으면 본문은 적용이며, S가 변환된 두 자식 모두에 매개변수를 전달합니다. 이 절차를 괄호 추상화(bracket abstraction)라고 합니다. 가장 안쪽 람다부터 바깥쪽으로 작업합니다. 닫힌 순수 람다 항을 변환하면 결국 콤비네이터와 적용만 남습니다.

예를 들어 f를 자유 이름으로 취급하여 \x -> f x에서 바인더를 제거해 봅시다:

[x](f x)
= S ([x]f) ([x]x)
= S (K f) I

결과에 인자를 하나 주어 확인해 봅시다:

S (K f) I a
→ (K f a) (I a)
→ f (I a)
→ f a

x의 출현이 사라졌습니다. 자유 변수 f는 당연히 그대로 남아 있습니다. 드 브루인 인덱스는 바인더를 유지하고 그 참조를 거리로 인코딩합니다. 브래킷 추상화는 바인더를 제거하고 바인더가 하던 일을 적용으로 표현합니다. 이로써 우리는 같은 계산의 두 표현 사이에서 일어나는 컴파일의 작은 예를 얻습니다.

함정이 하나 있는데, 그것은 우리가 처음에 다루었던 바로 그 평가 순서 문제입니다. 정규 순서는 omega가 영원히 실행되더라도 K 42 omega를 42로 축약합니다. 우리의 엄격한 평가기는 K의 본문에 들어가기 전에 omega를 계산하려 하므로 거기까지 도달하지 못합니다. 이 콤비네이터 등식들은 순수 대수에서의 재작성을 기술합니다. 이 등식들이 엄격한 컴파일러가 임의의 계산을 버려도 된다고 허용하는 것은 아닙니다. 우리는 바인딩과 축약을 이해하는 데 SKI를 사용하고, Fun의 백엔드는 클로저를 사용할 것입니다. 클로저를 쓰면 단순한 콤비네이터 변환이 만들어 낼 수 있는 거대한 적용 트리도 피할 수 있습니다.

구현

ast.rs는 람다, 적용, 불리언, 조건식을 추가합니다. 이 모듈의 프린터는 우선순위 문맥을 사용하며, 트리를 보존하는 데 필요한 곳에만 괄호를 추가합니다. 파서는 적용에 산술보다 높은 우선순위를 부여합니다:

Application: Expr = {
    <a:Application> <b:Atom> => {
        let (start, end) = (a.span.start, b.span.end);
        Expr::new(Kind::App(Box::new(a), Box::new(b)), start, end)
    },
    Atom,
};

names.rs는 자유 변수를 계산하고 포획을 피하는 치환을 수행합니다. 아래 헬퍼는 바인더 하나를 처리합니다. 재귀적인 치환은 각 항의 형태를 처리합니다. 새 이름은 원래 본문과 대체 항에 있는 자유 이름과 속박 이름을 모두 피하므로, 새 이름이 안쪽 람다와 충돌하지 않습니다.

#![allow(unused)]
fn main() {
fn binder(
    name: &str,
    body: &Expr,
    target: &str,
    value: &Expr,
) -> (String, Expr) {
    if name == target {
        return (name.to_owned(), body.clone());
    }
    let mut name = name.to_owned();
    let mut body = body.clone();
    if free(value).contains(&name) && free(&body).contains(target) {
        let mut used = BTreeSet::from([target.to_owned()]);
        all_names(&body, &mut used);
        all_names(value, &mut used);
        let mut fresh = format!("{name}'");
        while used.contains(&fresh) {
            fresh.push('\'');
        }
        let variable = Expr::new(Kind::Var(fresh.clone()), 0, 0);
        body = substitute(&body, &name, &variable);
        name = fresh;
    }
    (name, substitute(&body, target, value))
}
}

같은 모듈은 이름 붙은 항을 인덱스로 변환합니다. 스택은 가장 바깥 스코프부터 가장 안쪽 스코프까지의 이름을 담습니다. let의 우변은 그 바인더가 푸시되기 전에 변환됩니다. 그 바인더는 본문에만 속하기 때문입니다.

#![allow(unused)]
fn main() {
/// Bound names are distances to binders; free names remain explicit.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Bound(usize),
    Free(String),
    Int(i64),
    Bool(bool),
    Lam(Box<Term>),
    App(Box<Term>, Box<Term>),
    Let(Box<Term>, Box<Term>),
    If(Box<Term>, Box<Term>, Box<Term>),
    Neg(Box<Term>),
    Binary(Op, Box<Term>, Box<Term>),
    Error,
}

/// Convert without substitution; alpha-equivalent expressions have equal terms.
pub fn debruijn(expr: &Expr, bound: &mut Vec<String>) -> Term {
    let mut go = |e: &Expr| Box::new(debruijn(e, bound));
    match &expr.kind {
        Kind::Var(n) => bound
            .iter()
            .rev()
            .position(|x| x == n)
            .map_or_else(|| Term::Free(n.clone()), Term::Bound),
        Kind::Lam(n, a) => {
            bound.push(n.clone());
            let body = debruijn(a, bound);
            bound.pop();
            Term::Lam(Box::new(body))
        }
        Kind::Let(n, a, b) => {
            let value = go(a);
            bound.push(n.clone());
            let body = debruijn(b, bound);
            bound.pop();
            Term::Let(value, Box::new(body))
        }
        Kind::App(a, b) => Term::App(go(a), go(b)),
        Kind::Binary(op, a, b) => Term::Binary(*op, go(a), go(b)),
        Kind::If(c, a, b) => Term::If(go(c), go(a), go(b)),
        Kind::Neg(a) => Term::Neg(go(a)),
        Kind::Int(n) => Term::Int(*n),
        Kind::Bool(b) => Term::Bool(*b),
        Kind::Error => Term::Error,
    }
}
}

normal.rs는 작은 한 단계를 구현합니다. 적용의 경우, 인자를 먼저 평가하지 않고 치환합니다. 함수가 람다가 아니면 먼저 그 함수를 한 단계 진행하고, 그보다 앞선 redex가 없을 때 인자를 진행합니다.

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    if let Kind::Lam(name, body) = &function.kind {
        return Ok(Some(substitute(body, name, argument)));
    }
    if let Some(next) = step(function)? {
        Kind::App(Box::new(next), argument.clone())
    } else if let Some(next) = step(argument)? {
        Kind::App(function.clone(), Box::new(next))
    } else {
        return Ok(None);
    }
}
}

reduce는 한도와 각 항을 표시하는 콜백을 가지고 step을 반복해서 호출합니다. 이 축약기는 축약할 수 없는 적용을 포함한 열린 항도 살펴볼 수 있습니다. 이것은 Fun의 최종 실행 엔진이 아니라 항 재작성을 보여 주는 시연입니다.

반면 eval.rs는 람다의 환경을 클로저에 저장합니다:

#![allow(unused)]
fn main() {
/// Lexical bindings retained by a closure.
pub type Env = Vec<(String, Value)>;

#[derive(Clone, Debug)]
/// Runtime integers, booleans, and code paired with its lexical environment.
pub enum Value {
    Int(i64),
    Bool(bool),
    Closure(String, Rc<Expr>, Rc<Env>),
}
}

값에 의한 호출의 적용 경우는 그 순서를 명시적으로 드러냅니다:

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    let function = evaluate(function, env, fuel)?;
    let argument = evaluate(argument, env, fuel)?;
    if let Value::Closure(name, body, captured) = function {
        let mut local = (*captured).clone();
        local.push((name, argument));
        evaluate(&body, &local, fuel)
    } else {
        Err("expected a function".into())
    }
}
}

본문은 캡처된 환경에 인자를 추가한 환경에서 실행됩니다. 재귀 방문마다 연료가 소모됩니다. CLI는 이러한 트리 순회기를 위해 더 큰 호스트 스택을 사용합니다. 5장에서는 호스트 재귀를 명시적 기계로 대체합니다. 연료도, 더 큰 스택도 그 변환을 대신할 수는 없습니다.

실행해 보기

$ cd crates/ch03_lambda
$ cargo run -q -- run tests/programs/church.fun
2
$ cargo run -q -- dump --pass=debruijn tests/programs/identity.fun
App(Lam(Bound(0)), Int(42))
$ cargo run -q -- repl
Lambda: :quit, :parse EXPR, :trace EXPR.
lambda> :trace (\x -> x) 42
(\x -> x) 42
42
lambda> :quit

run --engine=normal로 정규 순서를 선택하십시오. 끝나지 않을 수도 있는 항으로 실험할 때는 --fuel=N을 사용하십시오. 두 엔진은 서로 다른 연산을 세므로, 같은 연료 한도라도 두 엔진이 반드시 같은 지점에서 멈추는 것은 아닙니다. 실패하는 인자를 무시하는 함수를 시도해 보면 두 엔진의 답이 왜 다를 수 있는지 알 수 있습니다.

연습 문제

1. 쉬움. \x -> \y -> y x를 손으로 드 브루인 인덱스로 변환하십시오.
2. 보통. \y -> \y' -> x y에서 x를 자유 이름 y로 치환하십시오. 결과의 자유 변수를 확인하십시오.
3. 보통. \x -> x x를 괄호 추상화(bracket abstraction)로 번역한 다음, 그 결과를 I에 적용하십시오. 그 축약 과정을 람다 항의 축약과 비교하십시오.
4. 보통. K I a b를 추적하고 어느 인자가 버려지는지 설명하십시오.
5. 어려움. 값에 의한 호출에 적합한 고정점 콤비네이터를 구성하고, 그 트레이스를 Y의 트레이스와 비교하십시오.

더 읽을거리

Pierce는 치환, 축약, 이름 없는 항을 다룹니다 (Pierce 2002). Felleisen과 Friedman은 우리가 5장에서 다시 다룰 추상 기계 설정을 소개합니다 (Felleisen and Friedman 1986).