Блог

Я знаю, что на подобные вопросы, похоже, смотрят свысока, но я не смог найти ответы в Интернете. У меня есть следующая функция:

 fun count :: "'a ⇒ 'a list ⇒ nat" where
  "count a [] = 0"
| "count a (b # xs) = (count a xs)   (if a = b then 1 else 0)"
 

Он подсчитывает количество элементов в списке, которые соответствуют данному элементу. Однако достаточно просто, когда я делаю следующее:
value "count x [x,x,y,x,y]"

Я получаю это как результат

"(if x = y then 1 else 0) 1 (if x = y then 1 else 0) 1 1" :: "nat"

Таким образом, вы можете видеть, что в выходных данных есть зависшие операторы «if» и недооцененные дополнения. Можно ли заставить Изабель упростить это?

Я так не думаю. value Команда является скорее чисто диагностическим инструментом и в основном предназначена для оценки основных терминов (т. Е. Без свободных переменных). Причина, по которой вы вообще получаете результат, заключается в том, что он отступает от своего стандартного метода (компиляция в ML, запуск кода ML и преобразование результата обратно в термины HOL) в NBE (нормализация путем оценки, которая намного медленнее и, по крайней мере, по моему опыту, не так полезнавремени).

Один трюк, который я иногда делаю, — это установить лемму

 lemma "count x [x, x, y, x, y] = myresult"
 

где myresult в правой части это просто фиктивная переменная. Тогда я делаю

 apply simp
 

и посмотрите на результирующее состояние проверки (если вы ничего не видите: попробуйте включить «Состояние вывода редактора» в настройках):

 proof (prove)
goal (1 subgoal):
 1. (x = y ⟶ Suc (Suc (Suc (Suc (Suc 0)))) = myresult) ∧
    (x ≠ y ⟶ Suc (Suc (Suc 0)) = myresult)
 

Это немного запутанно, но вы можете довольно хорошо прочитать результат: если x = y , то результат равен 5, в противном случае это 3. Простой способ избавиться от Suc в выводе — это привести к int , т. е. lemma "int (count x [x, x, y, x, y]) = myresult" . Тогда вы получаете:

 (x = y ⟶ myresult = 5) ∧ (x ≠ y ⟶ myresult = 3)