4

我写了一些代码在 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`

那么反映递归函数的正确方法是什么？我已经阅读了液体 haskell 教程，但我无法弄清楚它的示例有什么不同。

4

1 回答 1

2

在没有更多上下文的情况下确定要做什么有点困难，但inline确实不适用于递归函数：inline允许您通过在编译时扩展它来使用类型中的函数（在创建发送到求解器的验证条件之前)，因此需要可以ordLT a b用某些特定的逻辑公式替换每次出现的 （这是不可能的，因为它是递归的）。

如果您需要能够在逻辑中使用任意 Haskell 函数，您可以考虑使用 Refinement Reflection。{-@ reflect ordLT @-}您的示例使用and编译{-@ LIQUID "--exact-data-cons" @-}。但是，通过细化反射创建的功能符号不会在逻辑中自动完全解释。本文讨论了具体细节，这些幻灯片和这篇博文中提供了更易于理解的示例/解释。要记住的要点是，ordLT由反射创建的符号最初将被视为逻辑中完全未解释的函数：LH 唯一知道的就是类似的东西a0 == a1 ==> b0 == b1 ==> ordLT a0 b0 == ordLT a1 b1（如果你在相同的输入上调用它，结果是相同的） .

为了ordLT在逻辑中做一些有用的事情，您需要ordLT在范围内的某个地方调用值级别，这将显示该特定调用的值，因为ordLT（值级别函数）的返回类型断言了一些关于这些输入上的ordLT（逻辑级未解释函数）的输出。上面链接的幻灯片和论文中给出了示例。我希望这足以让你开始！

于 2018-11-22T18:49:05.110 回答