У меня определение Изабель / HOL выглядит как
definition "f1 args = filter g (f0 args)",
, где f0 возвращает список (хотя эта деталь не особенно важна).
Теперь, если я попытаюсь вычислить
value "f1 args0",
для заданного значения c args0, это медленнее, чем
value "f0 args0"
definition "f0args0 = <content pasted from the results obtained above>"
value "filter g f0args0"
Когда у меня есть большое количество вложенных определений (скажем, f (n + 1), чьи определения зависят от f (n), f (n-1), ..., f0), эта проблема становится невыносимой: если я попробую вычисление с использованием f (n + 1), оно никогда не прекратится, а если я разделю вручную Вычисления, как указано выше, передавая выходные данные f (j) в f (j + 1) путем копирования и вставки, будут.
Тем не менее, это невыносимая работа для даже умеренно больших значений n.
Могу ли я что-нибудь сделать с этим? Или это фундаментальное ограничение функционального программирования? (Я говорю это, потому что с помощью копирования / вставки выше, я думаю, формально вводит побочные эффекты)
Спасибо!