写入符号数组中符号数量的点

Question

我有一个

SArray Integer Integer

，我想向该数组写入

k

次。例如，我想打电话给

writeArray arr 1 10

，

writeArray arr 2 10

，...，

writeArray arr k 10

。但是，当

k

本身具有象征意义时，我不知道该怎么做。这可能吗？

我尝试了一些这样的事情：

import qaulified Data.SBV as S
import qualified Data.SBV.List as S

writeBlock :: S.SArray Integer Integer -> S.SInteger -> S.SInteger -> S.SInteger -> S.SArray Integer Integer
writeBlock arr sz k v =
  let keyVals = S.zip (keyList sz k) (valueList sz v)
  in S.foldl writeArray' arr keyVals
  where
    keyList 0 _ = S.nil
    keyList size key = key S..: keyList (size - 1) (key + 1)

    valueList 0 _ = S.nil
    valueList size value = value S..: valueList (size - 1) value

    writeArray' arr (key, value) = S.writeArray arr key value

失败，因为

SArray

不是

SBV a

。我还尝试使用具体列表，但由于不同的错误而失败。请告诉我是否有任何方法可以做到这一点。谢谢，非常感谢任何帮助。

Answer 1

进行符号编程时，您需要非常小心哪些变量用于控制以及哪些变量用作数据。让您的数据完全具有象征意义是完全可以的。但您希望避免控制流中的符号变量。也就是说，程序的数据流可以完全是象征性的，但控制路径应该（大部分）是具体的。

由于您使用

k

作为控制变量，因此您对其执行的任何类型的递归都将无法终止。想想这样的事情将如何执行：

    valueList 0    _     = S.nil
    valueList size value = value S..: valueList (size - 1) value

这里有两个问题：首先，不能对符号变量使用模式匹配。 （SBV 对此无能为力，Haskell 模式匹配仅适用于具体值；并且有充分的理由。）因此，编写此类内容的“符号”方式将是：

    valueList size value = ite (size .== 0)
                               S.nil
                               (value S..: valueList (size - 1) value)

不幸的是，这也不起作用，因为它无法终止。

ite

构造（if-then-else）不知道递归何时停止，因为

size

是象征性的。

解决此问题的一种方法是知道

size

的具体上限。在这种情况下，您可以使用它来执行有界循环。如果您提前知道这样一个具体的界限，这将是首选解决方案。

您可以在 https://hackage.haskell.org/package/sbv-10.3/docs/src/Documentation.SBV.Examples.CodeGeneration.GCD.html#sgcd 中查看使用上限的示例，其中idea用于象征性地实现GCD。也许你可以使用类似的策略来限制递归深度，使其具体可计算。