Как доказать этот код 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 ([PUSH n]) s = exec [] (n:s) = (n:s) используя определение функции exec.

Теперь eval (Val n) : s = n : s. Первый случай в порядке!

Второй случай: Предположим, e = (Add x y). Затем comp (Add x y) = comp x ++ comp y ++ [ADD].

Но теперь я борюсь с этим рекурсивным использованием comp. Должен ли я использовать какую-то форму деревьев и индукцию по этим деревьям, чтобы доказать это? Я не совсем уверен, как это сделать.


recursion haskell proof equational-reasoning
person Community    schedule 31.05.2016    source источник
comment
обратите внимание, что вам не хватает одной строки в exec _ [] = error "ADD applied to an empty or singleton stack"   -  person epsilonhalbe    schedule 31.05.2016
comment
Вам, вероятно, понадобится лемма о exec — в частности, у вас есть exec (a ++ b) s = exec b (exec a s). Это позволит вам написать exec (comp x ++ comp y ++ [ADD]) как exec [ADD] (exec (comp y) (exec (comp x)))   -  person user2407038    schedule 31.05.2016
comment
Благодарю вас! Но как мне тогда доказать комп х и комп у?   -  person    schedule 31.05.2016

Ответы (1)


arrow_upward
3
arrow_downward

Когда первым аргументом exec является список, возможны две возможности:

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

На шаге индукции вы можете предположить, что предложение верно для codes, т. е. вы можете предположить:

exec codes s = eval codes : s

для любого значения s — помните об этом — обычно это ключевой шаг в любом доказательстве индукции.

Начните с расширения #1, используя код, который вы написали для exec:

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

Вы видите место, где можно использовать гипотезу индукции?

person ErikR    schedule 31.05.2016