haskell - 如何使用等式推理证明此 Haskell 代码

Question

我在 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 的递归使用。我应该使用某种形式的树并对这些树进行归纳来证明这一点吗？我不完全确定如何做到这一点。

Answer 1

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

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

在归纳步骤中，您可以假设该命题适用于代码，即您可以假设:

exec codes s = eval codes : s

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

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

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

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