방정식 추론을 사용하여 하스켈 코드를 증명하는 법

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)을 찾습니다.

지금 eval (Val n) : s = n : s. 첫 번째 경우는 OK입니다!

두 번째 경우 : e = (Add x y)이라고 가정합니다. 그 다음 comp (Add x y) = comp x ++ comp y ++ [ADD].

하지만 이제는 comp의 재귀 적 사용에 어려움을 겪고 있습니다. 내가 이것을 증명하기 위해 어떤 형태의 나무와 유도를 사용해야합니까? 나는 그것을하는 방법을 완전히 모르겠습니다. exec에 첫 번째 인수가리스트 인 경우

Answer 1

, 두 가지 가능성이있다 : 당신이 제안이 codes을 위해 보유하고 있다고 가정 할 수 유도 단계에서

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

, 당신은 가정 할 수있다, 즉 :

exec codes s = eval codes : s 

임의의 값은 s입니다. 이는 일반적으로 모든 유도 증명의 핵심 단계입니다.

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

당신이 유도 가설을 사용하는 장소를 볼 수 : 당신이 exec 위해 작성한 코드를 사용하여 # 1을 확장하여

는

시작?