Логические соотношения для предиктивной системы в предикативной мета-теории

14

Логические отношения для непредсказуемых языков, таких как Система F, похоже, критически полагаются на непредсказуемость внешней логики. В частности, интерпретация для типа Форалла будет определяться в терминах всех типизированных отношений. В непредсказуемой системе (например, CiC / Coq) это нормально, но в предикативной системе (например, в Agda) это кажется невозможным.

Как это может быть сделано? Например, как бы вы доказали нормализацию для System F в Agda? Вы должны построить свою собственную непредсказуемую вселенную?

Макс Новый
источник

Ответы:

14

В общем, то, что мы обычно называем аргументом логических отношений, на самом деле не связано с непредсказуемостью: основная идея состоит в том, чтобы просто интерпретировать термины в некоторой абстрактной алгебре и представлять типы как ( -ное) отношение .ANрAN

Это прекрасно работает для всех видов теорий типов, включая теории с зависимой типизацией, см., Например, Shürmann and Sarnat: Структурные логические отношения, где предикативная логика (та из Twelf) используется, чтобы доказать определенное свойство (разрешимость равенства) для предикативного исчисления (просто набрал -calculus) используя логические отношения.λ

Как вы , возможно, подозревал, однако, не удалось доказать нормализацию системы F в Agda (если Agda не тайно сильнее , чем ожидалось, то есть о силе теории типа Мартин-LOF с кучей вселенных). Это связано с тем, что нормализация системы F подразумевает согласованность арифметики 2-го порядка ( ), которая сильнее теории типов ML с любым числом (предикативных) вселенных.пA2

Тем не менее, поучительно выяснить, где именно доказательства в Агде идут не так. Это действительно происходит, когда вы пытаетесь определить логические отношения интерпретации нечеткого количественного определения. Интерпретация неимпредикативных связок (включая «зависимое» количественное определение) кошерна в такой теории, как Агда.

Коди
источник
1
Ого, правда? Вы не можете доказать, что система F нормализуется в Агде? У вас есть цитата для этого?
Макс Новый
2
@MaxNew: это довольно сложно найти цитату. Самое близкое, что я могу найти, - это сила некоторых теорий типа Мартина-Лёфа, которая определенно решает вопрос о предикативной теории с единой вселенной и некоторой индукцией. Но у Агды есть ужасающая рекурсия индукции, которая делает ее намного более мощной.
Коди
1
Однако я должен добавить, что индукционная рекурсия в некоторых случаях, как известно, слабее, чем непредсказуемое количественное определение, как это хорошо объяснено здесь: fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html
cody
1
@cody К сожалению, ссылка больше не работает. Вы можете снова найти этот контент? Знаете ли вы о новых публикациях в области формализации непредсказуемости?
Лукаш Лью