TAPLのML実装をRustでやってみるシリーズ「7章 ラムダ計算のML実装」

Cargo.toml

[package]

name = "ch7"
version = "0.0.1"
authors = ["UEHARA Junji <[email protected]>"]

main.rs

#![allow(dead_code)]
#![allow(unused_imports)]
#![feature(box_patterns)]

mod named;
mod nameless;

use named::{abst, apply, var};

fn main() {
    // 演習6.2.5.(2)
    println!("{:?}",
             apply(abst("a", 
                         apply(abst("b",
                                    apply(var("b"), abst("x", var("b")))),
                               apply(var("a"), abst("z", var("a")))
                               )),
                    abst("w", var("w"))
                    ).remove_names().eval());
}

named.rs

#![allow(dead_code)]
#![allow(unused_variables)]

use std::fmt::Debug;
use std::fmt::Formatter;
use std::fmt::Error;

use nameless::{Term, Context, Binding};

#[derive(Clone,PartialEq)]
pub enum NamedLambdaTerm {
    Var(String),
    Abst(String, Box<NamedLambdaTerm>),
    Apply(Box<NamedLambdaTerm>,
          Box<NamedLambdaTerm>)
}

use named::NamedLambdaTerm::*;

impl Debug for NamedLambdaTerm {
    fn fmt(&self, fmt:&mut Formatter) -> Result<(), Error> {
        match self {
            &Var(ref s) =>
                fmt.write_str(&format!("Var({:?})", s)),
            &Abst(ref n, ref b) =>
                fmt.write_str(&format!("Abst({:?}, {:?})", n, b)),
            &Apply(ref f, ref a) =>
                fmt.write_str(&format!("Apply({:?}, {:?})", f, a)),
        }
    }
}

impl NamedLambdaTerm {
    fn remove_names_helper(&self, gm:&Context, nest:usize) -> Term {
        match self {
            &Var(ref s) => {
                match gm.iter().rposition(|x| x.0.eq(s)) {
                    None => Term::Var(999, nest),
                    Some(n) => Term::Var((gm.len() - n - 1) as isize, nest)
                }
            },
            &Abst(ref n, ref b) => {
                let mut gm_copy = gm.clone();
                gm_copy.push((n.clone(), Binding::NameBind));
                Term::Abst(n.clone(), Box::new(b.remove_names_helper(&gm_copy, nest+1)))
            },
            &Apply(ref f, ref a) => {
                let gm_copy = gm.clone();
                Term::Apply(Box::new(f.remove_names_helper(gm, nest)), Box::new(a.remove_names_helper(&gm_copy, nest)))
            }
        }
    }
    pub fn remove_names(&self) -> Term {
        self.remove_names_helper(&vec![], 0)
    }
}

pub fn var(name:&str) -> NamedLambdaTerm {
    Var(name.to_string())
}

pub fn abst(name:&str, x:NamedLambdaTerm) -> NamedLambdaTerm {
    Abst(name.to_string(), Box::new(x))
}

pub fn apply(f:NamedLambdaTerm, a:NamedLambdaTerm) -> NamedLambdaTerm {
    Apply(Box::new(f),Box::new(a))
}

#[test]
fn test() {
    assert_eq!(format!("{:?}", var("a").remove_names()), "fv999");
    assert_eq!(format!("{:?}", abst("a", var("a")).remove_names()), "(lambda a. a)");
    assert_eq!(format!("{:?}", abst("a", abst("b", apply(var("a"), var("b")))).remove_names()),
               "(lambda a. (lambda b. (a b)))");
}

nameless.rs

// http://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/
#![allow(dead_code)]
#![allow(unused_variables)]
#![allow(unused_imports)]

use std::fmt::Debug;
use std::fmt::Formatter;
use std::fmt::Error;

#[derive(Clone,PartialEq)]
pub enum Term {
    // Single Varialbe
    Var(isize, // de Bruijn Index.
        usize), // length of Context where this variable appealed.
    // Abstraction
    Abst(String, // lambda variable name
         Box<Term>), // lambda body
    // Application
    Apply(Box<Term>, // function
          Box<Term>) // argument
}

#[derive(Debug,Clone)]
pub enum Binding {
    NameBind
}

pub type Context = Vec<(String, Binding)>;

fn index2name(ctx: &Context, idx: isize) -> String {
    if idx > ctx.len() as isize-1 {
        return format!("fv{}", idx)
    }
    ctx[(ctx.len() as isize-idx-1) as usize].0.to_string()
}

use nameless::Term::*;

