如何在Liquid Haskell中编写log2函数 [英] How to write a log2 function in Liquid Haskell

问题描述

我正在尝试从书中学习Liquid Haskell. 为了测试我的理解，我想编写一个函数log2，该函数采用2 ^ n形式的输入并输出n.

I am trying to learn Liquid Haskell from the book. To test my understanding, I wanted to write a function log2 which takes an input of the form 2^n and outputs 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)

但是在执行此代码时会发生一些奇怪的错误，即优化中的排序错误".我无法理解并解决此错误.

But some strange error occurs while executing this code, namely "Sort Error in Refinement". I am unable to understand and resolve this error.

任何帮助将不胜感激.

摘自Liquid Haskell书:

From the Liquid Haskell book:

谓词是原子谓词，可以通过比较 两个表达式，或者将谓词函数应用于列表 争论...

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是原子二进制关系(而功能只是特殊的一种关系).

In the Liquid Haskell logic syntax, one of the allowed predicates are: e r e where r is an atomic binary relation (and functions are just special kind of relations).

此外，在本教程中，他们将Even子类型定义为: {-@ type Even = {v:Int | v mod 2 == 0 } @-}

Also, in the tutorial, they define the Even subtype as: {-@ type Even = {v:Int | v mod 2 == 0 } @-}

基于此，我认为elem应该可以工作.

Based on that, I thought elem should work.

但是，正如@ ThomasM.DuBuisson所指出的那样，我考虑改为编写自己的elem'，以避免造成混乱.

But now as @ThomasM.DuBuisson pointed out, I thought of writing my own elem' instead, so as to avoid confusion.

elem' :: Int -> [Int] -> Bool
elem' _ [] = False
elem' e (x:xs)
 | e==x = True
 | otherwise = elem' e xs

据我所知，现在要能够将此elem'用作谓词功能，我需要将其提升为度量.因此，我添加了以下内容:

Now, as far as I understand, to be able to use this elem' as a predicate function, I need to lift it as measure. So I added the following:

{-@ measure elem' :: Int -> [Int] -> Bool @-}

现在，在Powers的类型定义中，我用elem'替换了elem.但是我仍然遇到与上一个相同的错误.

Now I replaced elem by elem' in type definition of Powers. But I still get the same error as the previous one.

推荐答案

@TomMD是指反射"的概念，它使您可以将Haskell函数(在某些限制下)转换为精化形式，例如看到这些帖子:

@TomMD is referring to the notion of "reflection" which lets you convert Haskell functions (under some restrictions) into refinements, e.g. see these posts:

https://ucsd-progsys.github.io/liquidhaskell -blog/tags/reflection.html

不幸的是，还没有使用本资料更新本教程.

Unfortunately haven't gotten around to updating the tutorial with this material yet.

因此，例如，您可以如下所示描述log2/pow2:

So for example, you can describe log2/pow2 as shown here:

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)

然后您可以在编译时检查"以下各项是否正确:

You can then "check" at compile time that the following are true:

test8 :: () -> Int
test8 _ = log2 8 === 3

test16 :: () -> Int
test16 _ = log2 16 === 4

test3 :: () -> Int
test3 _ = pow2 3 === 8

test4 :: () -> Int
test4 _ = pow2 4 === 16 

但是，类型检查器将拒绝以下内容

However, the type checker will reject the below

test8' :: () -> Int
test8' _ = log2 8 === 5     -- type error

最后，您可以证明关于log2和pow2

Finally, you can prove the following theorem relating log2 and pow2

{-@ thm_log_pow :: n:Nat -> { log2 (pow2 n) == n } @-}

证明"是通过对n的归纳"来表示的，

The "proof" is by "induction on n", which means:

thm_log_pow :: Int -> () 
thm_log_pow 0 = ()
thm_log_pow n = thm_log_pow (n-1)

回到您的原始问题，您可以将isPow2定义为:

Returning to your original question, you can define isPow2 as:

{-@ 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) 

您可以通过验证以下内容来测试"它是否正确:

and you can "test" it does the right thing by verifying that:

testPow2_8 :: () -> Bool
testPow2_8 () = isPow2 8 === True 

testPow2_9 :: () -> Bool
testPow2_9 () = isPow2 9 === False 

最后，通过为pow2提供精确类型:

and finally, by giving pow2 the refined type:

{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> {v:Nat | isPow2 v} @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)

希望这会有所帮助！

这篇关于如何在Liquid Haskell中编写log2函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！