Насколько безопасна хорошо обоснованная рекурсия?

В вопросе о непрекращении с пунктами, скрывающими прекращение, в ответе предлагается обратиться к <-wellFounded.

Я смотрел определение <-wellFounded раньше, и мне показалось, что в OPTIONS есть --safe. Это должно работать без этой опции? То есть используется --safe некоторая оптимизация или решается какая-то фундаментальная проблема? Значит, в этом случае мы просто делегируем задачу завершения функции, помеченной как «безопасная»?


agda non-termination
person Sassa NF    schedule 13.11.2019    source источник
comment
Вам следует взглянуть (возможно, вы уже это сделали) на следующую вики-страницу, которая объясняет, что означает безопасность: agda.readthedocs.io/en/v2.6.0.1/language/safe-agda.html. Насколько я понимаю, лучше, чтобы функция находилась в безопасном контексте (очевидно), потому что небезопасные прагмы и тому подобное не принимаются внутри модуля, в котором она определена, или любого импортированного модуля. Имеет смысл отмечать прочную основу как безопасную, потому что это противоречит обоснованности доказательств и тому подобного.   -  person MrO    schedule 14.11.2019
comment
@MrO обоснованность ни на что не влияет. Это простая и ванильная Agda, использующая только основные функции, которые были доступны с давних времен.   -  person András Kovács    schedule 14.11.2019
comment
@ AndrásKovács Ofc, я не это имел в виду, извините, если я не совсем понял. Я имел в виду, что, поскольку обоснованность имеет дело с увольнением, если допустить, что это небезопасно, то это может привести к несоответствиям. Надеюсь, на этот раз моя точка зрения будет яснее!   -  person MrO    schedule 14.11.2019
comment
Обоснованность не имеет особых особенностей в отношении завершения, и большая часть стандартной библиотеки в любом случае засыпана --safe.   -  person András Kovács    schedule 14.11.2019
comment
@ AndrásKovács Спасибо. Я действительно видел хорошо обоснованное определение нескольких вещей, которые явно прекращались, но это не всегда показатель того, что это очевидно для Agda. Есть дополнительный вопрос: stackoverflow.com/questions/58899323/   -  person Sassa NF    schedule 17.11.2019

Ответы (1)


arrow_upward
4
arrow_downward

Это совершенно безопасно. --safe устанавливает для модуля более строгий стандарт, чем по умолчанию. Это не означает, что что-то небезопасно, это означает, что что-то безопасно. Использование хорошо обоснованной рекурсии из любого модуля, безопасного или нет, не приведет к незавершению. Завершение довольно сильно встроено в индуктивное определение доступности.

person András Kovács    schedule 13.11.2019