From b9e4b40b826c7b735e1c38b11a622f2f1f463f4a Mon Sep 17 00:00:00 2001 From: agentelement Date: Sat, 25 May 2024 01:29:51 -0700 Subject: [PATCH 1/3] feat: Term::has_free_variables() --- src/term.rs | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/src/term.rs b/src/term.rs index 823d83a..94a3db0 100644 --- a/src/term.rs +++ b/src/term.rs @@ -445,6 +445,32 @@ impl Term { _ => false, } } + + /// Returns `true` if `self` has any free vairables. + /// + /// # Example + /// ``` + /// use lambda_calculus::*; + /// + /// let with_freevar = abs(Var(2)); // λ 2 + /// let without_freevar = abs(Var(1)); // λ 1 + /// + /// assert!(with_freevar.has_free_variables()); + /// assert!(!without_freevar.has_free_variables()); + pub fn has_free_variables(&self) -> bool { + self.has_free_variables_helper(0) + } + + fn has_free_variables_helper(&self, depth: usize) -> bool { + match self { + Var(x) => x > &depth, + Abs(p) => p.has_free_variables_helper(depth + 1), + App(p_boxed) => { + let (ref f, ref a) = **p_boxed; + f.has_free_variables_helper(depth) && a.has_free_variables_helper(depth) + } + } + } } /// Wraps a `Term` in an `Abs`traction. Consumes its argument. @@ -713,4 +739,10 @@ mod tests { assert!(app(abs(Var(1)), Var(1)).is_isomorphic_to(&app(abs(Var(1)), Var(1)))); assert!(!app(abs(Var(1)), Var(1)).is_isomorphic_to(&app(Var(2), abs(Var(1))))); } + + #[test] + fn has_free_variables() { + assert!(!(abs(Var(1)).has_free_variables())); + assert!(abs(Var(2)).has_free_variables()); + } } From 3bc1afd5804bc3ebc0b9008a791c4d265f1bb656 Mon Sep 17 00:00:00 2001 From: agentelement Date: Thu, 30 May 2024 00:27:09 -0700 Subject: [PATCH 2/3] fix: has_free_variables considers Var(0) free --- src/term.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/term.rs b/src/term.rs index 94a3db0..0c61813 100644 --- a/src/term.rs +++ b/src/term.rs @@ -463,7 +463,7 @@ impl Term { fn has_free_variables_helper(&self, depth: usize) -> bool { match self { - Var(x) => x > &depth, + Var(x) => *x > depth || *x == 0, Abs(p) => p.has_free_variables_helper(depth + 1), App(p_boxed) => { let (ref f, ref a) = **p_boxed; @@ -744,5 +744,6 @@ mod tests { fn has_free_variables() { assert!(!(abs(Var(1)).has_free_variables())); assert!(abs(Var(2)).has_free_variables()); + assert!((Var(0)).has_free_variables()); } } From 49aa964afa40de66ac9039e10d6232230452b03f Mon Sep 17 00:00:00 2001 From: agentelement Date: Thu, 30 May 2024 01:21:22 -0700 Subject: [PATCH 3/3] fix: has_free_vars was broken under applications --- src/term.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/term.rs b/src/term.rs index 0c61813..0e732ef 100644 --- a/src/term.rs +++ b/src/term.rs @@ -467,7 +467,7 @@ impl Term { Abs(p) => p.has_free_variables_helper(depth + 1), App(p_boxed) => { let (ref f, ref a) = **p_boxed; - f.has_free_variables_helper(depth) && a.has_free_variables_helper(depth) + f.has_free_variables_helper(depth) || a.has_free_variables_helper(depth) } } } @@ -744,6 +744,15 @@ mod tests { fn has_free_variables() { assert!(!(abs(Var(1)).has_free_variables())); assert!(abs(Var(2)).has_free_variables()); + assert!(app(abs(Var(2)), Var(1)).has_free_variables()); + assert!(app(abs(Var(2)), abs(Var(1))).has_free_variables()); + assert!(app(abs(Var(1)), abs(Var(2))).has_free_variables()); + assert!(!app(abs(Var(1)), abs(Var(1))).has_free_variables()); + assert!(!(abs(app( + abs(app(Var(2), app(Var(1), Var(1)))), + abs(app(Var(2), app(Var(1), Var(1)))), + ))) + .has_free_variables()); assert!((Var(0)).has_free_variables()); } }