等式推論を使用してこのハスケルコードを証明する方法

Question

この演習は、ハスケルでの等式推論と証明に当てはまりました。次のコードが与えられます：

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の関数定義を使用してexec ([PUSH n]) s = exec [] (n:s) = (n:s)が見つかりました。最初のケースはOKです！

第2の場合：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 

あなたが取ることができる。すなわち、命題はcodes成立することを前提としてもらう誘導ステップで：

exec codes s = eval codes : s 

任意の値s - これは通常、誘導証明の重要なステップです。

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

あなたは帰納法の仮定を使用する場所を見ることができます：あなたはexecのために書かれたコードを使用して1位を拡大することにより

は

スタート？