haskell - 神灵如何运作？

Question

好吧，所以我意识到我可能会后悔一辈子，但是...... Djinn 实际上是如何工作的？

文档说它使用了一种“LJ 的扩展”算法，并指出了一篇关于 LJT 的长篇令人困惑的论文。据我所知，这是一个由高度形式化的规则组成的庞大复杂系统，用于确定哪些逻辑陈述是真还是假。但这甚至没有开始解释如何将类型签名转换为可执行表达式。想必所有复杂的形式推理都以某种方式参与，但图片是极其不完整的。

<小时/>

这有点像我当时尝试用 BASIC 编写 Pascal 解释器。 (别笑!我才十二岁……)我花了几个小时试图弄清楚，最后我不得不放弃。我只是不明白你到底是如何从包含整个程序的巨大字符串中得到可以与已知程序片段进行比较的东西，以便决定实际做什么。

答案当然是你需要编写一个称为“解析器”的东西。一旦你理解了这是什么以及它的作用，一切就会突然变得显而易见。噢，编写它仍然不是一件容易的事，但是想法很简单。您只需要编写实际的代码即可。如果我十二岁时就知道解析器，那么也许我就不会花两个小时盯着空白屏幕了。

我怀疑 Djinn 所做的事情从根本上来说很简单，但我遗漏了一些重要的细节，这些细节解释了所有这些复杂的逻辑体操如何与 Haskell 源代码相关......

Answer 1

Djinn 是一个定理证明者。看来你的问题是:定理证明与编程有什么关系？

强类型编程与逻辑有着非常密切的关系。特别是，ML传统中的传统函数式语言与Intuitionist密切相关。 Propositional Logic 。

口号是“程序就是证明，程序证明的命题就是它的类型。”
一般来说你可以想到

 foo :: Foo

表示foo是公式Foo的证明。例如类型

 a -> b  

对应于从a到b的函数，所以如果你有a的证明和a ->的证明b 你有一个b 的证明。因此，函数与逻辑中的蕴涵完全对应。同样

(a,b)

对应于连词(逻辑与)。因此，逻辑重言式 a -> b -> a & b 对应于 Haskell 类型 a -> b -> (a,b) 并有证明:

\a b -> (a,b)

这是“和介绍规则” 而fst::(a,b) -> a和snd::(a,b) -> b则对应了2个“和消除规则”

类似地，a OR b 对应于 Haskell 类型Either a b。

此对应关系有时被称为“Curry-Howard 同构”或“Curry-Howard Correspondence”之后的“Haskell Curry”和 William Alvin Howard

这个故事由于 Haskell 中的非整体性而变得复杂。

Djinn“只是”一个定理证明者。

如果您有兴趣尝试编写克隆，“简单定理证明器”的 Google 结果第一页有 this论文描述了为 LK 编写一个似乎是用 SML 编写的定理证明器。

编辑: 至于“如何证明定理可能？”答案是，从某种意义上来说，这并不难。这只是一个搜索问题:

考虑重述的问题:我们有一组知道如何证明 S 的命题，以及一个我们想要证明 P 的命题。我们该怎么办？ 首先，我们问:我们是否已经有了 S 中 P 的证明？如果是这样，我们可以使用它，如果不是，我们可以在 P 上模式匹配

case P of
   (a -> b) -> add a to S, and prove b (-> introduction)
   (a ^ b)  -> prove a, then prove b (and introduction)
   (a v b)  -> try to prove a, if that doesn't work prove b (or introduction)

如果这些都不起作用

for each conjunction `a ^ b` in S, add a and b to S (and elimination)
for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination)
for each implication `a -> P` is S, try proving `a` (-> elimination)

真正的定理证明者有一定的聪明才智，但想法是一样的。 “决策程序”的研究领域研究了为某些保证有效的公式寻找证据的策略。另一方面，“策略”着眼于如何以最佳方式排序证明搜索。

关于:“如何将证明转化为 Haskell？”

正式系统中的每个推理规则都对应于一些简单的 Haskell 构造，因此如果你有一棵推理规则树，你就可以构造一个相应的程序——Haskell 毕竟是一种证明语言。

含义介绍:

\s -> ?

或者介绍

Left
Right

及介绍

\a b -> (a,b)

并消除

fst
snd

等等

augustss 在他的回答中说，他们在 Djinn 中实现这一点的方式对于 SO 答案来说有点乏味。但我敢打赌，您可以自己弄清楚如何实现它。