Почему функции Изабеллы должны иметь хотя бы один аргумент?

Question

Когда я пытаюсь написать

fun foo :: "nat ⇒ nat" 
where "foo = Suc" 

Isabelle жалуется, что «функция не имеет аргументов». Почему это? Что случилось с fun без аргументов? Я знаю, что я могу изменить fun на abbreviation или definition, и все в порядке. Но, похоже, стыдно испортить единообразие моего файла .thy, в котором каждое другое определение объявлено с fun.

Answer 1

У настоящего поколения fun и function в Isabelle/HOL были особые мнения по этому поводу и, вероятно, также хорошие формальные основания утверждать, что «функция» действительно нуждается в аргументах. В SML у вас действительно есть аналогичная ситуация: «константы» без аргументов определяются через val не fun.

В тех редких случаях, когда функции нулевого аргумента необходимы в Isabelle/HOL, она достаточно проста в использовании definition [simp] "c = t, чтобы получить в основном один и тот же результат, кроме названия основных теорем, произведенных внутри страны: c_def против c.simps.

Я думаю, что главное неудобство и иногда pitfal из function в этом отношении является его воздействием вспомогательной c_def, который не предназначен для использования в приложениях: она раскрывает внутреннюю конструкцию за спецификацией функции, а не ее основное уравнение Характеризуя.

Answer 2

Поскольку никакого другого ответа, похоже, уже на пути, позвольте мне повторить и распространить на мой предыдущий комментарий. В Isabelle/хол существует три способа определения функций:

• definition для не рекурсивных функций (которые могут только быть замечены как константы, которые служат в качестве аббревиатуры для длинных операторов).

• primrec для примитивно-рекурсивных функций (в том смысле, что в каждом рекурсивном вызове существует фиксированный аргумент, в котором удаляется конструктор типа данных).

• fun для общих рекурсивных функций.

И, primrec и fun ожидать, по крайней мере один аргумент. Для первого автоматически проверяется, что один из его аргументов соответствует синтаксическому шаблону примитивной рекурсии по типам данных, в то время как для последней задача доказательства «завершения» (или, скорее, обоснованность графика вызова) будет делегирована пользователь в жестких случаях.

Во всяком случае, это было бы, конечно, можно передать primrec и fun в definition для простых случаев без аргументов, но, по крайней мере, для меня это, скорее, кажется, запутать вещи для пользователя вместо очистки их.