Как вы представляете условия CoC в Агде?

Question

Представлять, например, STLC в Агде можно следующим образом:

data Type : Set where
*   : Type
_⇒_ : (S T : Type) → Type

data Context : Set where
ε   : Context
_,_ : (Γ : Context) (S : Type) → Context

data _∋_ : Context → Type → Set where
here  : ∀ {Γ S} → (Γ , S) ∋ S
there : ∀ {Γ S T} (i : Γ ∋ S) → (Γ , T) ∋ S

data Term : Context → Type → Set where
var : ∀ {Γ S} (v : Γ ∋ S) → Term Γ S
lam : ∀ {Γ S T} (t : Term (Γ , S) T) → Term Γ (S ⇒ T)
app : ∀ {Γ S T} (f : Term Γ (S ⇒ T)) (x : Term Γ S) → Term Γ T

(с здесь .) Однако попытка адаптировать это к исчислению конструкцийпроблематично, потому что Тип и Термин - единственный тип.Это означает, что не только Context / Term должен быть взаимно рекурсивным, но также и то, что Term должен быть проиндексирован сам по себе.Вот первоначальная попытка:

data Γ : Set

data Term : Γ → Term → Set

data Γ where
  ε   : Γ
  _,_ : (ty : Term) (ctx : Γ) → Γ
infixr 5 _,_

data Term where
    -- ...

Agda, однако, жалуется, что Term не входит в сферу ее первоначального объявления.Можно ли представить это таким образом, или нам действительно нужны разные типы для термина и типа?Я бы очень хотел увидеть минимальную / справочную реализацию CoC в Agda.

Answer 1

Известно, что это очень сложная проблема.Насколько я знаю, не существует "минимального" способа кодирования CoC в Agda.Вы должны либо доказать много вещей, либо использовать поверхностное кодирование, либо использовать тяжелые (но совершенно разумные) методы, такие как факторное наведение, или сначала определить нетипизированные термины, а затем преобразовать их в типизированные.Вот некоторая связанная литература:

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

Проверка и нормализация типов , Джеймс Чепмен - пятая глава этого тезиса представляет собой формализациюзависимо типизированный язык.Это также формализация в стиле тонны лемм, за исключением того, что многие леммы являются просто конструкторами соответствующих типов данных.Например, у вас есть явные замены как конструкторы, а не как вычислительные функции (предыдущий тезис не имел их для типов, только для терминов, в то время как этот тезис имел явные замены даже для типов).

Возмутительные, но значимые совпадения.Зависимый типобезопасный синтаксис и оценка , Конор МакБрайд - в этой статье представлено глубокое кодирование теории зависимых типов, которая улучшает поверхностное кодирование теории.Это означает, что вместо определения подстановочных и проверочных свойств об этом автор просто использует оценочную модель Agda, но также дает полный синтаксис для целевого языка.

Типизированное синтаксическое метапрограммирование ,Доминик Девриз, Фрэнк Писсенс - нетипизированные термины, преобразованные в типизированные.IIRC было много постулатов в коде, когда я изучал его, так как это скорее структура для метапрограммирования, чем для формализации.

Теория типов пожирает себя сама? , Chuangjie Xu& Martin Escardo - формализация одного файла.Как всегда, несколько типов данных определены взаимно.Явные замены с явными переносами, которые «имитируют» поведение операций замещения.

EatEval.agda - мы получаем это, комбинируя идеи из двух предыдущих формализаций.В этом файле вместо определения нескольких явных транспортов у нас есть только один транспорт, который позволяет изменить тип термина на денотационно равный.Т.е. вместо явного указания поведения замещения с помощью конструкторов, у нас есть один конструктор, который говорит: «Если оценка двух типов в Agda дает одинаковые результаты, то вы можете преобразовать термин одного типа в другой через конструктор».

Теория типов в теории типов с использованием фактор-индуктивного типа , Торстен Альтенкирх, Амбрус Капоши - это самый многообещающий подход, который я бы сказал.Он «узаконивает» вычисления на уровне типов с помощью устройства с частными типами.Но у нас пока нет фактор-типов в Агде, они по существу постулируются в статье.Люди много работают над частными типами (есть целый тезис: Фактор-индуктивно-индуктивные определения - Дейкстра, Гейб), поэтому, возможно, мы их когда-нибудь получим.

Разрешимость преобразования для теории типов в теории типов , Андреас Абель, Йоаким Оман, Андреа Веццози - нетипизированные термины , реализованные как типизированные . Много свойств .Также имеет много метатеоретических доказательств и особенно интересное устройство, которое позволяет доказать обоснованность и полноту, используя те же логические отношения.Формализация огромна и хорошо прокомментирована.

Сетоидная модель экстенсиональной теории типа Мартина-Лёфа в Agda ( zip-файл с развитием ), Эрик Палмгрен - аннотация:

Аннотация.Мы представляем детали формализации Агды сетоидной модели теории типов Мартина-Лёфа с Пи, Сигмой, экстенсиональными типами тождеств, натуральными числами и бесконечной иерархией вселенной à la Russell.Ключевым компонентом является использование итерационных множеств типа Aczel V в качестве экстенсиональной вселенной сетоидов, что позволяет правильно интерпретировать равенство типов.

Coq в Coq Бруно Баррас и Бенджамин Вернер - формализация CC в Coq ( код ).Нетипизированные термины обозначены как типовые + множество лемм + метатеоретические доказательства.

Спасибо Андрасу Ковачу и Джеймсу Чепмену за предложения.