> По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
В целом вы правы. Но по неправильной причине :). Не то что бы дело в противоречиях. Дело в принятых терминах. Я человек к логике отношение имеющий постольку поскольку и думал что верный термин "естественный вывод". И он верный. Но "натуральная дедукция" тоже легко гуглится и по всей видимости это вполне устоявшийся термин. Ещё встретил "Натуральный вывод".
Так что я поторопился с поправкой.
Coq - как правило, нет (но есть чит-опция)
Coq имеет предикативную систему для Type и импредикативную для Prop. (Ещё можно сделать Set импредикативным с помощью опции).
Насчёт чит-опции я не в курсе, поясните, пожалуйста.
В целом очень интересный обзор (и личная история успеха). Просмотрел пока, думаю вернусь к чтению, любопытно побольше узнать про опыт, похожий на собственный (лет 6 назад).
Martin-Löf type theory (MLTT) и Calculus of Construction (CoC)
Он всё таки различаются. К примеру, MLTT предикативна (вроде бы?). А в CoC (в смысле Coq) есть импредикативный Prop. На сколько я понимаю раньше и Set был импредикативен.
Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).
> По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
В целом вы правы. Но по неправильной причине :). Не то что бы дело в противоречиях. Дело в принятых терминах. Я человек к логике отношение имеющий постольку поскольку и думал что верный термин "естественный вывод". И он верный. Но "натуральная дедукция" тоже легко гуглится и по всей видимости это вполне устоявшийся термин. Ещё встретил "Натуральный вывод".
Так что я поторопился с поправкой.
Coq имеет предикативную систему для Type и импредикативную для Prop. (Ещё можно сделать Set импредикативным с помощью опции).
Насчёт чит-опции я не в курсе, поясните, пожалуйста.
В целом очень интересный обзор (и личная история успеха). Просмотрел пока, думаю вернусь к чтению, любопытно побольше узнать про опыт, похожий на собственный (лет 6 назад).
> Натуральная Дедукция.
Естественный вывод.
Он всё таки различаются. К примеру, MLTT предикативна (вроде бы?). А в CoC (в смысле Coq) есть импредикативный Prop. На сколько я понимаю раньше и Set был импредикативен.
Так, это в закладки...
Унифицирует :) . Можно и в режиме написания кода
eq_symиспользовать в подобном случае (там дальше примеры есть в статье).Я, пожалуй, дополню ответы выше.
Программы не принадлежат к отдельному узкому классу.
Проблему останова действительно нельзя решить (по крайней мере на устройстве "одного ранга" что ли.. про гипотетические устройства более других "рангов" можно глянуть википедию).
Однако её нельзя решить в общем случае. Для каждого конкретного частного случая её можно попытаться решить. Построенное решение (если удалось его построить, конечно) и есть доказательство завершаемости алгоритма. Те математики которые анализируют алгоритмы, время от времени развлекаются решением проблемы останова (каждый раз в частном случае разумеется). Этим же занимаются и инженеры по формальной верификации.
Чуть более подробно, ситуация такая: для части случаев Coq (и другие подобные системы) может автоматически решать проблему останова. Конкретно Coq определяет что рекурсивный вызов рассматриваемой функции происходит на структурно меньшем аргументе. И если это так, то это значит что алгоритм завершится (поскольку так определяются индуктивные типы в Coq). Но это работает только для примитивно-рекурсивных функций. В общем случае приходится формулировать и доказывать утверждения о завершаемости руками.
Один из подходов к доказательству завершаемости общерекурсивных функций средствами Coq описан у автора в одной из публикаций.
Доказать отсутствие вполне можно. Например, ознакомившись со школьным курсом геометрии, в общем-то по моему вполне можно доказать что нет треугольников с суммой углов больше 180 градусов.
Ну и да, вполне можно доказывать отсутствие ошибок в программах, чем инженеры по формальной верификации и занимаются :).