diff options
Diffstat (limited to 'lambda-calcul/rust/src/lambda.rs')
| -rw-r--r-- | lambda-calcul/rust/src/lambda.rs | 292 |
1 files changed, 292 insertions, 0 deletions
diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs new file mode 100644 index 0000000..a73ca34 --- /dev/null +++ b/lambda-calcul/rust/src/lambda.rs @@ -0,0 +1,292 @@ +use proptest::{ + arbitrary::any, + prelude::*, + strategy::{Strategy, ValueTree}, + test_runner::TestRunner, +}; +use rand::Rng; +use std::collections::HashMap; + +use crate::ast::*; + +#[derive(Debug, PartialEq)] +pub struct Environment<'a> { + parent: Box<Option<&'a Environment<'a>>>, + bindings: HashMap<String, Value>, +} + +impl<'a> Environment<'a> { + pub fn new() -> Self { + Environment { + parent: Box::new(None), + bindings: HashMap::new(), + } + } + + fn bind(&mut self, var: &str, value: &Value) { + self.bindings.insert(var.to_string(), value.clone()); + } + + fn extends(&'a self) -> Self { + Environment { + parent: Box::new(Some(self)), + bindings: HashMap::new(), + } + } + + fn lookup(&self, var: &str) -> Option<&Value> { + self.bindings.get(var).or_else(|| match *self.parent { + Some(parent) => parent.lookup(var), + None => None, + }) + } +} + +impl<'a> Default for Environment<'a> { + fn default() -> Self { + Self::new() + } +} + +pub fn eval_all(values: &[Value]) -> Vec<Value> { + let mut env = Environment::new(); + values.iter().map(|v| eval_whnf(v, &mut env)).collect() +} + +/// Reduce the given value to weak head normal form using call-by-name +/// evaluation strategy. +/// +/// call-by-name reduces the leftmost outermost redex first, which is +/// not under a lambda abstraction. +pub fn eval_whnf(arg: &Value, env: &mut Environment) -> Value { + match arg { + Value::Def(var, value) => { + env.bind(var, value); + Value::Bool(true) // TODO: return a more meaningful value? + } + Value::Let(var, value, expr) => { + let mut newenv = env.extends(); + newenv.bind(var, value); + eval_whnf(expr, &mut newenv) + } + Value::App(l, r) => match eval_whnf(l, env) { + Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env), + Value::Sym(var) => match env.lookup(&var) { + Some(val) => eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env), + None => arg.clone(), + }, + other => Value::App(Box::new(other), r.clone()), + }, + Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(), + other => other.clone(), + } +} + +fn subst(var: &str, body: &Value, e: &Value) -> Value { + match body { + Value::Sym(x) if x == var => e.clone(), + Value::Lam(x, b) if x == var => { + let y = gensym(); + let bd = subst(x, b, &Value::Sym(y.clone())); + Value::Lam(y, Box::new(bd)) + } + Value::Lam(x, b) => Value::Lam(x.to_string(), Box::new(subst(var, b, e))), + Value::App(l, r) => Value::App(Box::new(subst(var, l, e)), Box::new(subst(var, r, e))), + other => other.clone(), + } +} + +pub fn gensym() -> String { + let mut rng = rand::thread_rng(); + + let n1: u8 = rng.gen(); + format!("x_{}", n1) +} + +pub fn generate_expr(size: u32, runner: &mut TestRunner) -> Value { + match size { + 0 | 1 => { + let n = any::<u16>().new_tree(runner).unwrap().current(); + Value::Num(n.into()) + } + 2 => Value::Sym(ascii_identifier().new_tree(runner).unwrap().current()), + 3 => any_sym().new_tree(runner).unwrap().current(), + 4 => simple_app().new_tree(runner).unwrap().current(), + 5 => nested_simple_app().new_tree(runner).unwrap().current(), + 6 => simple_lambda().new_tree(runner).unwrap().current(), + 7 => app_to_lambda().new_tree(runner).unwrap().current(), + 8 => multi_app().new_tree(runner).unwrap().current(), + _ => any::<u32>() + .prop_flat_map(gen_terms) + .new_tree(runner) + .unwrap() + .current(), + } +} + +pub fn generate_exprs(size: u32, runner: &mut TestRunner) -> Vec<Value> { + let sz = (0..size).new_tree(runner).unwrap().current(); + (0..sz) + .collect::<Vec<_>>() + .into_iter() + .map(|_| generate_expr(size, runner)) + .collect() +} + +fn simple_app() -> impl Strategy<Value = Value> { + let leaf = prop_oneof![any_num(), any_sym()]; + (leaf.clone(), leaf.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r))) +} + +fn multi_app() -> impl Strategy<Value = Value> { + let leaf = prop_oneof![any_num(), any_sym()]; + (leaf.clone(), leaf.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r))) +} + +fn any_num() -> impl Strategy<Value = Value> { + any::<i32>().prop_map(Value::Num) +} + +fn nested_simple_app() -> impl Strategy<Value = Value> { + let leaf = prop_oneof![any_num(), ascii_identifier().prop_map(Value::Sym)]; + leaf.prop_recursive(4, 128, 5, move |inner| { + (inner.clone(), inner.clone()).prop_map(|(l, r)| Value::App(Box::new(l), Box::new(r))) + }) +} + +fn any_sym() -> impl Strategy<Value = Value> { + identifier().prop_map(Value::Sym) +} + +fn simple_lambda() -> impl Strategy<Value = Value> { + // TODO: there's nothing to guarantee the variable appears in the body + (ascii_identifier(), nested_simple_app()).prop_map(|(v, b)| Value::Lam(v, Box::new(b))) +} + +fn app_to_lambda() -> impl Strategy<Value = Value> { + let lam = simple_lambda(); + let arg = prop_oneof![any_num(), any_sym(), nested_simple_app()]; + (lam, arg).prop_map(|(l, a)| Value::App(Box::new(l), Box::new(a))) +} + +/// Cantor pairing function +/// See https://en.wikipedia.org/wiki/Pairing_function +fn pairing(k: u32) -> (u32, u32) { + let a = ((((8 * (k as u64) + 1) as f64).sqrt() - 1.0) / 2.0).floor(); + let b = (a * (a + 1.0)) / 2.0; + let n = (k as f64) - b; + (n as u32, (a - n) as u32) +} + +fn gen_terms(u: u32) -> impl Strategy<Value = Value> { + if u % 2 != 0 { + let j = (u - 1) / 2; + if j % 2 == 0 { + let k = j / 2; + let (n, m) = pairing(k); + let r = (gen_terms(n), gen_terms(m)) + .prop_map(move |(l, r)| Value::App(Box::new(l), Box::new(r))); + r.boxed() + } else { + let k = (j - 1) / 2; + let (n, m) = pairing(k); + let r = gen_terms(m).prop_map(move |v| Value::Lam(format!("x_{}", n), Box::new(v))); + r.boxed() + } + } else { + let j = u / 2; + Just(Value::Sym(format!("x_{}", j))).boxed() + } +} + +#[cfg(test)] +mod lambda_test { + use crate::parser::parse; + + use super::{eval_all, eval_whnf, Environment, Value}; + + fn parse1(string: &str) -> Value { + parse(string).pop().unwrap() + } + + fn eval1(value: &Value) -> Value { + eval_whnf(value, &mut Environment::new()) + } + + #[test] + fn evaluating_a_non_reducible_value_yields_itself() { + let value = parse1("(foo 12)"); + assert_eq!(value, eval1(&value)); + } + + #[test] + fn evaluating_application_on_an_abstraction_reduces_it() { + let value = parse1("((lam x x) 12)"); + assert_eq!(Value::Num(12), eval1(&value)); + } + + #[test] + fn substitution_occurs_within_abstraction_body() { + let value = parse1("(((lam x (lam y x)) 13) 12)"); + assert_eq!(Value::Num(13), eval1(&value)); + } + + #[test] + fn substitution_occurs_within_application_body() { + let value = parse1("(((lam x (lam y (y x))) 13) 12)"); + assert_eq!( + Value::App(Box::new(Value::Num(12)), Box::new(Value::Num(13))), + eval1(&value) + ); + } + + #[test] + fn substitution_does_not_capture_free_variables() { + let value = parse1("(((lam x (lam x x)) 13) 12)"); + assert_eq!(Value::Num(12), eval1(&value)); + } + + #[test] + fn interpretation_applies_to_both_sides_of_application() { + let value = parse1("((lam x x) ((lam x x) 12))"); + assert_eq!(Value::Num(12), eval1(&value)); + } + + #[test] + fn reduction_is_applied_until_normal_form_is_reached() { + let value = parse1("((((lam y (lam x (lam y (x y)))) 13) (lam x x)) 11)"); + assert_eq!(Value::Num(11), eval1(&value)); + } + + #[test] + fn reduction_always_select_leftmost_outermost_redex() { + // this should not terminate if we evaluate the rightmost redex first, eg. + // applicative order reduction + let value = parse1("((lam x 1) ((lam x (x x)) (lam x (x x))))"); + assert_eq!(Value::Num(1), eval1(&value)); + } + + #[test] + fn defined_symbols_are_evaluated_to_their_definition() { + let values = parse("(def foo 12) foo"); + assert_eq!(vec![Value::Bool(true), Value::Num(12)], eval_all(&values)); + } + + #[test] + fn let_expressions_bind_symbol_to_expression_in_environment() { + let values = parse("(let (foo (lam x x)) (foo 12))"); + assert_eq!(vec![Value::Num(12)], eval_all(&values)); + } + + #[test] + fn let_expressions_introduce_new_scope_for_bindings() { + let values = parse("(let (foo (lam x x)) ((let (foo foo) foo) 13))"); + assert_eq!(vec![Value::Num(13)], eval_all(&values)); + } + + #[test] + fn bound_symbol_in_higher_scope_are_resolved() { + let values = parse("(let (id (lam x x)) (let (foo 12) (id foo)))"); + assert_eq!(vec![Value::Num(12)], eval_all(&values)); + } +} |