Изабелла возвращает номера вместо Suc (Suc (... 0))

Question

Когда я использую value, чтобы узнать какое-то значение функции, которая возвращает натуральные числа, я всегда получаю ответ в виде повторных функций-преемников 0, т.е. Suc(Suc(... 0)), которые иногда трудно читать. Есть ли способ напрямую выводить число, которое возвращает Изабель?

Answer 1

Это то, что я хотел исправить некоторое время назад, но, видимо, я забыл. Угадание Карцигената неверно; это действительно полностью оцененный результат. Проблема в том, что натуральные числа печатаются этим громоздким способом.

Вы можете сделать следующие вещи:

1. Самый простой способ, чтобы преобразовать число в целое, т.е. вместо value "foo x y z" (где foo x y z является выражением типа nat, который вы хотите eavluate) вы напишите value "int (foo x y z)".

2. Вы можете добавить ~~/src/HOL/Library/Code_Target_Numeral в список ваших товаров. Это делает генератор кода Изабеллы использовать целые числа произвольной точности целевого языка (в случае value, это ML и его целые числа на основе GMP) вместо неэффективной нотации преемника. Как побочный эффект, это также печатает натуральные числа в лучшем виде.

3. Вы можете добавить следующий код к вашей теории, которая изменяет способ value команда отображает натуральные числа:

Код:

lemma Suc_numeral_bit0: "Suc (numeral (Num.Bit0 n)) = numeral (Num.Bit1 n)" 
    by (subst Suc_numeral) simp 

lemma Suc_numeral_bit1: "Suc (numeral (Num.Bit1 n)) = numeral (Num.Bit0 (n + Num.One))" 
    by (subst Suc_numeral) simp 

lemmas [code_post] = 
    One_nat_def [symmetric] Suc_numeral_bit0 Suc_numeral_bit1 Num.Suc_1 Num.arith_simps 

Обратите внимание, что команда value является диагностическим только команда. Он в основном используется для быстрых тестов достоверности и отладки настроек генерации кода, и заставить его работать иногда может быть сложным.

По умолчанию value полагается на генератор кода, то есть Isabelle должен знать, как генерировать исполняемый код для выражения, и если он не может этого сделать, value, вероятно, не удастся. (Иногда это может также вернуться к некоторым другим стратегиям, нормализации путем оценки или оценки путем упрощения, но обычно они не дают полезного вывода)

Я просто говорю вам об этом, чтобы вы знали, чего ожидать от value и не создается впечатление, что это неотъемлемая часть Изабель, которую люди используют все время.