Skip to content

Instantly share code, notes, and snippets.

@uehaj
Last active Jan 21, 2018
Embed
What would you like to do?
TAPLのML実装をRustでやってみるシリーズ「7章 ラムダ計算のML実装」
[package]
name = "ch7"
version = "0.0.1"
authors = ["UEHARA Junji <uehaj@jggug.org>"]
#![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());
}
#![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)))");
}
// 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)");
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment