Докажите распределительный закон умножения над функциями сложения в Haskell

В настоящее время я прохожу курс для начинающих по хаскелю и лямбда-исчислению, и я не знаю, как выполнить следующее упражнение:

Используя следующие определения операций (+) и (*) в haskell, докажите:

1) Закон распределения (*) над (+)

(∀m⇓,n⇓,k⇓::N) (m+n) * k = m * k + n * k

Определения:

(+) :: N -> N -> N
(+) = \m n -> case m of { 0 -> n; S(y) -> S(y+n)}

(*) :: N -> N -> N
(*) = \m n -> case m of { 0 -> 0; S y -> n + (y*n)}

Моя идея состояла в том, чтобы сделать то же, что и в предыдущем упражнении, доказать для каждого возможного случая m. Разница в том, что упражнение, которое я сделал, было для логического типа, который может быть только истинным или ложным, и это естественно, поэтому я решил провести доказательство для случаев m = 0 и m = S(y).

Мне легко удалось доказать равенство для m = 0, но я застрял, делая это для m = S(y)

Случай m = 0

(0 + n) * k =? 0 * k + n * k
Left side:
(0 + n) * k = (case 0 of {0->n;Sy->...}) * k
= n * k
Right side:
0 * k + n * k = (case 0 of {0->0;Sy->...}) + (n * k)
= 0 + (n * k) = (case 0 of {0->(n*k);Sy->...}) = n * k (equal to the left side)

Случай m = S(y)

(Sy + n) * k =? Sy * k + n * k
Left side:
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k
= case Sx of {0->...;Sx-> k + k * (y+n)
Right side:
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k
= k + k*y + n * k (Point at which I got stuck)

(...) Обозначает нерелевантный код

Побочный вопрос: что именно означает стрелка вниз ⇓ на ∀m⇓? Заранее спасибо!


functional-programming haskell lambda-calculus
person Chapi    schedule 01.10.2016    source источник
comment
Расскажите, что вы делали и где именно застряли.   -  person leftaroundabout    schedule 02.10.2016
comment
@leftaroundabout Конечно, только что добавил часть для m = 0 и в настоящее время добавляю свою попытку для m = Sy   -  person Chapi    schedule 02.10.2016
comment
Стрелка ⇓, вероятно, означает: для каждого конечного, не нижнего значения. Учтите, что в Haskell вы можете определить: n :: Nat; n = S n, что является бесконечным числом. А также: loop :: Nat; loop = loop, которое является расходящимся вычислением типа Nat. Если вы подставите такие значения в это уравнение, уравнение может не выполняться.   -  person Bakuriu    schedule 02.10.2016
comment
Спасибо, @Bakuriu, на самом деле это было мое предположение, не нижнее значение, но я не был уверен, спасибо, что прояснили это!   -  person Chapi    schedule 02.10.2016

Ответы (1)


arrow_upward
0
arrow_downward

Ну, вы просто забываете применить индуктивную гипотезу:

(Sy + n) * k =? Sy * k + n * k
Left side:
(case Sy of {0->...;Sy->S(y+n)}) * k = S(y+n) * k
= case Sx of {0->...;Sx-> k + k * (y+n)
( inductive hypothesis; we know that k * (y+n) = k*y + k*n)
= k + k*y + k*n
Right side:
Sy * k + n * k = (case Sy of {0->...;Sy->k + k*y}) + n * k
= k + k*y + n * k

Помните: вы устанавливали индукцией по первому аргументу +, что (m+n)*k == m*k + n*k. Вы доказали базовый случай (0+n)*k, поэтому при доказательстве индуктивного случая вы предполагаете, что знаете, что (y+n)*k == y*k + n*k до определенного значения y, и хотите доказать, что (S(y) + n)*k == S(y)*k + n*k.

person Bakuriu    schedule 02.10.2016
comment
Большое спасибо, я думаю, что причина, по которой я не подумал об этом раньше, заключается в том, что я никогда не собирался использовать индукцию в первую очередь. Но да, работает отлично, еще раз спасибо - person Chapi; 03.10.2016