Djinn是如何工作的？

Question

好的,所以我意识到我可能会在余生中后悔,但...... Djinn实际上是如何工作的？

文档说它使用的算法是"LJ的扩展",并指出了一篇关于LJT的长篇令人困惑的论文.就我所知,这是一个非常复杂的高度形式化规则系统,用于确定哪些逻辑陈述是真是假.但是,这甚至没有开始解释如何将类型签名转换为可执行表达式.据推测,所有复杂的形式推理都是以某种方式涉及的,但这种情况至关重要.

---

这有点像我在BASIC写一个Pascal解释器的时候.(不要笑!我只有十二岁......)我花了好几个小时试图解决它,最后我不得不放弃.我只是无法弄清楚你是如何从包含整个程序的巨型字符串中得到的,以及你可以与已知程序片段进行比较以确定实际操作的内容.

答案当然是你需要写一个叫做"解析器"的东西.一旦你理解了它是什么以及它做了什么,突然一切都变得明显.哦,编码它仍然不是一件容易的事,但这个想法很简单.你只需要编写实际的代码.如果我在十二岁时就知道解析器,那么也许我不会花两个小时只是盯着一个空白的屏幕.

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

Answer 1

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

强类型编程与逻辑关系非常密切.特别是,ML传统中的传统功能语言与直觉 主义命题逻辑密切相关.

口号是"程序是证明,程序证明的是它的类型".
一般来说,你可以想到

 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.

在Haskell Curry和William Alvin Howard之后,这种对应关系有时被称为"Curry-Howard Isomorphism"或" Curry-Howard Correspondence ".

Haskell中的非整体性使这个故事变得复杂.

Djinn"只是"一个定理证明者.

如果你有兴趣尝试写一个克隆,谷歌结果的"简单的定理证明"的第一页有这个文件,该文件描述了写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

等等

奥古斯丁在他的回答中说,他们在Djinn实施这一点的方式对于SO答案来说有点单调乏味.我敢打赌,你可以自己想一想如何实现它.

Answer 2

在最一般的术语中,根据库里 - 霍华德的同构,类型和命题之间存在对应关系,也存在价值和证据.Djinn使用这种信件.

更具体一点,比如说你想要找到一个类型的Haskell术语(a, b) -> (b, a).首先,您将类型转换为逻辑中的语句(Djinn使用命题逻辑,即没有量词).逻辑声明说(A and B) is true implies (B and A) is true.下一步是证明这一点.对于命题逻辑,总是可以机械地证明或反驳陈述.如果我们可以反驳它,那么这意味着在(终止)Haskell中不会有相应的术语.如果我们可以证明它,那么就有一个类型的Haskell术语,而且,Haskell术语与证明具有完全相同的结构.

最后的陈述必须是合格的.您可以选择使用不同的公理和推理规则来证明该陈述.如果你选择一个建设性的逻辑,证明和Haskell术语之间只有一个对应关系."正常",即经典逻辑具有像A or (not A)公理一样的东西.这将对应于Haskell类型Either a (a -> Void),但是没有这种类型的Haskell术语,所以我们不能使用经典逻辑.任何命题陈述都可以在建设性命题逻辑中得到证实或证明,但这种做法与经典逻辑相比更为复杂.

因此,回顾一下,Djinn通过将类型转换为逻辑中的命题来工作,然后它使用建构逻辑的决策过程来证明命题(如果可能的话),最后证明被转换回Haskell术语.

(在这里说明这是如何工作太痛苦了,但是在白板上给我10分钟,你会很清楚.)

作为最后的评论供你思考:Either a (a -> Void)如果你有方案,可以实施call/cc.选择一个更具体的类型,Either a (a -> Int)并弄清楚如何.