Information

Founded
Location
Россия
Website
www.jetbrains.com
Employees
501–1,000 employees
Registered
Pull to refresh
Comments 19

Я ненастоящий сварщик (и метатеорию HoTT не знаю совсем), но чем inProp принципиально отличается от аксиомы K?

inProp просто говорит, что любые два элемента утверждения (то есть типа, лежащего в \Prop) равны. Аксиома K эквивалентна UIP, которая говорит, что любые два элемента типа равенства равны. Другими словами, что тип равенства является утверждением.


Кстати, пока готовилась эта статья, вышла версия языка 1.1, в которой inProp больше нет, так как теперь любые два элемента утверждения вычислительно равны (а не только пропозиционально).

inProp просто говорит, что любые два элемента утверждения (то есть типа, лежащего в \Prop) равны. Аксиома K эквивалентна UIP, которая говорит, что любые два элемента типа равенства равны.

Да, мне только потом пришло в голову, что inProp универсальнее. Будет ли корректной ментальной моделью сказать, что inProp эквивалентна семейству K-подобных аксиом для каждого возможного предиката?


Лично для меня профит от Prop/Agda-style irrelevance/Idris-style erasure в том, что, ну, доказательства стираются и не утекают в рантайм, и вы их случайно в рантайме не начнёте вычислять (что может быть медленно).


Однако, например, если вы захотите что-нибудь выразить через фундированную рекурсию/индукцию, то стандартный фреймворк (например, в терминах идриса wfInd : WellFounded rel => (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (x10 : a) -> P x10) будет паттерн-матчиться на доказательство фундированности (вот это вот rel y x), что имеет все шансы утечь в рантайм (и надо дополнительно приседать, чтобы этого избежать — Idris 1 не умеет в автоматическое erasure для higher-order arguments). Ну и да, если вы не можете использовать Prop кроме как для других Prop, то как это всё будет вместе работать для того, чтобы дать вам что-то в Set в случаях типа этого?


Кстати, пока готовилась эта статья, вышла версия языка 1.1, в которой inProp больше нет, так как теперь любые два элемента утверждения вычислительно равны (а не только пропозиционально).

То есть, для примера доказательств сортированности списка из статьи, метатеория языка гарантирует, что есть последовательность некоторых редукций (каких?), которая приводит термы друг в друга?


Если да, это это прям получается этакий вариант конфлюэнтности, и это ппц изящно!

Да, мне только потом пришло в голову, что inProp универсальнее. Будет ли корректной ментальной моделью сказать, что inProp эквивалентна семейству K-подобных аксиом для каждого возможного предиката?

Я бы не сказал, что он универсальнее. Тут просто причина в том, что в Arend есть специальная вселенная утверждений. Разумеется, должен быть способ доказать, что она эквивалентна обычной вселенной типов, являющихся утверждениями. Для этого есть несколько механизмов. Один из них — это inProp, который в точности говорит, что все типы в \Prop являются утверждениями.


Лично для меня профит от Prop/Agda-style irrelevance/Idris-style erasure в том, что, ну, доказательства стираются и не утекают в рантайм, и вы их случайно в рантайме не начнёте вычислять (что может быть медленно).

Я бы сказал, что в Arend нет понятия рантайма. Если говорить более формально, то в нем есть выражения, которые вообще не вычисляются. Элиминация из \Prop в не \Prop — это действительно проблема, но если запретить таким функциям вычисляться, то всё будет хорошо. Именно таким образом эта проблема решается в Arend.


То есть, для примера доказательств сортированности списка из статьи, метатеория языка гарантирует, что есть последовательность некоторых редукций (каких?), которая приводит термы друг в друга?

Я не совсем понял о каких термах идет речь. В общем, эквивалентность не обязательно должна работать через редукции. Например, эта-эквивалентность часто без редукций проверяется. Аналогично, чтобы проверить эквивалентность термов, имеющих тип в \Prop, достаточно проверить в какой вселенной лежит их тип.

Я бы сказал, что в Arend нет понятия рантайма.

Ну вот вы написали, скажем, функцию сортировки и что-то про неё доказали. А что вы дальше с этой функцией делаете?


Элиминация из \Prop в не \Prop — это действительно проблема, но если запретить таким функциям вычисляться, то всё будет хорошо. Именно таким образом эта проблема решается в Arend.

Мой поинт в том, что бывают случаи, когда вычисляться таки надо


Правда, все такие случаи, что я могу придумать, связаны с необходимостью убедить termination checker, что всё хорошо, а те termination checker'ы, к которым я привык, основаны на тупой проверке синтаксического уменьшения терма. Я в работу Абеля пока внимательно не прочитал (спасибо автору статьи за ссылку!), но у него там вроде что-то умнее, так что, может, проблема не столь актуальна.


Я не совсем понял о каких термах идет речь.

Которые доказательства выражают же ж :)


Аналогично, чтобы проверить эквивалентность термов, имеющих тип в \Prop, достаточно проверить в какой вселенной лежит их тип.

Если я правильно понимаю, что такое computational equality, то этого недостаточно, и нужно предъявить цепочку преобразований. Скорее всего, у нас просто небольшое расхождение в терминологии.

