Неверное определение: нелинейные шаблоны не допускаются в последовательном режиме - PullRequest
Новая
       10

Неверное определение: нелинейные шаблоны не допускаются в последовательном режиме

3 голосов
/ 16 марта 2019

Я определил следующую функцию: 

fun count:: "'a ⇒ 'a list ⇒ nat" where
"count a Nil = 0" |
"count a (Cons b xs) = (count a xs)" |
"count a (Cons a xs) = (count a xs) + (Suc 0)"

Должен подсчитывать количество вхождений элемента a в списке с элементами одного типа с a.Я получаю следующую ошибку: 

Malformed definition:
Nonlinear patterns not allowed in sequential mode.
⋀a xs. count a (a # xs) = count a xs + Suc 0

1 Ответ

4 голосов
/ 16 марта 2019

В отношении шаблонов «линейный» означает, что каждая свободная переменная встречается только один раз . В третьей строке шаблон с левой стороны содержит a дважды, что делает его нелинейным. Это не поддерживается «последовательным» режимом пакета функций. Это режим, в котором вы можете указывать, возможно, перекрывающиеся функциональные уравнения одно за другим, и первое, которое соответствует, является тем, которое считается. Это также режим, который использует команда «fun» и который обычно используют функциональные языки программирования, такие как Haskell (обратите внимание, что они также обычно не допускают нелинейных шаблонов).

У вас есть две возможности: если вы абсолютно хотите использовать нелинейные шаблоны, вы можете написать 

function count:: "'a ⇒ 'a list ⇒ nat" where
  "count a Nil = 0"
| "a ≠ b ⟹ count a (Cons b xs) = (count a xs)"
| "count a (Cons a xs) = (count a xs) + (Suc 0)"
  by (metis neq_Nil_conv surj_pair) auto
termination by lexicographic_order

Обратите внимание, что вы должны показать тот факт, что шаблоны являются исчерпывающими и не перекрываются вручную, а также терминированием. «Веселье» не так мощно, но делает все это автоматически.

Гораздо проще и эффективнее переформулировать свое определение таким образом, который более приемлем для автоматизации системы: 

fun count:: "'a ⇒ 'a list ⇒ nat" where
  "count a Nil = 0"
| "count a (Cons b xs) = (count a xs) + (if a = b then 1 else 0)‹›

Это почти всегда предпочтительнее по разным причинам (короче, проще, лучше работает с генерацией кода).

Для получения дополнительной информации о пакете функций см. Документацию . Это очень мощный и универсальный инструмент, но если вы можете получить то, что вы хотите, только «весело», это обычно так, как вы хотите.

...