如何使用等式推理來證明這個Haskell代碼

我在Haskell的等式推理和證明中發現了這個練習。以下代碼給出：如何使用等式推理來證明這個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的函數定義exec ([PUSH n]) s = exec [] (n:s) = (n:s)。

現在eval (Val n) : s = n : s。第一種情況是好的！

第二種情況：假設e = (Add x y)。然後comp (Add x y) = comp x ++ comp y ++ [ADD]。

但現在我正在努力使用comp的遞歸使用。我是否應該在這些樹上使用某種形式的樹木和歸納法來證明這一點？我不完全確定如何做到這一點。

來源

2016-05-31 Pieter Verschaffelt

請注意，您在'exec _ [] = error「添加應用於空或單個堆棧時缺少一行'' – epsilonhalbe

您可能需要'exec'的引理 - 特別是您有'exec（a + + b）s = exec b（exec as）'。這將允許您將'exec（comp x ++ comp y ++ [ADD]）'寫爲'exec [ADD]（exec（comp y）（exec（comp x）））' – user2407038

謝謝！但是，我如何證明comp x和comp y呢？ –

當第一個參數exec是一個列表，這兩個可能性：

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

在感應步驟中，您得到的假設，命題成立爲codes，即你可以假設：

exec codes s = eval codes : s

對於任何值s - 記住這一點 - 這通常是任何感應證明中的關鍵步驟。

開始使用你爲exec編寫的代碼擴展＃1：

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

你能看到使用歸納假設的地方嗎？

來源

2016-05-31 14:47:26 ErikR

如何使用等式推理來證明這個Haskell代碼

回答

相關問題