はじめに

この記事は、42Tokyo Advent Calendar 2024の16日目の記事です。

この記事では、型無しラムダ計算における基本的な概念（α変換、β簡約、η簡約）および、それらをRustで実装する方法を説明します。

実装は Writing a lambda calculus interpreter in Rust という記事を大いに参考にしています。Rustについての説明も丁寧にされているので、英語の読める方はこちらを読むことをおすすめします。

目次

ラムダ計算とは
β簡約について
α変換について
η簡約について
実装
まとめ
参考

ラムダ計算とは

ラムダ計算とは関数型言語の基盤となっている計算モデルで、数値や演算の具体的な表記ではなく、「関数そのもの」を使って計算を表現するという性質を持ちます。
具体的に、ラムダ計算は以下のような生成規則から成ります。

M ::= x         (1)
    | λx.M      (2)
    | M_1 M_2   (3)

(2)の規則をラムダ抽象、(3)の規則を関数適用と呼びます。
これだけの簡単な生成規則でありながら、ラムダ計算はチューリング機械と同等の表現力を持つ (= チューリング完全) ことが知られています。

ここで、ラムダ計算での演算の結合の強さについて、以下の性質を約束とします:

- 関数適用は左結合
例: x y z なるラムダ式は、x (y z)ではなく (x y) z と評価する。
- ラムダ抽象の範囲はなるべく広く取る
例: λx. x y は、(λx. x) y ではなく、(λx. x y) と評価する。

これらに従って意味が変化しない限り、優先順位づけのための()は外すことができます。

β簡約について

β簡約は、ラムダ式の中で引数が関数に適用される際、引数をその関数内の変数に代入して式を簡略化する操作です。

形式的には次のように表されます:

(λx. M)N -> [N/x]M

ここで、[N/x]Mは「M中のxをNに置き換えたもの」に対応します。

例を示せば、

(λx. x + 2)1
-> [1/x](λx. x + 2)
-> 1 + 2

という操作です。

この簡約では以下を約束とします:

- 代入はラムダ抽象のスコープに応じて行う:
代入は、ラムダ式の中で変数がどの範囲で使われているかを考慮して行う。
ラムダ式の外部で定義された変数と内部の変数が同じ名前であっても、外部の変数には影響を与えない。
- 名前が衝突する場合にはα変換を施す

一つ目の規則に関して、(λx. (λx. x) x) 1というラムダ式を考えてみましょう。

[1/x](λx. (λx. x) x)なる簡約を行う際、機械的に式中のxを1に置き換えると、λ1.1 1となりますが、これは意味を考えると明らかに不適です。
同様にして、λ1.x 1やλx. 1 1が意味的に誤りであることも理解されるかと思います。

こうした不当な簡約を禁止するための規則が一つ目の規則です (この場合では外のラムダ抽象の中で定義されたxに対応するxだけを書き換える、 λx.x 1が正しいです) 。

二つ目の規則に関しては次章で説明します。

一般にβ簡約できる部分が複数あるラムダ式に対しては評価の経路が複数通りあり得ますが、すべての簡約は合流して同じラムダ式に到達できることが知られています (チャーチロッサーの定理) 。

α変換について

(λx. λy. x) yというラムダ式を考えてみましょう。

(λx. λy. x)というラムダ式は、引数を2つ取り、1つ目の引数を返す、という関数になっています。
今考えている(λx. λy. x) yでは一つ目の引数だけ与えているので、これを部分適用すれば、(λ y. y)という恒等関数に対応するラムダ式が得られました。
一見正しそうに見えますが、これは誤りです。実際、元のラムダ式は引数を2つ取り、1つ目の引数を返すはずでしたが、2つ目の引数を返す動作をするように意味が書き変わってしまいました。

この問題は、ラムダ抽象の中で引数として定義されたyと、引数として与えた定数のyが同じ名前を持つことに起因しています。
実際、(λx. λy. x) yの末尾のyをzと書きかえてみると、

(λx. λy. x) z -> λy. z // これはyの値によらず第一引数であるzを返す

