Пруфчекинг

[Утундрий]

Гм... А что по этому поводу говорит Кальтенбруннер ChatGPT?

[george66]

Желая понять, как устроен Coq внутри (какая в нём теория типов, как делается проверка типизации и т.д.), читаю свежую статью авторитетов
https://inria.hal.science/hal-04077552/document
и оттуда узнал, что в Coq (программе Coq на языке Ocaml) каждый год находят критические уязвимости (наподобие "забыли где-то написать подстановку"), в результате опытный пользователь может написать доказательство лжи, которое Coq одобрит как правильное. Авторитеты пытаются сам алгоритм Coq формализовать и доказать, что он правильно работает.

[ozheredov]

george66, a "четыре краски" cock доказал, или последний всего лишь пруфчекер? Могут ли найтись уязвимости в индуцирующей машинное доказательство системе?

[george66]

ozheredov в сообщении #1647569 писал(а):

george66, a "четыре краски" cock доказал, или последний всего лишь пруфчекер? Могут ли найтись уязвимости в индуцирующей машинное доказательство системе?

Coq позволяет строить доказательства полуавтоматически. Пользователь даёт руководящие указания ("тактики"). Например, я пишу
induction m.
Это значит "попробуй индукцию по m". Coq выдаёт два утверждения ("цели"), которые надо доказать: базис индукции и шаг индукции, я их доказываю по очереди (на самом деле можно и не по по очереди, а в любом порядке). Допустим, я вижу, что базис уже доказан раньше в виде Lemma 1, я пишу
apply Lemma1.
одна цель пропадает, кусочек доказательства добавляется. Тактики - это программки на языке Ocaml, тактика применяется к существующему на данный момент доказательству и набору целей и выдаёт новый набор целей и новое доказательство. Тактики могут содержать ошибки, но Coq всегда проверяет законченное доказательство ещё раз, поэтому ошибки в тактиках быстро становятся видны.

[Утундрий]

george66 в сообщении #1647566 писал(а):

в Coq (программе Coq на языке Ocaml) каждый год находят критические уязвимости (наподобие "забыли где-то написать подстановку")

Это символично, господа! Поскольку Coq, очевидно, не способен проверить сам себя, то напрашивается целая иерархия "проверяторов".

[ozheredov]

Утундрий в сообщении #1647574 писал(а):

Поскольку Coq, очевидно, не способен проверить сам себя, то напрашивается целая иерархия "проверяторов"

Притом, по-видимому, бесконечная.

[Утундрий]

ozheredov в сообщении #1647576 писал(а):

Притом, по-видимому, бесконечная.

Это если george66 не поведётся на мой "продуманный" развод и не сочинит селфпруфчекер.

[george66]

Формализовал свою теорему в Coq, получилось 1600 строк (за вычетом пустых и комментариев)
https://www.mediafire.com/file/kxhk8yo5 ... /99.v/file
(файл можно смотреть любым текстовым редактором, но лучше поставить Coq).
Теорема доказывает, что обычная подстановка действительно соответствует подстановке де Брёйна. Краткое содержание первых 200 строк.
В самом начале строчки

Parameter Var : Set.
Parameter eq_dec : forall (x y : Var), {x=y}+{x<>y}.

Они говорят "возьмём произвольное множество Var (содержательно, это множество переменных) с разрешимым равенством (по любым переменным x,y можно эффективно проверить, совпадают они или нет)". Далее идёт
1) Определение типа данных Lam (лямбда-термы) и предиката isfresh x M, который проверяет, что переменная x не входит свободно в терм M ("свежая для M"). Также определяется предикат isfresh_forall x L, который проверяет, что переменная x не входит свободно ни в какой терм из списка L. Пишутся строчки

Parameter fresh : forall (L : list Lam), Var.
Axiom freshness : forall (L : list Lam), isfresh_forall (fresh L) L = true.

которые утверждают, что есть функция fresh, которая по любому списку термов L выдаёт переменную, свежую для них всех (это понадобится при определении подстановки).
2) Определение типа данных dB (лямбда-термы де Брёйна). Определение вспомогательной функции index, которая находит номер первого вхождения переменной в список переменных (и выдаёт 0, если её там нет). Определение функции transfer, которая по списку переменных Gamma и лямбда-терму M выдаёт соответствующий терм де Брёйна. Все эти определения стандартные.
3) Определение одновременной подстановки M [N0/x0, N1/x1 ... Nk/xk]
4) Определение аналогичной подстановки де Брёйна M' [N'0, N'1, ... N'k]
Чтобы понять, о каких "\uparrow" и "\Uparrow" идёт речь, надо скачать несколько статей по явной подстановке (начиная с вот этой
https://inria.hal.science/file/index/do ... R-2477.pdf
достаточно понять страницы 6-9, но это тоже не совсем легко)
5) Формулировка основной теоремы:
для любого списка переменных Gamma, лямбда-терма M и подстановки [N0/x0,...,Nk/xk]
если список переменных подстановки x0,...,xk не содержит повторений (иначе определение подстановки неправильно работает), то
transfer (Gamma, M [N0/x0,...,Nk/xk]) = M'[N'0,...,N'k]
где
M' = transfer ([x0,...,xk]++Gamma, M)
N'0 = transfer (Gamma, N0)
...
N'k = transfer (Gamma, Nk)

Доказательства, записанные в Coq, не предназначены для чтения человеком, так что можно просто посмотреть "как это выглядит всерьёз".