Haskell - 将De Bruijn术语转换为Lambda术语(反之亦然)

Question

我有一个编写Haskell程序的任务,该程序能够将De Bruijn术语转换为Lambda术语,并将Lambda术语转换为De Bruijn术语,并检查术语是否"关闭".

我不是在寻找某人为我做这项任务,但我们将非常感谢您的帮助!我对如何开始这个问题基本上一无所知.

所以,我最大的问题是:De Bruijn术语和Lambda术语之间的区别是什么？我理解变量"闭合"意味着什么,但我怎样才能在Haskell中检查它？

您可以想到的任何其他帮助将不胜感激.

这是完整的任务:

(通常)lambda术语定义为数据类型:

data Term = Var Int | Lam Int Term | App Term Term deriving (Eq, Show, Read)

变量表示为整数.一个术语被称为关闭,如果每个i人Var i都有Lam i <subterm>从它到根的路径上的from 一个术语,为它提供一个绑定.

De Bruijn术语被定义为数据类型:

data BTerm =BVar Int | BLam BTerm | BApp BTerm BTerm deriving (Eq,  Show, Read)

编写一个Haskell函数db2lam,将de Bruijn项转换为lambda项.编写一个Haskell函数lam2db,将lambda项转换为Bruijn项.

编写一个isClosed测试lambda术语是否关闭的函数.编写一个函数isClosed来测试de Bruijn项是否已关闭.

选择以下两个科目之一:

a)为de Bruijn术语实现正常的顺序beta减少b)对(通常的)lambda术语实施正常的顺序beta减少

非常感谢您的帮助(大或小)!我正处于学习Haskell的早期阶段,很抱歉这么不确定!这个任务在这个时候是我的头脑.

Answer 1

基本上你的任务是要求你探索"命名"和"无名"lambda calculi实现之间的区别.通常,当我们作为人类编写lambda术语时,我们使用命名变量来编写它们

(\g -> (\f -> f (\x -> g x))) (\m -> m)

这假设每当一个名字被一个lambda"绑定"时,我们就可以独特地追踪所有在lambda体中使用该名称的地方.特别是,像"阴影"这样的概念变得很重要.

作为一个小的切线,重要的是要注意当我们写下名为lambda的术语时,它们是非唯一的.如果我们真的很迂腐,那么我们会注意到(\x -> x)并且(\y -> y)是不同的术语.我们理解它们最终代表相同的"过程",因此引入了α等价的概念来处理两个相似的命名lambda术语实际上可能在功能上相同的事实.这是一个名为lambda术语的语句"在重命名时是唯一的",其中"重命名"按照您认为应该的方式工作.

名为lambda术语的一个更重要的方面是"通过替换捕获",这是天真实现中的一个缺陷.特别是,虽然α等价表明两个术语相等于重命名,但这可能会被某些病态的,冲突的重命名所违反,例如:

(\x -> (\q -> q x))  ====>  (\x -> (\x -> x x))

虽然重命名q -> x可能是允许的,因为我改变了q-lambda术语"捕获"变量的方式,这导致我的程序的含义发生变化.这显然是病态的,但在实施替代时也很容易意外制定.

捕获避免替代通常是一个重要的事情.随着LC ADT的片段移动并在其新的替代上下文中进行解释,其含义会发生变化,并且必须考虑到这种变化.也就是说,使用命名术语的捕获避免替换可能是昂贵的,因为必须知道整个术语的上下文以识别哪些名称有被捕获的风险.

因此,出于这两个原因,尽管人们对语言的熟悉程度,但对于等效性和捕获命名风险的需求并不总是最佳选择.

所以现在我们转向无名的术语.de Bruijn将您的作业要求您实施的是无名的.特别是,如果你看一下ADT,很明显BLams不再指定哪个变量受它们约束 - 我们只是被迫从ADT结构中确定变量的含义.

特别是,规则是变量是绑定它们的lambda的指针.A BVar n绑定在它n BLam上面的lambda .因此,如果我们要将一个从命名的翻译成无名的翻译,他们就会看起来像

(\x -> x)            ===>  (\ 0)
(\x -> (\q -> q x))  ===>  (\ (\ 0 1))

(\g -> (\f -> f (\x -> g x))) (\m -> m)
===>
(\ (\ 0 (\ 2 0))) (\ 0)

无名的术语很难像人类一样阅读,但它们有两个很好的特质:

1. 不再存在alpha等价的东西了; 两个无名的术语在结构上相等时完全代表相同的计算
2. 由于变量非常系统地"命名",完全归因于实现捕获避免的术语结构,因此更简单.