Ну вот вы написали, скажем, функцию сортировки и что-то про неё доказали. А что вы дальше с этой функцией делаете?
На этом всё. Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет. Это может быть полезно и в математике, но не в первую очередь.
Мой поинт в том, что бывают случаи, когда вычисляться таки надо.
Мне кажется, что есть какое-то недопонимание. Если все функции не будут вычисляться, то проблемы с termination вообще не будет. В Arend 1.1 появилось новое ключевое слово \sfunc для определения функций, которые вычисляться не будут. Любая функция, которая элиминирует из \Prop в не \Prop, обязана быть \sfunc. С termination checker'ом это никак не связано, так как просто проблемные функции не вычисляются.
Если я правильно понимаю, что такое computational equality, то этого недостаточно, и нужно предъявить цепочку преобразований. Скорее всего, у нас просто небольшое расхождение в терминологии.
На самом деле большой разницы нет между тем, чтобы проверять произвольное отношение эквивалентности или отношение, которое задается через редукцию. Второе является частным случаем первого, а первое сводится ко второму. Для этого просто достаточно добавить фиктивный терм и сказать, что все эквивалентные термы редуцируются к нему.
Да, мне только потом пришло в голову, что inProp универсальнее. Будет ли корректной ментальной моделью сказать, что inProp эквивалентна семейству K-подобных аксиом для каждого возможного предиката?
Я бы не сказал, что он универсальнее. Тут просто причина в том, что в Arend есть специальная вселенная утверждений. Разумеется, должен быть способ доказать, что она эквивалентна обычной вселенной типов, являющихся утверждениями. Для этого есть несколько механизмов. Один из них — это inProp, который в точности говорит, что все типы в \Prop являются утверждениями.
Лично для меня профит от Prop/Agda-style irrelevance/Idris-style erasure в том, что, ну, доказательства стираются и не утекают в рантайм, и вы их случайно в рантайме не начнёте вычислять (что может быть медленно).
Я бы сказал, что в Arend нет понятия рантайма. Если говорить более формально, то в нем есть выражения, которые вообще не вычисляются. Элиминация из \Prop в не \Prop — это действительно проблема, но если запретить таким функциям вычисляться, то всё будет хорошо. Именно таким образом эта проблема решается в Arend.
То есть, для примера доказательств сортированности списка из статьи, метатеория языка гарантирует, что есть последовательность некоторых редукций (каких?), которая приводит термы друг в друга?
Я не совсем понял о каких термах идет речь. В общем, эквивалентность не обязательно должна работать через редукции. Например, эта-эквивалентность часто без редукций проверяется. Аналогично, чтобы проверить эквивалентность термов, имеющих тип в \Prop, достаточно проверить в какой вселенной лежит их тип.
Формализация математики — это одно из приложений HoTT. Но поиск доказательств — это отдельная задача, и насколько HoTT для нее будет полезна не очевидно. На данный момент мне не известно никаких исследований в этом направлении.
inProp просто говорит, что любые два элемента утверждения (то есть типа, лежащего в \Prop) равны. Аксиома K эквивалентна UIP, которая говорит, что любые два элемента типа равенства равны. Другими словами, что тип равенства является утверждением.
Кстати, пока готовилась эта статья, вышла версия языка 1.1, в которой inProp больше нет, так как теперь любые два элемента утверждения вычислительно равны (а не только пропозиционально).
Но список же двусвязный. Чем начало отличается от конца? Перестраивать нужно все вершины, достижимые из данной, а для двусвязных списков любая вершина достижима из любой другой. Чтобы избежать недопонимания, я сразу уточню, что я говорю про двусвязные списки, которые получаются при помощи техники, известной под названием tying the knot. Других способов, не использующих монады, получить их я не знаю.
Такие двусвязные списки в хаскелле всё равно будут иммутабельные. Ими можно эффективно пользоваться только read-only. Чтобы внести изменение в эту структуру, придется ее полностью перестроить и создать новый список.
Это называется теория доменов. В статье на википедии есть ссылки на разные материалы по теме, если интересно узнать подробнее. Я советую книгу Абрамского.
Прошу обратить внимание, что нигде не написано, что Arend — это язык программирования.
Конечно, даже двумя способами.
На этом всё. Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет. Это может быть полезно и в математике, но не в первую очередь.
Мне кажется, что есть какое-то недопонимание. Если все функции не будут вычисляться, то проблемы с termination вообще не будет. В Arend 1.1 появилось новое ключевое слово \sfunc для определения функций, которые вычисляться не будут. Любая функция, которая элиминирует из \Prop в не \Prop, обязана быть \sfunc. С termination checker'ом это никак не связано, так как просто проблемные функции не вычисляются.
На самом деле большой разницы нет между тем, чтобы проверять произвольное отношение эквивалентности или отношение, которое задается через редукцию. Второе является частным случаем первого, а первое сводится ко второму. Для этого просто достаточно добавить фиктивный терм и сказать, что все эквивалентные термы редуцируются к нему.
Я бы не сказал, что он универсальнее. Тут просто причина в том, что в Arend есть специальная вселенная утверждений. Разумеется, должен быть способ доказать, что она эквивалентна обычной вселенной типов, являющихся утверждениями. Для этого есть несколько механизмов. Один из них — это inProp, который в точности говорит, что все типы в \Prop являются утверждениями.
Я бы сказал, что в Arend нет понятия рантайма. Если говорить более формально, то в нем есть выражения, которые вообще не вычисляются. Элиминация из \Prop в не \Prop — это действительно проблема, но если запретить таким функциям вычисляться, то всё будет хорошо. Именно таким образом эта проблема решается в Arend.
Я не совсем понял о каких термах идет речь. В общем, эквивалентность не обязательно должна работать через редукции. Например, эта-эквивалентность часто без редукций проверяется. Аналогично, чтобы проверить эквивалентность термов, имеющих тип в \Prop, достаточно проверить в какой вселенной лежит их тип.
Формализация математики — это одно из приложений HoTT. Но поиск доказательств — это отдельная задача, и насколько HoTT для нее будет полезна не очевидно. На данный момент мне не известно никаких исследований в этом направлении.
inProp просто говорит, что любые два элемента утверждения (то есть типа, лежащего в \Prop) равны. Аксиома K эквивалентна UIP, которая говорит, что любые два элемента типа равенства равны. Другими словами, что тип равенства является утверждением.
Кстати, пока готовилась эта статья, вышла версия языка 1.1, в которой inProp больше нет, так как теперь любые два элемента утверждения вычислительно равны (а не только пропозиционально).