2

我在 Haskell 中找到了这个关于等式推理和证明的练习。给出以下代码：

type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
deriving (Show)
--
-- Stack machine
--
exec :: Code -> Stack -> Stack
exec [ ] s = s
exec (PUSH n : c) s = exec c (n:s)
exec (ADD:c) (m:n:s) = exec c (n+m : s)
--
-- Interpeter
--
data Expr = Val Int | Add Expr Expr
deriving (Show)
eval :: Expr -> Int
eval (Val n) = n
eval (Add x y) = eval x+eval y
--
-- Compiler
--
comp :: Expr -> Code
comp (Val n) = [PUSH n]
comp (Add x y) = comp x ++ comp y ++ [ADD]

现在我必须证明这一点exec(comp e) s = eval e : s。

所以到目前为止我找到了这个答案：

我们必须证明这一点exec (comp e) s = eval e : s。

第一种情况：假设e = (Val n). 那么comp (Val n) = [PUSH n]，所以我们要证明这一点exec ([PUSH n]) s = eval ([PUSH n] : s)。我们发现exec ([PUSH n]) s = exec [] (n:s) = (n:s)使用exec的函数定义。

现在eval (Val n) : s = n : s。第一种情况OK！

第二种情况：假设e = (Add x y). 然后comp (Add x y) = comp x ++ comp y ++ [ADD]。

但现在我正在努力解决这种递归使用 comp 的问题。我应该在这些树上使用某种形式的树和归纳法来证明这一点吗？我不完全确定该怎么做。

4

1 回答 1

3

当第一个参数exec是一个列表时，两种可能性是：

exec (PUSH n: codes)  -- #1
exec (ADD   : codes)  -- #2

在归纳步骤中，您可以假设命题适用于codes，即您可以假设：

exec codes s = eval codes : s

对于s的任何值——记住这一点——这通常是任何归纳证明中的关键步骤。

首先使用您编写的代码扩展#1 exec：

exec (PUSH n: codes) s == exec codes (n:s)
                       == ...
                       == ...
                       == eval (PUSH n: codes) : s

你能找到使用归纳假设的地方吗？

于 2016-05-31T14:47:26.777 回答