Rob*_*ert 6 interpreter haskell
我正在Haskell中编写一个小函数式编程语言,但我找不到如何实现(==)的定义,因为这看起来很棘手？
Joh*_*kin 14
Haskell使用"类型类"的概念.实际定义是这样的:
class Eq a where
(==) :: a -> a -> Bool
-- More functions follow, for more complex concepts of equality (eg NaN)
然后,您可以为自己的类型定义它.例如:
-- Eq can't be automatically derived, because of the function
data Foo = Foo Int (Char -> Bool)
-- So define it here
instance Eq Foo where
(Foo x _) == (Foo y _) = x == y
phy*_*sis 11
我认为你的问题非常非常有趣.如果您还想要了解您的问题背后的理论根源,那么,我认为,我们可以从Haskell中抽象出来并在更一般的算法概念中研究您的问题.至于Haskell,我认为,以下两个事实很重要:
但我还没有完成讨论(语言的力量在这里究竟如何).
我认为,从根本上说,计算机科学的两个定理提供了答案.如果我们想要从技术细节中抽象出来,我们可以在lambda演算中(或在组合逻辑中)研究你的问题.可以在它们中定义相等吗？因此,让我们首先将自己限制在lambda演算或组合逻辑领域.
必须指出的是,这两种算法方法都非常简约.它们中没有"预定义"的数据类型,甚至没有数字,也没有布尔值,也没有列表.但你可以巧妙地模仿所有这些.
因此,即使在诸如lambda演算和组合逻辑之类的极简主义"函数语言"中,您也可以模仿所有有意义的数据类型.您可以在模拟所需数据类型的聪明场景中使用lambda函数(或组合器).
现在让我们首先尝试用这些简约函数式语言回答你的问题,看看答案是否是Haskell特定的,或者更确切地说是一些更一般的定理的结果.
在"实现"数据类型之后,可以为其编写相应的相等函数.对于大多数实际情况(列表,数字,案例分析选择),没有相应的相等函数缺乏的神秘"数据类型".这个肯定的答案由伯姆定理提供.
你可以写一个教会 - 数字 - 相等函数,它取两个教会数字,并回答它们是否相等.你可以编写另一个 lambda函数/组合器,它需要两个(Church)-booleans并回答它们是否相等.此外,您可以在纯lambda演算/ CL中实现列表(建议的方法是使用catamorphisms的概念),然后,您可以定义一个函数来回答布尔列表的相等性.你可以写另一个函数来回答教会数字列表的相等性.您也可以实现树,然后,您可以编写一个函数来回答树的相等性(在布尔值上,另一个在教堂数字上).
您可以自动完成部分工作,但不是全部.您可以自动导出一些(但不是全部)相等的函数.如果您已经具有树和列表的特定映射函数以及布尔值和数字的相等函数,那么您也可以自动为布尔树,布尔列表,数字列表,数字树派生相等函数.
但是没有办法定义一个适用于所有可能的"数据类型"的单一全自动相等函数.如果您在lambda演算中"实现"具体的给定数据类型,则通常必须为该场景规划其特定的相等函数.
此外,没有办法定义一个lambda函数,它将采用两个lambda项并回答,两个lambda项在减少时是否会表现相同.更有甚者,没有办法定义一个lambda函数,它将采用两个lambda项的表示(引用)并回答,两个原始lambda项在减少时是否会表现相同(Csörnyei2007:141,Conseq 7.4.3).那不走的回答是斯科特-库里不可判定定理(Csörnyei2007:140,钍7.4.1)提供.
我认为,上述两个答案并不局限于lambda演算和组合逻辑.类似的可能性和限制适用于其他一些算法概念.例如,没有递归函数可以采用两个一元函数的哥德尔数,并决定这些编码函数是否在扩展方面表现相同(Monk 1976:84,= Cor 5.18).这是莱斯定理的结果(Monk 1976:84,= Th 5.17).我觉得,莱斯的定理听起来与Scott-Curry不可判定性定理非常相似,但我还没有考虑过.
如果我想编写一个组合逻辑解释器来提供全面的相等性测试(限制为暂停,具有正常形式的术语),那么我会这样实现:
如果是这样,那么他们未减少的原始形式也必须在语义上等同.
但这只有严格的限制,尽管这种方法适用于几个实际目标.我们可以在数字,列表,树等之间进行操作,并检查我们是否得到了预期的结果.我的quine(用纯粹的组合逻辑编写)使用这种受限制的平等概念,并且它足够了,尽管这个quine需要非常复杂的结构(在组合逻辑本身中实现的术语树).
我还不知道这种受限制的平等概念的局限是什么,但我怀疑,如果与正确的平等定义相比,它是非常有限的.它使用的动机是它可以计算,不受不受限制的限制.平等的概念.
这种限制也可以从这样一个事实看出,即这种受限制的平等概念只能用于具有正常形式的组合器.对于一个反例:受限制的平等概念不能检查是否我 Ω = Ω,虽然谁都知道这两个词可以相互转化为彼此.
我必须考虑,这种受限制的平等概念的存在如何与斯科特 - 库里不可判定性定理和赖斯定理所声称的负面结果有关.这两个定理都涉及部分函数,但我还不知道这究竟是多么重要.
但是受限制的平等概念还存在进一步的局限性.它无法处理可扩展性的概念.例如,它没有注意到S K以任何方式与K I相关,尽管S K在应用于至少两个参数时表现与K I相同:
必须更详细地解释后一个例子.我们知道,小号 ķ和ķ 我是作为术语不相同:小号 ķ ≢ ķ 我.但是如果我们分别将两者都应用于任何两个参数X和Y,我们就会看到一个相关性:
当然ÿ ≡ Ÿ,任何ÿ.
当然,我们不能为每个可能的X和Y参数实例"尝试"这种相关性,因为可以有无限多个这样的CL术语实例被替换为这些元变量.但我们不必陷入无限的这个问题.如果我们用(自由)变量扩充我们的对象语言(组合逻辑):
我们相应地以适当的方式定义约简规则,然后我们可以以"有限"的方式陈述相等的扩展定义,而不依赖于具有无限可能实例的元变量.
因此,如果在组合逻辑术语中允许自由变量(对象语言用其自己的对象变量进行扩充),则可以在某种程度上实现扩展性.我还没有考虑过这一点.至于上面的例子,我们可以使用表示法
S K = 2 K I.
(Curry&Feys&Craig 1958:162,= 5 C 5),基于S K x y和K I x y可以证明是相等的事实(已经没有求助于扩展性).这里,x和y不是方程式中无限多个CL项的实例的元变量,而是对象语言本身的一等公民.因此,该等式不再是方程式,而是单个等式.
至于理论研究,我们可以通过所有n的= n个实例的"联合"来表示.
或者,可以定义相等性,使其归纳定义也考虑到扩展性.我们再添加一个处理扩展性的推理规则(Csörnyei2007:158):
关于不包含的约束是重要的,如下面的反例所示:K x ≠ I,尽管K x x = I x.两个(偶然发生的)变量出现的"角色"完全不同.排除这种发生率,这就是约束的动机.-
这个新的推理规则的使用可以通过展示如何证明定理S K x = K I x来举例说明:
这些剩余的推论规则是什么？这些是他们列出的(Csörnyei2007:157):
转换公理方案:
平等公理方案和推理规则
我还没有清楚地解释Böhm定理是如何与这样一个事实相关的:在大多数实际情况中,一个合适的相等测试函数肯定可以用于有意义的数据类型(即使在诸如纯lambda演算或组合逻辑之类的极简主义函数语言中).
然后,该定理声称,有一种合适的方法可以测试相等性,并将它们应用于一系列合适的参数.换句话说:存在一个自然数n和一系列闭合的lambda项G 1,G 2,G 3,... G n,这样将它们应用于这一系列的参数分别减少为false和true:
其中,真和假是两个著名的,羊肉驯服,易于管理和区分lambda项:
如何利用这个定理来实现纯lambda演算中的实际数据类型？这个定理的隐含应用可以通过组合逻辑中定义链表的方式来例证(Tromp 1999:Sec 2).
| 归档时间： |
|
| 查看次数： |
937 次 |
| 最近记录： |