我写了一些Haskell代码来进行序数算术,现在正在尝试使用Liquid Haskell验证某些属性。然而,我在“反映”递归函数方面遇到了麻烦。我已经在下面的“小于”函数中分离出了一个问题:
-- (Ord a n b) = a^n + b
{-@ data Ordinal [size] = Ord { a :: Ordinal, n :: Nat, b :: Ordinal }
| Zero {} @-}
data Ordinal = Ord Ordinal Integer Ordinal
| Zero
deriving (Eq, Show)
{-@ measure size @-}
{-@ size :: Ordinal -> Nat @-}
size :: Ordinal -> Integer
size Zero = 1
size (Ord a n b) = (size a) + 1 + (size b)
{-@ inline ordLT @-}
ordLT :: Ordinal -> Ordinal -> Bool
ordLT _ Zero = False
ordLT Zero _ = True
ordLT (Ord a0 n0 b0) (Ord a1 n1 b1) =
(ordLT a0 a1) ||
(a0 == a1 && n0 < n1) ||
(a0 == a1 && n0 == n1 && ordLT b0 b1)
one = (Ord Zero 1 Zero) -- 1
w = (Ord one 1 Zero) -- omega
main = print w -- Ord (Ord Zero 1 Zero) 1 Zero
仅使用上述内容执行liquid ordinals.hs
会出现以下错误:
Error: Cyclic type alias definition for `Main.ordLT`
14 | {-@ inline ordLT @-}
^^^^^
The following alias definitions form a cycle:
* `Main.ordLT`
那么如何正确地反映递归函数呢?我已经阅读了liquid haskell教程,但是我无法弄清楚它的示例与其他示例有何不同。
reflect
,但我还没有多少使用LH的经验。https://github.com/ucsd-progsys/liquidhaskell/blob/develop/README.md - jberryman