Ну вот вы написали, скажем, функцию сортировки и что-то про неё доказали. А что вы дальше с этой функцией делаете?

На этом всё. Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет. Это может быть полезно и в математике, но не в первую очередь.


Мой поинт в том, что бывают случаи, когда вычисляться таки надо.

Мне кажется, что есть какое-то недопонимание. Если все функции не будут вычисляться, то проблемы с termination вообще не будет. В Arend 1.1 появилось новое ключевое слово \sfunc для определения функций, которые вычисляться не будут. Любая функция, которая элиминирует из \Prop в не \Prop, обязана быть \sfunc. С termination checker'ом это никак не связано, так как просто проблемные функции не вычисляются.


Если я правильно понимаю, что такое computational equality, то этого недостаточно, и нужно предъявить цепочку преобразований. Скорее всего, у нас просто небольшое расхождение в терминологии.

На самом деле большой разницы нет между тем, чтобы проверять произвольное отношение эквивалентности или отношение, которое задается через редукцию. Второе является частным случаем первого, а первое сводится ко второму. Для этого просто достаточно добавить фиктивный терм и сказать, что все эквивалентные термы редуцируются к нему.

Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет.

А, ну тогда да, вопрос снят.


Для этого просто достаточно добавить фиктивный терм и сказать, что все эквивалентные термы редуцируются к нему.

Именно! Кажется, мы тут говорим об одном и том же :)

Так как язык ориентирован именно на доказательство теорем, то большой необходимости запускать функции нет

А ну т.е. это еще одна система для доказательств. С Idris тогда нечего сравнивать, он как general purpose язык вне конкуренции :D
Хотя Куклев и смышлёный, но воеводская наука вся фигня. А уже кое-кто это называл «основаниями математики 21-го века». И тут Воеводский, со свойственной ему оригинальностью, взял да помер. И что теперь делать основателям математики 21-го века?
Правильно ли я понимаю, что этот HoTT нужен для того чтобы формализовать математические теоремы, то есть перевести их на этот язык типов, чтобы программно можно было проверить что доказательство теоремы верно? А если так, то можно ли тогда программно найти доказательство какой-нибудь открытой гипотезы, например, путём перебора всех возможных доказательств?

Формализация математики — это одно из приложений HoTT. Но поиск доказательств — это отдельная задача, и насколько HoTT для нее будет полезна не очевидно. На данный момент мне не известно никаких исследований в этом направлении.

Правильно ли я понимаю, что этот HoTT нужен для того чтобы формализовать математические теоремы, то есть перевести их на этот язык типов, чтобы программно можно было проверить что доказательство теоремы верно?

Это можно делать и без HoTT (упомянутые в статье Coq и Agda/Idris это успешно делают, Coq так вообще лет 30 как, а какой-нибудь Automath — лет 60). HoTT (как я, глупый, понимаю) нужна для устранения некоторых проблем с понятием равенства.


А если так, то можно ли тогда программно найти доказательство какой-нибудь открытой гипотезы, например, путём перебора всех возможных доказательств?

Долго перебирать придётся, быстрее вырастить поколение математиков под вашу открытую гипотезу. Но очень ограниченный вариант этого перебора вполне используется, да.

Статья на хабре: новый язык программирования, jetbrains, inteliJ, обычное хипстерство, вдруг, HoTT, взрыв мозга, читать пословно.


Спасибо за описание.


Вопрос. Написано:


Сумма типов A + B. В Haskell этот тип называется Either A B. Так как этот тип населен тогда и только тогда, когда один из типов A или B населен, то эта конструкция соответствует логическому «или».


А если A и B населены, то A+B населено или нет?

Статья на хабре: новый язык программирования, jetbrains, inteliJ, обычное хипстерство, вдруг, HoTT, взрыв мозга, читать пословно.

Прошу обратить внимание, что нигде не написано, что Arend — это язык программирования.


А если A и B населены, то A+B населено или нет?

Конечно, даже двумя способами.

Если A+B населено если А населено и B населено, то формулировка неверна:


Сумма типов A + B. В Haskell этот тип называется Either A B. Так как этот тип населен тогда и только тогда, когда один из типов A или B населен, то эта конструкция соответствует логическому «или».


Правильно: хотя бы один.

Воеводский обнаружил, что на языке теории типов (Мартин-Лёфа) можно говорить о так называемых гомотопиях (а это большой и авторитетный раздел математики). До этого специалисты по теории типов воспринимали программистов как главную цель. На форуме types-list много лет стоял печальный стон «почему программисты нас не ценят?» И тут пришёл Воеводский, известный математик, лауреат премии Филдса. Возник энтузиазм «нафиг программистов, давайте охмурять гомотопных математиков!» Вся орда специалистов по Coq бросилась изучать гомотопии (во главе с Тьерри Коканом). Стали скромно называть себя «основания математики 21-го века». И тут Воеводский взял да помер. А кого из них, кроме Воеводского, знает гомотопный математик? Приходится опять охмурять программистов.

Правильно ведь понимаю, что язык назван в честь Гейтинга? Добавьте в статью!

Only those users with full accounts are able to leave comments. Log in, please.