Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl)
复制标题
所有人的定理证明：液体 Haskell 中的等式推理（功能性珍珠）
DOI：
10.1145/3242744.3242756
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
G. Hutton
中科院分区：
文献类型：
--
作者：
Niki Vazou;Joachim Breitner;Rose Kunkel;David Van Horn;G. Hutton
等式推理是Haskell等纯函数式语言的关键特性之一。然而，到目前为止，这种推理总是在Haskell外部进行，要么在纸上手动进行，要么在定理证明器中机械化。本文展示了如何在Haskell中直接无缝地执行等式推理，并使用Liquid Haskell进行检查。特别是，语言学习者-对他们来说，外部定理证明器是遥不可及的-可以从机械地检查他们的证明中受益。具体地说，我们展示了如何从格雷厄姆的教科书中的方程证明和推导可以被改写为Haskell中的证明（剧透：它们看起来本质上是一样的）。
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell. In particular, language learners --- to whom external theorem provers are out of reach --- can benefit from having their proofs mechanically checked. Concretely, we show how the equational proofs and derivations from Graham's textbook can be recast as proofs in Haskell (spoiler: they look essentially the same).