のように期待する動作が得られました。

ラムダ計算では、前述した「ラムダ抽象の中で引数として定義された」変数のことを束縛変数、そうでない変数のことを自由変数といいます。
そして、この束縛変数と自由変数が衝突しない様に束縛変数に別の命名をする操作のことをα-変換と呼びます。

実装する上では、自由変数の一覧を事前に記録しておき、同名の束縛変数があれば名前を付け替える、という操作が必要になります。
詳しくは実装のセクションで見ることにします。

η簡約について

λx. M xというラムダ式を考えます。

Mにxが自由に出現しない時、λx. M xはMと同じ関数になります。

実際、引数Nを渡すと、

(λx. M x)N
-> M N

となり同じ戻り値を与えることがわかります。

以上からλx. M xはMに、逆にMはλx. M xへと変換することができ、
前者をη簡約、後者をη展開と呼びます。

実装

では、以上のα変換・β簡約を実際に実装してみましょう。
具体的には、以下のステップで実装します:

入力をトークンに分割
トークンから構文木を構成
得られた構文木を変換・簡約する

1,2のステップはラムダ計算に限らず、プログラミング言語を解析する上で一般的に用いられる手続きです。
構文解析について詳しく知りたい方は、こちらの記事が参考になるかと思います。

全体の実装を見たい方は以下のレポジトリを参照してください。

入力をトークンに分割

ここでは、以下のトークンに分割します。

lambda: λ | \
term: 変数名、英小文字および英大文字からなるものとする
lparen: (
rparen: )

Rustはマルチバイト文字をサポートしているので、"λ"もストレスなく扱えるのですが、入力が厄介なので""も"λ"と同等の意味を持つ記号として考えます。

トークンを管理する上で扱いやすい型を用意します。今回はエラーメッセージにエラーの発生位置を載せたいので、トークンの入力列内での位置を保持する様にしましょう。
具体的には、以下のように定義します。

models.rs

pub enum Token {
    LParen(usize),
    RParen(usize),
    Lambda(usize),
    Term(usize, String),
}

以下が、トークン化のコードになります。

tokenize.rs

use crate::models::Token;
use regex::Regex;

pub fn tokenize(input: &str) -> Vec<Token> {
    let mut tokens = Vec::new();
    let token_pattern =
        Regex::new(r"(?P<lambda>[λ\\])|(?P<lparen>\()|(?P<rparen>\))|(?P<term>[A-Za-z]+)").unwrap();

    for cap in token_pattern.captures_iter(input) {
        if let Some(_) = cap.name("lambda") {
            tokens.push(Token::Lambda(cap.get(0).unwrap().start()));
        } else if let Some(_) = cap.name("lparen") {
            tokens.push(Token::LParen(cap.get(0).unwrap().start()));
        } else if let Some(_) = cap.name("rparen") {
            tokens.push(Token::RParen(cap.get(0).unwrap().start()));
        } else if let Some(term) = cap.name("term") {
            tokens.push(Token::Term(
                cap.get(0).unwrap().start(),
                term.as_str().to_string(),
            ));
        }
    }

    tokens
}

トークン化に際して、regexクレートを使用しました。
正規表現は直感的かつ簡潔にパターンを表現でき、トークン定義を変更したい場合も容易に対応できます。

トークンから構文木を構成

まず、ラムダ計算の構文を定義しましょう。ここでは、以下のように定義します。

expr ::= term | abstraction | application | "(" expr ")"
term ::= [A-Za-z]+
lambda ::= "\" | "λ"
abstraction ::= lambda term "." expr
application ::= expr expr

このような記法はBNFと呼ばれる記法で、プログラミング言語の文法を定義するための標準的な記法です。上で説明した様にラムダ計算では、定義、ラムダ抽象、関数適用が基本的な構成単位となります。

この生成規則をもとに、抽象構文木を作ります。詳しくは説明しませんが、これもBNFによる再帰的な構文定義と相性がよく、ごく一般的に用いられます。
詳しく勉強したい方は、こちらをご参照ください。

