Индексы де Брюин в Изабель и Кок

Question

Я хотел бы иметь возможность использовать что-то вроде индексов де Брюйна в Изабель или в Coq, чтобы ссылаться на переменные, которые были введены квантификаторами. Например, вместо того, чтобы писать:

forall x. forall y. (p x y)

Я хотел бы написать что-то вроде:

forall x. forall y. (p '2' '1')

где индексы "2" и "1" указывают, что эти переменные связаны, соответственно, вторым и первым квантификатором (считая изнутри наружу).

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

box box (p '2' '1')

где box должен быть аббревиатурой для чего-то, что вводит безымянную / скрытую связанную переменную, и я хочу, чтобы '2' и '1' ссылались на безымянные / скрытые переменные, введенные крайним левым и правым "ящиком", соответственно.

Можно ли добиться чего-то подобного в Изабель или в Кок??

Answer 1

Здесь я могу говорить только конструктивно за Изабель: формальный синтаксис использует стандартное представление лямбда-терминов де-Брейна для внутренних целей, и существуют различные способы его повторного использования для собственного синтаксиса и специальных обозначений. На самом деле, Isabelle/HOL - это просто еще одно приложение Isabelle, поэтому его квантификаторы и другие связующие элементы определяются в пространстве пользователя обычными механизмами системы.

Понятия, на которые нужно обратить внимание: "связующие", "синтаксические преобразования", "синтаксические переводы" и т. Д., В частности, в Справочном руководстве Изабель / Изар. Это можно растянуть довольно далеко, например, посмотреть, как делается неявное связывание для логики Хоара; это всего лишь один маленький пример из множества других, накопленных за эти годы.

В примере Hoare Logic неявная абстракция вводится через специальную синтаксическую константу _quote, который связан с Syntax_Trans.quote_tr от Изабель /Pure - это практически полезная концепция. Эту идею можно продвинуть еще дальше, чтобы позволить вложение цитаты / антикатотации (см. $ISABELLE_HOME/src/HOL/ex/Multiquote.thy), хотя это не имело практической значимости в приложениях, насколько мне известно.

Кстати, я был бы очень удивлен, если бы у Coq не было подобных механизмов для пользовательской записи с помощью связывателей.