1
Я пытаюсь определить функцию Sum f k, суммирующий f от 0 до к-1, такие, чтоОшибка: «Non-конструктор шаблон не допускается в последовательном режиме» (Isabelle)
Sum f k = f 0 + ⋯ + f (k - 1).
Я определил его следующим образом:
fun Sum :: "(nat => nat) => nat => nat" where
"Sum f 1 = f 0"
| "Sum f k = f (k-1) + Sum f (k-1)"
Однако это дает следующее сообщение об ошибке:
Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀f. Sum f 1 = f 0
Это сообщение об ошибке исчезает, когда я определяю Sum f 0 = f 0, но это не функция, которую я пытаюсь определить. Я также могу использовать function и дать доказательства устойчивости, но я был бы очень удивлен, если бы это было необходимо
Может ли кто-нибудь объяснить сообщение об ошибке и порекомендовать обходное решение/исправление?
Спасибо, я последовал твоему совету, но теперь у него есть «незавершенные подцели». Я ожидаю, что это означает, что мне нужно использовать 'function' вместо этого, хотя я бы предпочел не делать этого. – IIM
Хорошо, я попробовал 'fun Sum ::" (nat => nat) => nat => nat "где " Sum f 0 = 0 " | «Сумма f (Suc k) = f k + Sum f k", и это, казалось, сработало! Я предполагаю, что он должен быть «Сук» повсюду (и теперь «базовый случай» имеет больше смысла). – IIM
У вас есть незавершенные подцели, потому что ваше исходное определение не завершилось: 'Sum f 0 = f (0-1) + Sum f (0-1) = f 0 + Sum f 0 = ...'. Добавив случай для 0, исправьте это. – peq