以下に実装を示します:

models.rs

pub enum Expr {
    Var(String),
    Abs(String, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
}

pub enum ParseError {
    UnclosedParen(usize),
    UnopenedParen(usize),
    MissingLambdaVar(usize),
    MissingLambdaBody(usize),
    EmptyExprList(usize),
}

parse.rs

use crate::models::{Expr, ParseError, Token};

fn find_matching_paren(tokens: &[Token], start: usize) -> Option<usize> {
    let mut depth = 0;
    for j in start + 1..tokens.len() {
        match tokens[j] {
            Token::LParen(_) => depth += 1,
            Token::RParen(_) => {
                if depth == 0 {
                    return Some(j);
                }
                depth -= 1;
            }
            _ => {}
        }
    }
    None
}

fn combine_exprs(exprs: Vec<Expr>) -> Result<Expr, ParseError> {
    exprs
        .into_iter()
        .reduce(|acc, item| Expr::App(Box::new(acc), Box::new(item)))
        .ok_or_else(|| ParseError::EmptyExprList(0))
}

pub fn parse(tokens: &[Token]) -> Result<Expr, ParseError> {
    let mut i = 0;
    let mut exprs = Vec::new();

    while i < tokens.len() {
        match &tokens[i] {
            Token::LParen(paren_index) => match find_matching_paren(tokens, i) {
                Some(j) => {
                    let inside_expr = parse(&tokens[i + 1..j])?;
                    exprs.push(inside_expr);
                    i = j;
                }
                None => return Err(ParseError::UnclosedParen(*paren_index)),
            },
            Token::RParen(paren_index) => {
                return Err(ParseError::UnopenedParen(*paren_index));
            }
            Token::Lambda(lambda_index) => {
                if let Some(Token::Term(_, var)) = tokens.get(i + 1) {
                    if tokens.len() > i + 2 {
                        let body = parse(&tokens[i + 2..])?;
                        exprs.push(Expr::Abs(var.clone(), Box::new(body)));
                        break;
                    } else {
                        return Err(ParseError::MissingLambdaBody(*lambda_index));
                    }
                } else {
                    return Err(ParseError::MissingLambdaVar(*lambda_index));
                }
            }
            Token::Term(_, var) => {
                exprs.push(Expr::Var(var.clone()));
            }
        }
        i += 1;
    }

    combine_exprs(exprs)
}

各パターンマッチについて解説していきます。

Token::LParen

まず、(を見つけたら、対応する)を探し、インデックスを取得します (find_matching_paren)。
depth変数にいま何重のネスト状態なのかを保持しておき、それが0となった時に見つかった)が対応する)ということになります。
そして、対応する)の位置までの式を先に解析します。こうすることで()による計算順序付けが可能になります。
なお対応する)がない場合は、式として不正な形をしているので、エラーとして処理しています。

Token::RParen

ここでの処理は簡単です。Token::LParenを見つけた時点で対応する)の次の位置までインデックスが進んでいるはずなので、
パターンマッチの状態でこのトークンがヒットする場合、対応しない)ということになります。
したがって、この場合は無条件にエラーとして処理してしまいましょう。

Token::Lambda

λないしは\はラムダ抽象の開始と解釈できます。そこでこの場合のゴールはExpr::Absを作ることになります。
このために、まずはλ抽象の束縛変数 (これは次のトークンのはずです) を記録しておき、その後ろを関数本体として再帰的に解析します。
なお、λはあるが束縛変数がない、あるいは関数本体が存在しない場合には、エラーとして処理します。

Token::Term

これは(1)の規則である変数に他なりません。したがって、Expr::Varノードとして素直に処理することができます。

ここまでのプログラム中では陽に関数適用の規則が表れていません。これは関数適用を再帰的に解析すれば(1)および(2)の規則に帰着されることによります。
そこで、最後に解析した式をつなげて一つのラムダ式とします (combine_exprs)。
この関数はリスト内の各要素を左から結合し、最終的にひとつのツリーを作成します。
リストが空の場合は結合できる要素がないため、ラムダ式としては不正な形といえます。