pub fn add_name(ctx:&Context, name:&String) -> Context {
    let mut new_ctx = ctx.clone();
    new_ctx.push((name.clone(), Binding::NameBind));
    new_ctx
}

fn pick_fresh_name(ctx:&Context, x:&String) -> (Context, String) {
    if ctx.iter().any(|&(ref var_name,_)|{*var_name==*x}) {
        //名前xがctxに存在(重複)していたら、新規名称に変更して再トライ
        pick_fresh_name(ctx, &format!("{}'", x))
    }
    else { // 重複しない名前を得たら
        // ctxにその名前を登録して、(ctx,その名前)を返す。
        (add_name(ctx, x), x.clone())
    }
}

fn print_term(ctx:&Context, t:&Term) -> String {
    match *t {
        Abst(ref var_name, ref t1) => {
            // λ var_name . t1 は、var_nameを環境ctxでユニークであるx_にした上で、
            // x_をctxに登録しそのx_を登録したctx(ctx_)の元で、t1を表示する。
            let (ctx_, x_) = pick_fresh_name(ctx, var_name);
            format!("(lambda {}. {})", x_, print_term(&ctx_, &t1))
        },
        Apply(ref t1, ref t2) => {
            format!("({} {})", print_term(ctx, &t1), print_term(ctx, &t2))
        },
        Var(x, n) => {
            if ctx.len() == n {
                format!("{}", index2name(ctx, x))
            } else {
                format!("[bad index, ctx.len={}, n={}]", ctx.len(), n).to_string()
            }
        }
    }
}

impl Debug for Term {
    fn fmt(&self, fmt:&mut Formatter) -> Result<(), Error> {
        fmt.write_str(&format!("{}", print_term(&vec![], self)))
    }
}

fn term_shift(d:isize, t:&Term) -> Term {
    fn term_shift_helper(c:isize, d:isize, t:&Term) -> Term {
        match *t {
            Var(x, n) =>
                if x >= c { Var(x+d, (n as isize + d) as usize) }
                else { Var(x, (n as isize + d) as usize) },
            Abst(ref x, ref t1) =>
                Abst(x.clone(), Box::new(term_shift_helper(c+1, d, &t1))),
            Apply(ref t1, ref t2) =>
                Apply(Box::new(term_shift_helper(c, d, t1)), Box::new(term_shift_helper(c, d, t2)))
        }
    }

    term_shift_helper(0, d, t)
}

fn term_subst(j:isize, s:&Term, t:&Term) -> Term {
    fn term_subst_helper(j:isize, s:&Term, c:isize, t:&Term) -> Term {
        match *t {
            Var(x, n) =>
                if x == j+c { term_shift(c, s) } else { Var(x, n) },
            Abst(ref x, ref t1) =>
                Abst(x.clone(), Box::new(term_subst_helper(j, s, c+1, t1))),
            Apply(ref t1, ref t2) =>
                Apply(Box::new(term_subst_helper(j, s, c, t1)), Box::new(term_subst_helper(j, s, c, t2)))
        }
    }
    term_subst_helper(j, s, 0, t)
}

fn term_subst_top(s:&Term, t:&Term) -> Term {
    // Apply(Abst(x, t12), v2@Abst(_,_))
    //
    //                        -1        1
    // (λ.t12) v2    →    ↑   ([0→↑  (v2)] t12)
    //
    // 「Apply(Abst(x, t12), v2@Abst(_,_))」の評価は、t12が使用して
    // いる変数x(de Bruijn index=0)をv2で置換するということである
    // (β簡約)。しかし、v2も(de Bruijn index 0)を参照している可能
    // 性があるので、単なる置換はできない。そのためには、v2の(de
    // Bruijn index 0)を(de Bruijn index 1)にする必要がある。さらに、
    // v2はもともと(de Bruijn index 1)を使用しているかもしれないの
    // で、0→1、1→2、2→3...というようにv2で使用している変数すべ
    // ての玉つきでの増加が必要。これが内側のシフト操作
    //      1
    // 0→↑  (v2) 
    // の意味である。
    // 上記より、無事v2から(de Bruijn index 0)を消去できたとして、
    // λの中にあったt12を、λ取ってその外側の中で通用する値として
    // 機能させるには、ネストレベルを一個浅くする必要がある。これが
    // 外側の
    //   -1
    // ↑
    // の操作である。これが意味するのは最内周の変数(de Bruijn
    // index 0)の削除であり、de Bruijn index 1以上の変数をそれぞれ
    // 1個インデックスが減るようにずらす。t12の(de Bruijn index 0)
    // をv2で置換した結果には、(de Bruijn index 0)は(置換されている
    // ので)もう存在していないので、これは安全に実行できる。
    term_shift(-1, &term_subst(0, &term_shift(1, s), t))
}

