如何在 Liquid 中编写 log2 函数 Haskell
How to write a log2 function in Liquid Haskell
我正在尝试从 book 学习 Liquid Haskell。
为了测试我的理解,我想写一个函数 log2
它接受 2^n 形式的输入并输出 n.
我有以下代码:
powers :: [Int]
powers = map (2^) [0..]
{-@ type Powers = {v:Nat | v elem powers } @-}
{-@ log2 :: Powers -> Nat @-}
log2 :: Int -> Int
log2 n
| n == 1 = 0
| otherwise = 1 + log2 (div n 2)
但是在执行这段代码时出现了一些奇怪的错误,即"Sort Error in Refinement"。我无法理解和解决此错误。
任何帮助将不胜感激。
编辑:来自 Liquid Haskell 书:
A Predicate is either an atomic predicate, obtained by comparing
two expressions, or, an application of a predicate function to a list of
arguments...
在 Liquid Haskell 逻辑语法中,允许的谓词之一是:e r e
其中 r
是原子二元关系(函数只是一种特殊的关系)。
此外,在教程中,他们将 Even
子类型定义为:
{-@ type Even = {v:Int | v mod 2 == 0 } @-}
基于此,我认为 elem
应该可行。
但现在正如@ThomasM.DuBuisson指出的那样,我想改为自己编写elem'
,以避免混淆。
elem' :: Int -> [Int] -> Bool
elem' _ [] = False
elem' e (x:xs)
| e==x = True
| otherwise = elem' e xs
现在,据我了解,为了能够将此 elem'
用作谓词函数,我需要将其提升为度量。所以我添加了以下内容:
{-@ measure elem' :: Int -> [Int] -> Bool @-}
现在我在 Powers
的类型定义中用 elem'
替换了 elem
。但我仍然得到与上一个相同的错误。
@TomMD 指的是 "reflection" 的概念,它允许您将 Haskell 函数(在某些限制下)转换为细化,例如查看这些帖子:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
遗憾的是,还没有抽出时间用这个 material 更新教程。
例如,您可以如下所示描述 log2/pow2:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573673688_378.hs
特别是你可以写:
{-@ reflect log2 @-}
log2 :: Int -> Int
log2 1 = 0
log2 n = 1 + log2 (div n 2)
{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> Nat @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)
然后您可以 "check" 在编译时满足以下条件:
test8 :: () -> Int
test8 _ = log2 8 === 3
test16 :: () -> Int
test16 _ = log2 16 === 4
test3 :: () -> Int
test3 _ = pow2 3 === 8
test4 :: () -> Int
test4 _ = pow2 4 === 16
但是,类型检查器会拒绝以下内容
test8' :: () -> Int
test8' _ = log2 8 === 5 -- type error
最后,你可以证明下面关于log2
和pow2
的定理
{-@ thm_log_pow :: n:Nat -> { log2 (pow2 n) == n } @-}
"proof"是由"induction on n",意思是:
thm_log_pow :: Int -> ()
thm_log_pow 0 = ()
thm_log_pow n = thm_log_pow (n-1)
回到你原来的问题,你可以定义isPow2
为:
{-@ reflect isEven @-}
isEven :: Int -> Bool
isEven n = n `mod` 2 == 0
{-@ reflect isPow2 @-}
isPow2 :: Int -> Bool
isPow2 1 = True
isPow2 n = isEven n && isPow2 (n `div` 2)
你可以 "test" 它通过验证以下内容来做正确的事情:
testPow2_8 :: () -> Bool
testPow2_8 () = isPow2 8 === True
testPow2_9 :: () -> Bool
testPow2_9 () = isPow2 9 === False
最后,通过给 pow2
精炼类型:
{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> {v:Nat | isPow2 v} @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)
希望对您有所帮助!
我正在尝试从 book 学习 Liquid Haskell。
为了测试我的理解,我想写一个函数 log2
它接受 2^n 形式的输入并输出 n.
我有以下代码:
powers :: [Int]
powers = map (2^) [0..]
{-@ type Powers = {v:Nat | v elem powers } @-}
{-@ log2 :: Powers -> Nat @-}
log2 :: Int -> Int
log2 n
| n == 1 = 0
| otherwise = 1 + log2 (div n 2)
但是在执行这段代码时出现了一些奇怪的错误,即"Sort Error in Refinement"。我无法理解和解决此错误。
任何帮助将不胜感激。
编辑:来自 Liquid Haskell 书:
A Predicate is either an atomic predicate, obtained by comparing two expressions, or, an application of a predicate function to a list of arguments...
在 Liquid Haskell 逻辑语法中,允许的谓词之一是:e r e
其中 r
是原子二元关系(函数只是一种特殊的关系)。
此外,在教程中,他们将 Even
子类型定义为:
{-@ type Even = {v:Int | v mod 2 == 0 } @-}
基于此,我认为 elem
应该可行。
但现在正如@ThomasM.DuBuisson指出的那样,我想改为自己编写elem'
,以避免混淆。
elem' :: Int -> [Int] -> Bool
elem' _ [] = False
elem' e (x:xs)
| e==x = True
| otherwise = elem' e xs
现在,据我了解,为了能够将此 elem'
用作谓词函数,我需要将其提升为度量。所以我添加了以下内容:
{-@ measure elem' :: Int -> [Int] -> Bool @-}
现在我在 Powers
的类型定义中用 elem'
替换了 elem
。但我仍然得到与上一个相同的错误。
@TomMD 指的是 "reflection" 的概念,它允许您将 Haskell 函数(在某些限制下)转换为细化,例如查看这些帖子:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
遗憾的是,还没有抽出时间用这个 material 更新教程。
例如,您可以如下所示描述 log2/pow2:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573673688_378.hs
特别是你可以写:
{-@ reflect log2 @-}
log2 :: Int -> Int
log2 1 = 0
log2 n = 1 + log2 (div n 2)
{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> Nat @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)
然后您可以 "check" 在编译时满足以下条件:
test8 :: () -> Int
test8 _ = log2 8 === 3
test16 :: () -> Int
test16 _ = log2 16 === 4
test3 :: () -> Int
test3 _ = pow2 3 === 8
test4 :: () -> Int
test4 _ = pow2 4 === 16
但是,类型检查器会拒绝以下内容
test8' :: () -> Int
test8' _ = log2 8 === 5 -- type error
最后,你可以证明下面关于log2
和pow2
{-@ thm_log_pow :: n:Nat -> { log2 (pow2 n) == n } @-}
"proof"是由"induction on n",意思是:
thm_log_pow :: Int -> ()
thm_log_pow 0 = ()
thm_log_pow n = thm_log_pow (n-1)
回到你原来的问题,你可以定义isPow2
为:
{-@ reflect isEven @-}
isEven :: Int -> Bool
isEven n = n `mod` 2 == 0
{-@ reflect isPow2 @-}
isPow2 :: Int -> Bool
isPow2 1 = True
isPow2 n = isEven n && isPow2 (n `div` 2)
你可以 "test" 它通过验证以下内容来做正确的事情:
testPow2_8 :: () -> Bool
testPow2_8 () = isPow2 8 === True
testPow2_9 :: () -> Bool
testPow2_9 () = isPow2 9 === False
最后,通过给 pow2
精炼类型:
{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> {v:Nat | isPow2 v} @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)
希望对您有所帮助!