From 2448ee4ea0cfbd585a214ff90cf9a2da10113bb0 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Sun, 2 Oct 2022 18:59:29 +0200
Subject: [PATCH] [WIP] feat(term): Improve beta-reduction + Add tests
---
core/src/lib.rs | 1 +
core/src/term.rs | 252 +++++++++++++++++++++++++++++++++++++++++------
2 files changed, 225 insertions(+), 28 deletions(-)
diff --git a/core/src/lib.rs b/core/src/lib.rs
index 30e5e5c8..b91b3b42 100644
--- a/core/src/lib.rs
+++ b/core/src/lib.rs
@@ -1,3 +1,4 @@
+#![feature(box_patterns)]
#![feature(box_syntax)]
mod command;
diff --git a/core/src/term.rs b/core/src/term.rs
index 6277231a..acda4ef1 100644
--- a/core/src/term.rs
+++ b/core/src/term.rs
@@ -13,20 +13,25 @@ pub enum Term {
use Term::*;
impl Term {
+ /// Returns the normal form of the term
+ ///
+ /// # Examples
+ ///
+ /// ```
+ /// // TODO: Use parser
+ /// ```
pub fn beta_reduction(self) -> Term {
match self {
- App(box Abs(_, box mut t1), box t2) => {
- t1.substitute(t2, 1);
- t1
- }
+ App(box Abs(_, box t1), box t2) => t1.substitute(t2, 1),
+ App(box t1, box t2) => App(box t1.beta_reduction(), box t2.beta_reduction()),
Abs(x, box t) => Abs(x, box t.beta_reduction()),
_ => self,
}
}
- fn shift(&mut self, offset: usize) -> Term {
+ fn shift(self, offset: usize) -> Term {
match self {
- Var(x) => Var(*x + offset),
+ Var(x) => Var(x + offset),
App(box t1, box t2) => App(box t1.shift(offset), box t2.shift(offset)),
Abs(x, box t) => Abs(x.clone(), box t.shift(offset)),
Prod(x, box t) => Prod(x.clone(), box t.shift(offset)),
@@ -34,18 +39,18 @@ impl Term {
}
}
- fn substitute(&mut self, rhs: Term, depth: usize) {
+ fn substitute(self, rhs: Term, depth: usize) -> Term {
match self {
- Var(i) if *i == depth => *self = rhs.clone().shift(depth - 1),
- Var(i) if *i != depth => *self = Var(*i - 1),
- App(l, r) => {
- l.substitute(rhs.clone(), depth);
- r.substitute(rhs, depth);
- }
- Abs(_, t) | Prod(_, t) => {
- t.substitute(rhs, depth + 1);
- }
- _ => {}
+ Var(i) if i == depth => rhs.shift(depth - 1),
+ Var(i) if i > depth => Var(i - 1),
+
+ App(l, r) => App(
+ box l.substitute(rhs.clone(), depth),
+ box r.substitute(rhs, depth),
+ ),
+ Abs(t, term) => Abs(t, box term.substitute(rhs, depth + 1)),
+ Prod(t, term) => Prod(t, box term.substitute(rhs, depth + 1)),
+ _ => self,
}
}
}
@@ -63,17 +68,208 @@ impl Display for Term {
}
}
-#[test]
-fn subst() {
- let term = Abs(
- box Prop,
- box App(
- box Abs(box Prop, box App(box Var(2), box Var(1))),
- box Var(1),
- ),
- );
+#[cfg(test)]
+mod tests {
+ // TODO: Correctly types lambda terms.
+
+ use super::Term::*;
+
+ #[test]
+ fn simple_subst() {
+ // λx.(λy.x y) x
+ let term = Abs(
+ box Prop,
+ box App(
+ box Abs(box Prop, box App(box Var(2), box Var(1))),
+ box Var(1),
+ ),
+ );
+
+ // λx.x x
+ let reduced = Abs(box Prop, box App(box Var(1), box Var(1)));
+
+ assert_eq!(term.beta_reduction(), reduced);
+ }
+
+ #[test]
+ fn complex_subst() {
+ // [λa.λb.λc.a (λd.λe.e (d b)) (λ_.c) (λd.d)] (λa.λb.a b)
+ let term = App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box Var(3),
+ box App(
+ box App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(4))),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ ),
+ ),
+ ),
+ box Abs(box Prop, box Abs(box Prop, box App(box Var(2), box Var(1)))),
+ );
+
+ // λa.λb.((λc.(λd.λe.e (d a)) c) (λ_.b)) (λc.c)
+ // λa.λb.((λc.λd.(d (c a))) (λ_.b)) (λc.c)
+ // λa.λb.(λc.c ((λ_.b) a)) (λc.c)
+ // λa.λb.(λc.c) ((λ_.b) a)
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(term.beta_reduction(), reduced);
+ }
+
+ #[test]
+ fn complex_subst_step_5() {
+ // λa.λb.((λc.(λd.λe.e (d a)) c) (λ_.b)) (λc.c)
+ let term = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(5))),
+ ),
+ ),
+ box Var(1),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(
+ term.beta_reduction()
+ .beta_reduction()
+ .beta_reduction()
+ .beta_reduction()
+ .beta_reduction(),
+ reduced
+ );
+ }
- let reduced = Abs(box Prop, box App(box Var(1), box Var(1)));
+ #[test]
+ fn complex_subst_step_4() {
+ // λa.λb.((λc.λd.(d (c a))) (λ_.b)) (λc.c)
+ let term = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box App(
+ box Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(box Var(1), box App(box Var(2), box Var(4))),
+ ),
+ ),
+ box Abs(box Prop, box Var(2)),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
- assert_eq!(term.beta_reduction(), reduced);
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(
+ term.beta_reduction()
+ .beta_reduction()
+ .beta_reduction()
+ .beta_reduction(),
+ reduced
+ );
+ }
+
+ #[test]
+ fn complex_subst_step_3() {
+ // λa.λb.(λc.c ((λ_.b) a)) (λc.c)
+ let term = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(
+ box Prop,
+ box App(
+ box Var(1),
+ box App(box Abs(box Prop, box Var(3)), box Var(3)),
+ ),
+ ),
+ box Abs(box Prop, box Var(1)),
+ ),
+ ),
+ );
+
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(
+ term.beta_reduction().beta_reduction().beta_reduction(),
+ reduced
+ );
+ }
+
+ #[test]
+ fn complex_subst_step_2() {
+ // λa.λb.(λc.c) ((λ_.b) a)
+ let term = Abs(
+ box Prop,
+ box Abs(
+ box Prop,
+ box App(
+ box Abs(box Prop, box Var(1)),
+ box App(box Abs(box Prop, box Var(2)), box Var(2)),
+ ),
+ ),
+ );
+
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(term.beta_reduction().beta_reduction(), reduced);
+ }
+
+ #[test]
+ fn complex_subst_step_1() {
+ // λa.λb.(λc.b) a
+ let term = Abs(
+ box Prop,
+ box Abs(box Prop, box App(box Abs(box Prop, box Var(2)), box Var(2))),
+ );
+
+ // λa.λb.b
+ let reduced = Abs(box Prop, box Abs(box Prop, box Var(1)));
+
+ assert_eq!(term.beta_reduction(), reduced);
+ }
}
--
GitLab