fn is_val(t: &Term) -> bool {
    match *t {
        Abst(_,_) => true,
        _ => false
    }
}

fn eval1(ctx:&Context, t:&Term) -> Option<Term> {
    match t {
        &Apply(box Abst(ref x, box ref t12), ref v2) if is_val(v2) => {
            Some(term_subst_top(v2, &t12))
        },
        // Apply(v1@Abst(_,_), t2)
        // (λ _._) t2
        &Apply(ref v1, ref t2) if is_val(v1) => {
            match eval1(ctx, t2) {
                Some(t2_) => {
                    // (λ _._) t2_
                    Some(Apply(v1.clone(), Box::new(t2_)))
                },
                None => None
            }
        },
        // Apply(t1, t2)
        &Apply(ref t1, ref t2) => {
            match eval1(ctx, &t1) {
                Some(t1_) => Some(Apply(Box::new(t1_), t2.clone())),
                None => None
            }
        },
        _ => None
    }
}

fn eval(ctx:&Context, t:&Term) -> Term {
    match eval1(ctx, &t) {
        Some(x) => x.eval(),
        None => t.clone()
    }
}

impl Term {
    pub fn eval(&self) -> Term {
        eval(&vec![], self)
    }
}

fn abst(s:&str, t:Term) -> Term {
    Abst(s.to_string(), Box::new(t))
}

fn apply(t1:Term, t2:Term) -> Term {
    Apply(Box::new(t1), Box::new(t2))
}

#[test]
fn simple_test() {
    assert_eq!(format!("{:?}", Var(0, 0)), "fv0");
    let a1 = abst("a", Var(0, 1));
    assert_eq!(format!("{:?}", a1), "(lambda a. a)");
    let a2 = apply(a1, Var(0, 0));
    assert_eq!(format!("{:?}", a2), "((lambda a. a) fv0)");
}

#[test]
fn index2name_test() {
    let mut ctx1 = vec![("a".to_string(),Binding::NameBind),
                        ("b".to_string(),Binding::NameBind)];
    assert_eq!(ctx1.len(), 2);
    assert_eq!(index2name(&ctx1, 0), "b");
    assert_eq!(index2name(&ctx1, 1), "a");
    ctx1.push(("c".to_string(), Binding::NameBind));
    assert_eq!(ctx1.len(), 3);
    assert_eq!(index2name(&ctx1, 0), "c");
    assert_eq!(index2name(&ctx1, 1), "b");
    assert_eq!(index2name(&ctx1, 2), "a");
    assert_eq!(index2name(&ctx1, 3), "fv3");
}

#[test]
fn pick_fresh_name_test() {
    let mut ctx1 = vec![("a".to_string(),Binding::NameBind),
                        ("b".to_string(),Binding::NameBind)];
    ctx1.push(("c".to_string(),Binding::NameBind));
    let (ctx2, name2) = pick_fresh_name(&ctx1, &"d".to_string());
    assert_eq!(name2, "d");
    let (ctx3, name3) = pick_fresh_name(&ctx2, &"d".to_string());
    assert_eq!(name3, "d'");
    let (ctx4, name4) = pick_fresh_name(&ctx3, &"d".to_string());
    assert_eq!(name4, "d''");
}

#[test]
fn print_term_test() {
    let ctx5:Context = vec![("a".to_string(),Binding::NameBind),
                            ("b".to_string(),Binding::NameBind)];
    assert_eq!(print_term(&ctx5, &Var(0, 2)), "b");
    assert_eq!(print_term(&ctx5, &Var(1, 2)), "a");
    assert_eq!(print_term(&ctx5, &abst("x", Var(0,3))), "(lambda x. x)");
    assert_eq!(print_term(&ctx5, &abst("x", Var(1,3))), "(lambda x. b)");
    assert_eq!(print_term(&ctx5, &abst("x", Var(2,3))), "(lambda x. a)");
    assert_eq!(print_term(&ctx5, &abst("b", Var(0,3))), "(lambda b'. b')");
    assert_eq!(print_term(&ctx5, &abst("b", Var(1,3))), "(lambda b'. b)");
    assert_eq!(print_term(&ctx5, &abst("b", Var(2,3))), "(lambda b'. a)");

    let ctx6:Context = vec![("a".to_string(),Binding::NameBind),
                            ("b".to_string(),Binding::NameBind)];
    assert_eq!(print_term(&ctx6, &apply(abst("x", Var(0,3)), Var(0,2))), "((lambda x. x) b)");
}