得られた構文木を変換・簡約する

ようやくラムダ計算に関してのパートです。ここでは先にコードを示し、解説を加える形にします。

reduce.rs

use crate::models::Expr;
use std::cell::RefCell;
use std::collections::HashSet;

// expr中の自由変数の一覧を取得する
fn get_free_vars(expr: &Expr) -> HashSet<String> {
    fn collect_free_vars(
        expr: &Expr,
        free_vars: &mut HashSet<String>,
        bound_vars: &mut HashSet<String>,
    ) {
        match expr {
            Expr::Var(var_name) => {
                if !bound_vars.contains(var_name) {
                    free_vars.insert(var_name.clone());
                }
            }
            Expr::Abs(param, body) => {
                let is_new_binding = bound_vars.insert(param.clone());
                collect_free_vars(body, free_vars, bound_vars);
                if is_new_binding {
                    bound_vars.remove(param);
                }
            }
            Expr::App(left, right) => {
                collect_free_vars(left, free_vars, bound_vars);
                collect_free_vars(right, free_vars, bound_vars);
            }
        }
    }

    let mut free_vars = HashSet::new();
    let mut bound_vars = HashSet::new();
    collect_free_vars(expr, &mut free_vars, &mut bound_vars);
    free_vars
}

// static変数で、解消すべき変数名のカウンタを持っておく
// もし自由変数と同名の束縛変数があった場合、衝突を避けるためにsuffixをつける
thread_local!(static DISAMBIGUATE_CTR: RefCell<u64> = RefCell::new(0));
fn disambiguate(w: &str) -> String {
    DISAMBIGUATE_CTR.with(|ctr| {
        let mut ctr = ctr.borrow_mut();
        *ctr += 1;
        format!("{}_{}", w, ctr)
    })
}

fn alpha_convert(var: String, body: Expr) -> (String, Expr) {
    let new_vars = disambiguate(&var);
    let new_body = substitute(body, &var, &Expr::Var(new_vars.clone()));
    (new_vars, new_body)
}

// expr中の変数varをreplacementで置き換える
fn substitute(expr: Expr, var: &str, replacement: &Expr) -> Expr {
    let free_vars = get_free_vars(replacement);
    match expr {
        Expr::Var(var_name) => {
            if var_name == var {
                replacement.clone()
            } else {
                Expr::Var(var_name)
            }
        }
        Expr::Abs(param, body) => {
            if param == var {
                Expr::Abs(param, body)
            } else if free_vars.contains(&param) {
                let (new_var, new_body) = alpha_convert(param, *body);
                Expr::Abs(new_var, Box::new(substitute(new_body, var, replacement)))
            } else {
                Expr::Abs(param, Box::new(substitute(*body, var, replacement)))
            }
        }
        Expr::App(left, right) => Expr::App(
            Box::new(substitute(*left, var, replacement)),
            Box::new(substitute(*right, var, replacement)),
        ),
    }
}

fn beta_reduce(abs: Expr, replacement: Expr) -> Expr {
    if let Expr::Abs(param, body) = abs {
        substitute(*body, &param, &replacement)
    } else {
        panic!("can't apply to non-abstraction");
    }
}

pub fn reduce_expression(expr: Expr) -> Expr {
    match expr {
        Expr::App(left, right) => {
            let reduced_left = reduce_expression(*left);
            let reduced_right = reduce_expression(*right);

            if let Expr::Abs(var, body) = reduced_left {
                return reduce_expression(beta_reduce(Expr::Abs(var, body), reduced_right));
            } else {
                return Expr::App(Box::new(reduced_left), Box::new(reduced_right));
            }
        }
        _ => expr,
    }
}

reduce_expression関数が外から呼び出される関数です。まず関数適用を検出し、その中でラムダ抽象をβ簡約します。その後、結果が再度簡約可能であれば、再帰的に簡約を進めます。
substitute関数では以下のルールにしたがって再帰的に変数を置き換えています:

