Как объявить «свободный» экземпляр класса типа?

Question

Я пытаюсь смоделировать некоторый программный анализ в Isabelle/HOL. Анализ вычисляет значения в ограниченной решетке, но (на данный момент и для общности) я не хочу фиксировать какое-либо конкретное определение решетки; все, о чем я забочусь, является ли какой-то результат дном или нет. Я ищу способ объявить абстрактный тип, который является экземпляром класса класса Isabelle/HOL bounded_lattice, не переходя к конкретному экземпляру.

То есть, аналогично тому, как я мог бы написать

typedecl some_data 
type_synonym my_analysis_result = "var => some_data" 

где some_data полностью свободен, я хотел бы быть в состоянии написать что-то вроде

typedecl "some_lattice::bounded_lattice" 
type_synonym my_analysis_result = "var => some_lattice" 

где some_lattice бы «бесплатно «ограниченная решетка которой не требует ничего, кроме того, что она выполняет законы решетки. Этот конкретный синтаксис не принимается Isabelle/HOL, и ни что-то вроде

type_synonym my_analysis_result = "var => 'a::bounded_lattice" 

я могу обойти эту проблему, определив конкретный тип данных и делает его экземпляр bounded_lattice, но я не вижу, почему не должен быть более общим способом. Есть ли простой (или сложный) синтаксис для достижения того, что я делаю? Должен ли я (каким-то образом, я не уверен, будет ли это работать) все мои разработки внутри блока context bounded_lattice? Или есть причина, почему логически нормально иметь полностью свободные типы через typedecl, но не бесплатные типы, ограниченные классом типа?

Answer 1

Выполнение неуказанного типа экземпляр класса типа может привести к несогласованности, если класс типа имеет противоречивые предположения. Чтобы объяснить эту аксиоматическую природу, вам нужно аксиоматизировать экземпляр. Вот пример:

typedecl some_lattice 
axiomatization where some_lattice_bounded: 
    "OFCLASS(some_lattice, bounded_lattice_class)" 
instance some_lattice :: bounded_lattice by(rule some_lattice_bounded) 

NB: Несколько лет назад, вы могли бы использовать команду arities, но это было прекращено, чтобы подчеркнуть аксиоматический характер неопределенных конкретизации класса типа.

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

type_synonym 'a my_analysis_result = "var => 'a" 

Синонимы типа с ограничениями сортировки не поддерживаются Isabelle (как не имеет смысла в любом случае). Если вы добавите ограничение сортировки, вы получите предупреждение о том, что оно будет проигнорировано. Всякий раз, когда вам нужен экземпляр bounded_lattice, введите вывод, чтобы добавить ограничение сортировки (или вы должны указать его явно для переменной типа).