循环的大步语义，我不断得到一个无限循环答案

【问题标题】：big step semantics for loop, I keep getting an infinite loop循环的大步语义，我不断得到一个无限循环
【发布时间】：2013-03-19 20:24:52
【问题描述】：

虽然这只是代码的一部分，但能否解释一下我为什么会出现无限循环这就是大步语义的样子

eval (For iexp c, s)
    |(bEval (Compare Leq iexp (IConst 0), s)) = s
    |otherwise = eval (For n' c, s')
    where
        s' = eval(c,s)
        n' = (IBin Minus iexp (IConst 1))

【问题讨论】：

bEval (Compare Leq iexp (IConst 0), s) 周围的括号不是必需的（并且会混淆我的心理解析器；-)）。有更多的非惯用括号和缺少的空格。

标签： haskell for-loop semantics infinite-loop

【解决方案1】：

无限循环很可能来自代码的不同部分。您提供的 sn-p 看起来是正确的，并且 - 适当地模拟了必要的类型和函数 - 终止。

也许您没有正确评估减法？另一种可能是bEval 不能正常工作。

这是Data.Trace 的一个很好的用例，它提供了一个用于调试的trace 函数。这就像使用 print 语句以任何其他语言进行调试一样。（在内部，它使用unsafePerformIO。）

trace 函数接受一个字符串和一个表达式；它打印字符串并返回表达式。还有一个traceShow 函数，它在打印之前在其参数上使用show。

您可以使用它在循环执行时打印出中间值。我建议是这样的：

eval (For iexp c, s)
  | condition `traceShow` condition = s
  | otherwise = n' `traceShow` eval (For n' c, s')
  where condition = bEval (Compare Leq iexp (IConst 0), s)
        s' = eval(c,s)
        n' = (IBin Minus iexp (IConst 1))

这将在每一步打印出计数器的条件和值。这应该可以帮助您找出循环的来源。如果没有，您可以移动跟踪语句，使用方式与我在这里相同。

【讨论】：