alpha-conversion when substituting variables under lambda

1 files changed, 19 insertions, 0 deletions

diff --git a/rust/src/lambda.rs b/rust/src/lambda.rs
index d767003..0080f63 100644
--- a/rust/src/lambda.rs
+++ b/rust/src/lambda.rs
@@ -1,3 +1,4 @@
+use rand::Rng;
 use std::fs::read_to_string;
 
 mod ast;
@@ -32,12 +33,24 @@ fn apply(l: &Value, r: &Value) -> Value {
 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(),
     }
 }
 
+fn gensym() -> String {
+    let mut rng = rand::thread_rng();
+
+    let n1: u8 = rng.gen();
+    format!("x_{}", n1)
+}
+
 #[cfg(test)]
 mod lambda_test {
     use crate::{interpret, parse, Value};
@@ -68,4 +81,10 @@ mod lambda_test {
             interpret(&value)
         );
     }
+
+    #[test]
+    fn substitution_does_not_capture_free_variables() {
+        let value = parse("(((lam x (lam x x)) 13) 12)");
+        assert_eq!(Value::Num(12), interpret(&value));
+    }
 }