考虑以下无类型lambda演算的实现：
pub enum Term {
Var(usize), // a variable with a De Bruijn index
Abs(Box<Term>), // an abstraction
App(Box<Term>, Box<Term>) // an application
}
impl Term {
...
}
我觉得这种设计虽然简单简洁，但可以从转化为特征中受益。不同的术语应该有不同的方法集，例如，只有抽象应该是"不可抽象的"，只有应用程序应该是可评估的。
我知道枚举与特征中常见的争论;即使枚举是更好的选择，我仍然想知道它是否可能。
到目前为止，我的基本构建块或多或少如下：
#[derive(Clone, PartialEq, Eq)]
pub struct Var(usize);
#[derive(Clone, PartialEq, Eq)]
pub struct Abs<T: Term>(T);
#[derive(Clone, PartialEq, Eq)]
pub struct App<T: Term, U: Term>(T, U);
pub trait Term: Clone {
fn abs(self) -> Abs<Self> { Abs(self) }
fn app<T: Term>(self, other: T) -> App<Self, T> { App(self, other) }
fn update_free_variables(&mut self, added_depth: usize, own_depth: usize);
fn _apply<T: Term>(&mut self, other: &mut T, depth: usize); // this is a helper function that enables term tree traversal for Abs<T>::apply
fn is_reducible(&self, limit: usize, count: &usize) -> bool;
fn beta_reduce(&mut self, order: Order, limit: usize, verbose: bool) -> usize;
}
impl Var {
pub fn new(index: usize) -> Self {
assert!(index > 0);
Var(index)
}
}
impl<T: Term> Abs<T> {
fn unabs(self) -> T {
self.0
}
fn apply<U: Term>(mut self, other: &mut U) -> T {
self._apply(other, 0);
self.unabs()
}
}
impl<T: Term, U: Term> App<T, U> {
fn unapp(self) -> (T, U) {
(self.0, self.1)
}
}
// and some impl Term for X
虽然实现基本功能非常容易，但在某些地方我正在努力提出正确的解决方案。我需要能够执行以下操作：
- 创建一个能够使用单个函数解释任何术语(从普通变量到复杂术语)的解析器
- 将任何变量(无论嵌套多深)替换为另一个变量或其他术语
- 递归减少术语(我不确定对于可能必须是特征对象的解析术语是否可能)
我宁愿尝试自己实现它，我只需要一些关于方向的建议。没有枚举包装器甚至可能吗？如果是这样，我应该采取什么方法(在对象安全、unsafe诡计等方面)？
枚举与特征
不同的术语应该有不同的方法集，例如，只有抽象应该是"不可抽象的"，只有应用程序应该是可评估的。
我不认为这是基于特征的设计的一个很好的论据。通过模式匹配，枚举在运行时公开术语类型之间的差异，但特征隐藏了这些差异，迫使您以相同的方式处理所有术语。在编译时，您可能不知道术语的类型，因此为不同类型的术语提供不同的方法没有多大意义。如果要使用特定于每种类型的术语的功能，而不是仅通过统一接口与术语进行多态交互，则应使用基于枚举的设计。
如果您决定坚持使用基于 trait 的实现，则需要删除所有泛型方法并改用 trait 对象。如果动态调度具有泛型方法，则无法对Term使用动态调度，因为它不是对象安全的。
基于特征的设计的一个潜在优势是可扩展性，但在这种情况下，这不是一个问题，因为非类型化 lambda 演算的定义是固定的。
三个问题
创建一个能够使用单个函数解释任何术语(从普通变量到复杂术语)的解析器
如果所有应用程序都需要用括号括起来，则解析表达式应该相当简单。我在解析方面没有太多经验，但我可能会尝试这样的递归方法：
To read one term, given a mutable reference to a variable stack (which begins empty):
If the next character is an opening parenthesis:
Consume it.
Read a term.
Read a term.
Make sure the next character is a closing parenthesis, and consume it.
Return an application of the two terms.
If the next character is a lambda:
Consume it.
Make sure the next character is a variable, then consume it.
Make sure the next character is a dot, and consume it.
Push the variable to the variable stack.
Read a term.
Pop the variable off of the stack.
Return an abstraction of the term.
If the next character is a variable:
Consume it.
Search the variable stack find the first index of the variable from the top.
Return a variable term with this index.
您可以修改此设置以接受 lambda 演算表示法中的常见快捷方式，例如(a b c)for((a b) c)。目前，它将接受λx.λy.λz.((x z) (y z))但不接受λx.λy.λz.x z (y z)。
将任何变量(无论嵌套多深)替换为另一个变量或其他术语
我假设变量项存储的数字是引入变量的点和使用变量的点之间的抽象层数。如果是这种情况，则可以递归遍历结构，同时记住当前的抽象深度。当遇到与数字匹配的变量时，它将被替换为给定项，除了该项中的所有自由变量(可以通过查找数字大于给定项中抽象深度的变量来找到)应将当前抽象深度添加到其数字中以解释级别差异。遇到应用程序时，将在其两个子项中递归执行替换过程。当遇到新的抽象时，替换在其主体中递归执行，抽象深度增加 1 以考虑新层。
如果你真的想使用特征，那么Term会有这样的方法：
fn substitute(&mut self, variable_number: usize, other: &Term);
只是为了澄清编号系统，以下是否正确？
λn.λf.λx.(f ((n f) x))→Abs(Abs(Abs(App(Var(1),App(App(Var(2),Var(1)),Var(0))))))
递归减少术语(我不确定对于可能必须是特征对象的解析术语是否可能)
虽然很麻烦，但这可以通过特征对象来实现。你可以在Term中定义两个方法，第一个方法除了在Abs实现中什么都不做，在实现中，它接受一个项并返回抽象的主体，在变量索引 0 处替换给定的项。第二种方法除了在App实现中之外什么都不做，它将在应用程序的左侧项上调用第一种方法，传递正确的项。使用类似的策略，您可以定义查找 beta 可约项的方法，并且通过组合这些方法，您可以对枚举模式匹配进行混乱的模拟，这将是完成此任务的更好工具。
您可能会发现本文在实施β还原时很有帮助。我没有读太多，但它似乎为有效的β减少算法提供了策略。
再次与特征
尽管枚举和特征可以实现相同的行为，但当不需要可扩展性并且需要以复杂的方式分析和重新排列数据结构时，枚举是更好的选择。对于这个问题，基于枚举的解决方案可能更胜一筹。