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！
2 番目のケース: と仮定しe = (Add x y)ます。それからcomp (Add x y) = comp x ++ comp y ++ [ADD]。
しかし今、私はこのcompの再帰的な使用に苦労しています。これを証明するために、何らかの形のツリーとこれらのツリーの帰納法を使用する必要がありますか? その方法が完全にはわかりません。