#[test]
fn term_shift_test() {
    let ctx7:Context = vec![("b".to_string(),Binding::NameBind),
                            ("a".to_string(),Binding::NameBind),
                            ("y".to_string(),Binding::NameBind),
                            ("x".to_string(),Binding::NameBind)];

    assert_eq!(print_term(&ctx7, &Var(0,4)), "x");
    assert_eq!(print_term(&ctx7, &Var(1,4)), "y");
    assert_eq!(print_term(&ctx7, &Var(2,4)), "a");
    assert_eq!(print_term(&ctx7, &Var(3,4)), "b");

    assert_eq!(print_term(&ctx7, &term_shift(1, &Var(0,3))), "y");
    assert_eq!(print_term(&ctx7, &term_shift(2, &Var(0,2))), "a");
    assert_eq!(print_term(&ctx7, &term_shift(3, &Var(0,1))), "b");
    assert_eq!(print_term(&ctx7, &term_shift(1, &Var(1,3))), "a");
    assert_eq!(print_term(&ctx7, &term_shift(2, &Var(1,2))), "b");
}

#[test]
fn term_shift_minus_test() {
    let mut ctx8:Context = vec![("b".to_string(),Binding::NameBind),
                                ("a".to_string(),Binding::NameBind),
                                ("y".to_string(),Binding::NameBind),
                                ("x".to_string(),Binding::NameBind)];
    ctx8.pop();
    assert_eq!(print_term(&ctx8, &term_shift(-1, &Var(1,4))), "y");
}

#[test]
fn practices_test() {
    // 演習6.2.2.(1) ↑2(λ.λ. 1 (0 2))
    let t1 = abst("a", abst("b", apply(Var(1,4), apply(Var(0,4), Var(2,4)))));
    let t2 = abst("a", abst("b", apply(Var(1,6), apply(Var(0,6), Var(4,6)))));
    assert_eq!(term_shift(2, &t1), t2);

    // 演習6.2.2.(2) ↑2(λ. 0 1 (λ. 0 1 2)) = ↑2(λ. ((0 1) (λ. (0 1) 2)))= λ. ((0 3) (λ. (0 1) 4))
    let t3 = abst("b", apply(apply(Var(0,4),Var(1,4)), abst("a", apply(apply(Var(0,4), Var(1,4)), Var(2,4)))));
    let t4 = abst("b", apply(apply(Var(0,6),Var(3,6)), abst("a", apply(apply(Var(0,6), Var(1,6)), Var(4,6)))));
    assert_eq!(term_shift(2, &t3), t4);
    
    assert_eq!(term_subst(0, &Var(0,2), &Var(1,2)), Var(1,2)); // k!=j
    assert_eq!(term_subst(1, &Var(0,2), &Var(1,2)), Var(0,2)); // k=j
    
    assert_eq!(term_subst(1, &Var(1,2), &abst("a", Var(0,2))), abst("a", Var(0,2)));
    assert_eq!(term_subst(6, &Var(1,2), &abst("a", Var(7,2))), abst("a", Var(2,3)));

    // 演習6.2.5.(1)
    assert_eq!(term_subst(5, &Var(999,2), &apply(Var(5,2), abst("x", abst("y", Var(7,2))))),
               apply(Var(999, 2), abst("x", abst("y", Var(1001, 4)))));

    // 演習6.2.5.(2)
    assert_eq!(term_subst(9, &apply(Var(6,2), abst("z", Var(6,2))), &apply(Var(9,2), abst("x", Var(10,2)))),
               apply(apply(Var(6, 2), abst("z", Var(6, 2))), abst("x", apply(Var(7, 3), abst("z", Var(7, 3)))))
               ); // [b->a (\z.a)] (b (\x.b)) = (a \z.a) ((\x a) (\z. a))
}

#[test]
fn eval_test() {
    use named::{var, apply, abst};
    assert_eq!(format!("{:?}", apply(abst("y", var("y")), abst("x", var("x"))).remove_names().eval()),
               "(lambda x. x)");

    // 演習6.2.5.(1)
    assert_eq!(format!("{:?}", &apply(abst("b",
                                           apply(var("b"), abst("x", abst("y", var("b"))))),
                                      abst("a", var("a"))).remove_names().eval()),
               "(lambda x. (lambda y. (lambda a. a)))");

    // 演習6.2.5.(2)
    assert_eq!(format!("{:?}",
                       apply(abst("a", 
                                   apply(abst("b",
                                              apply(var("b"), abst("x", var("b")))),
                                         apply(var("a"), abst("z", var("a")))
                                         )),
                              abst("w", var("w"))
                              ).remove_names().eval()),
               "(lambda w. w)");
}