Wie man diesen Haskell-Code unter Verwendung von Gleichargumentation beweisen kann

Question

Ich fand diese Übung über Gleichargumentation und Beweise in Haskell. Der folgende Code ist gegeben:

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] 

Jetzt muss ich, dass exec(comp e) s = eval e : s beweisen.

So fand ich diese Antwort so weit:

wir, dass exec (comp e) s = eval e : s beweisen.

Erster Fall: Angenommen e = (Val n). Dann comp (Val n) = [PUSH n], so müssen wir beweisen, dass exec ([PUSH n]) s = eval ([PUSH n] : s). Wir finden das exec ([PUSH n]) s = exec [] (n:s) = (n:s) mit der Funktionsdefinition von exec.

Jetzt eval (Val n) : s = n : s. Der erste Fall ist OK!

Zweiter Fall: angenommen e = (Add x y). Dann comp (Add x y) = comp x ++ comp y ++ [ADD].

Aber jetzt kämpfe ich mit dieser rekursiven Verwendung von comp. Sollte ich eine Form von Bäumen und Induktion auf diesen Bäumen verwenden, um dies zu beweisen? Ich bin mir nicht ganz sicher, wie ich das machen soll.

Answer 1

Wenn das erste Argument exec eine Liste ist, sind die beiden Möglichkeiten sind:

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

Im Induktionsschritt Sie davon ausgehen, bekommen, dass der Satz für codes hält, dh man annehmen kann:

exec codes s = eval codes : s 

für beliebig Wert von s - Denken Sie daran - dies ist in der Regel der wichtigste Schritt in jedem Induktionsbeweis.

Starten von # 1 mit dem Code erweitern Sie exec geschrieben haben:

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

Können Sie sich einen Platz finden Sie in der Induktionsvoraussetzung zu benutzen?