Как написать функцию log2 в Liquid Haskell - PullRequest
Новая
       21

Как написать функцию log2 в Liquid Haskell

3 голосов
/ 11 ноября 2019

Я пытаюсь выучить 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)

Нопри выполнении этого кода возникает странная ошибка, а именно «Ошибка сортировки при уточнении». Я не могу понять и устранить эту ошибку.

Любая помощь будет очень признательна.

РЕДАКТИРОВАТЬ: Из книги Liquid Haskell:

Предикат либоатомарный предикат, полученный путем сравнения двух выражений или применения функции предиката к списку аргументов ...

В логическом синтаксисе 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 @-}

Теперь я заменил elem на elem' в определении типа Powers. Но я все равно получаю ту же ошибку, что и предыдущая.

1 Ответ

4 голосов
/ 13 ноября 2019

@ TomMD относится к понятию «отражение», которое позволяет вам преобразовывать функции Haskell (с некоторыми ограничениями) в уточнения, например, см. Следующие сообщения:

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

К сожалению, пока не удосужились обновить учебник этим материалом.

Так, например, вы можете описать log2 /pow2, как показано здесь:

https://ucsd -progsys.github.io / liquidhaskell-blog / tags / absolute.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)

Затем вы можете "проверить" во время компиляции, что верно следующее: 

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 } @-}

«Доказательством» является «индукция по 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)

и вы можете "проверить" егоделает правильные вещи, проверяя, что: 

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)

Надеюсь, это поможет!

...