現在の変数が置き換え対象の変数と一致する場合、渡された式で置き換える。
そうでない場合、変数をそのまま保持。
ラムダ抽象内では、自由変数と束縛変数が衝突しないように α変換を適用。

α変換およびβ簡約については、上の説明と素直に対応する実装になっているかと思います。

おまけ

以下に示す様な出力用のmain関数を用意します。詳細はこちらを参照してください。

main.rs

use crate::models::{Expr, ParseError};
use std::fmt::{Display, Formatter, Result as FmtResult};
use std::io;

impl Display for Expr {
    fn fmt(&self, f: &mut Formatter<'_>) -> FmtResult {
        match self {
            Expr::Var(s) => write!(f, "{}", s),
            Expr::Abs(s, e) => write!(f, "λ{}.{}", s, e),
            Expr::App(u, v) => {
                match u.as_ref() {
                    Expr::Abs(_, _) => write!(f, "({}) ", u),
                    _ => write!(f, "{} ", u),
                }?;
                match v.as_ref() {
                    Expr::Abs(_, _) => write!(f, "({})", v),
                    Expr::App(_, _) => write!(f, "({})", v),
                    _ => write!(f, "{}", v),
                }
            }
        }
    }
}

fn main() {
    let mut buf = String::new();
    if let Err(e) = io::stdin().read_line(&mut buf) {
        eprintln!("Error reading input: {}", e);
        return;
    }

    let tokens = tokenize::tokenize(&buf);

    let expr = match parse::parse(&tokens) {
        Ok(e) => e,
        Err(e) => {
            match e {
                ParseError::UnclosedParen(index) => {
                    eprintln!("Error: Unclosed parenthesis at index {}", index)
                }
                ParseError::UnopenedParen(index) => {
                    eprintln!("Error: Unopened parenthesis at index {}", index)
                }
                ParseError::MissingLambdaVar(index) => {
                    eprintln!("Error: Missing lambda variable at index {}", index)
                }
                ParseError::MissingLambdaBody(index) => {
                    eprintln!("Error: Missing lambda body at index {}", index)
                }
                ParseError::EmptyExprList(index) => {
                    eprintln!("Error: Empty expression list at index {}", index)
                }
            }
            return;
        }
    };

    let result = reduce::reduce_expression(expr);
    println!("-> {}", result);
}

それでは、ここまでで作った計算機を用いて、0の0乗を計算してみましょう。
ラムダ計算は自然数や冪乗に対応する表現を持ちます (チューリング機械と同等の表現を持つことからも明らかですね) 。
自然数に対応するラムダ式は以下の様に書けます:

0 := λf λx. x
1 := λf λx. f x
2 := λf λx. f (f x)
3 := λf λx. f (f (f x))
...

そして、mのn乗に対応するラムダ式はλm. λn. n mとなります (詳しく知りたい方はwikipediaを参照していただければと思います)。

実際に0の0乗を実行してみると、、、

❯ cargo run
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.01s
     Running `target/debug/lambda-rs`
(λm. λn. n m) (λf. λx. x) (λf. λx. x)
-> λx.x

恒等関数に対応するラムダ式が得られました。
解釈のため、束縛変数のxをfとして書き換え、λf. fを考えます。
そしてこのfを変数xについてη展開すれば、λf. λx. f xが得られます。
これは1に対応するラムダ式に他なりません。
実際、wikipediaの0の0乗についてのページをみるとMLやHaskellといった関数型言語では0の0乗は1と定義されていることがわかります。

まとめ

この記事では型無しラムダ計算の基本概念（α変換、β簡約、η簡約）について説明し、それらをRustで実装する方法を示しました。

浅学の私が知る限りでも、上で紹介した話のほかにラムダ計算に関する面白い話はいくつもあります。ぜひこの記事を出発点として、ラムダ計算に入門していただければと思います。

明日は@ryaoi42さんによる記事です。わくわく。

参考