gpt4 book ai didi

haskell - LiquidHaskell : failing DeMorgan's law

转载 作者:行者123 更新时间:2023-12-04 17:45:19 27 4
gpt4 key购买 nike

我在用 LiquidHaskell 证明以下定律时遇到了麻烦:

DeMorgan's law

它被称为(之一)德摩根定律,并简单地说明了 or 的否定。两个值必须与 and 相同否定每个。它已经被证明了很长时间,并且是 LiquidHaskell 的 tutorial 中的一个例子。 .我正在学习本教程,但无法通过以下代码:

-- Test.hs
module Main where

main :: IO ()
main = return ()

(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True = True
True ==> True = True
True ==> False = False

(<=>) :: Bool -> Bool -> Bool
False <=> False = True
False <=> True = False
True <=> True = True
True <=> False = False

{-@ type TRUE = {v:Bool | Prop v} @-}
{-@ type FALSE = {v:Bool | not (Prop v)} @-}

{-@ deMorgan :: Bool -> Bool -> TRUE @-}
deMorgan :: Bool -> Bool -> Bool
deMorgan a b = not (a || b) <=> (not a && not b)

运行时 liquid Test.hs ,我得到以下输出:
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE: Parsed All Specifications ******************************************


**** DONE: Loaded Targets *****************************************************


**** DONE: Extracted Core using GHC *******************************************

Working 0% [.................................................................]
Done solving.

**** DONE: solve **************************************************************


**** DONE: annotate ***********************************************************


**** RESULT: UNSAFE ************************************************************


Test.hs:23:16-48: Error: Liquid Type Mismatch

23 | deMorgan a b = not (a || b) <=> (not a && not b)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Inferred type
VV : Bool

not a subtype of Required type
VV : {VV : Bool | Prop VV}

In Context

现在我绝不是 LiquidHaskell 的专家,但我很确定一定是出了什么问题。几年前我已经说服自己该身份成立,但为了确保我使用所有可能的输入调用该函数,并最终运行
λ: :l Test.hs 
λ: import Test.QuickCheck
λ: quickCheck deMorgan
>>> +++ OK, passed 100 tests.

所以我在 Haskell 代码中似乎没有拼写错误,错误必须出在 LiquidHaskell 规范中。 LiquidHaskell 似乎无法推断结果 Bool是严格的 TRUE :
Inferred type
VV : Bool

not a subtype of Required type
VV : {VV : Bool | Prop VV}

我在这里有什么错误?任何帮助表示赞赏!

PS:我正在使用 z3求解器,并运行 GHC 7.10.3。 LiquidHaskell 版本是 2009-15 .

最佳答案

LiquidHaskell 无法证明您的程序安全,因为它没有足够强的类型来支持 (<=>) .我们确实推断函数的类型,但推断是基于程序中的其他类型签名。具体来说,我们需要弄清楚

{-@ (<=>) :: p:Bool -> q:Bool -> {v:Bool | Prop v <=> (Prop p <=> Prop q)} @-}

( Prop 语法是我们将 Haskell Bool 提升为 SMT bool 值的方式。)

为了让 LiquidHaskell 推断出这种类型,它需要看到一个谓词 Prop v <=> (Prop p <=> Prop q)在另一种类型签名中的某处(对于某些 vpq )。这个片段没有出现在任何地方,所以我们需要明确提供签名。

这是 LiquidHaskell 的一个不幸限制,但对于保持可判定性至关重要。

PS:这是您示例的工作版本的链接。
http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1461434240_7574.hs

关于haskell - LiquidHaskell : failing DeMorgan's law,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36813497/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com