Логическая структура против теории типов

В чем разница между логической структурой и теорией типов? Оба они имеют типы, термины и основаны на лямбда-исчислении с зависимой типизацией.

У нас есть Edinburg LF, который основан на исчислении лямбда-пи, однако мне кажется, что здесь есть некоторая тонкая разница.

Резюме. Логическая структура - это метаязык для формализации дедуктивных систем, где дедукции становятся синтаксическими объектами.

Конечно, то, что считается метаязыком, довольно расплывчато, и полезно понимать историческое развитие логических структур. Первой логической структурой была автоматика де Брюина (1), основанная на $\lambda$ расчете. Многие идеи из семейства языков Automath нашли свое отражение в современных логических рамках. Работа Мартина-Лёфа над конструктивными теориями типов, также основанная на $\lambda$ калькуляциях, также оказала влияние.

LF (2) в Эдинбурге - очень влиятельная логическая структура. Эдинбург LF - это то, что вы получаете, когда обогащаете простой тип калькуляции зависимостью от типа. Вот и все. Для того чтобы сделать типа зависимости точными, необходимо заменить функциональное пространство оператор A → B на типах с типом-абстракцией, обычно записываются Π х A . B , и ввести вид типов, а также вид абстракции. С точки зрения правил ключ находится в правиле исключения для A → B , соответственно. Π х A . B :$\lambda$$A \rightarrow B$$\Pi x^A. B$$A \rightarrow B$$\Pi x^A. B$

Слева у нас есть правило для простого типа -calculus, справа - правило, обобщающее левое с типовой зависимостью. Мы видим, что значение «втекает» в тип в заключении справа.$\lambda$

Я думаю, что интерактивный помощник по проверке Изабель использует интуитивистскую логику второго порядка, основанную на -calculus, без каких-либо чисел или рекурсивных типов данных в качестве логической структуры. Различные другие были предложены.$\lambda$

Одним из преимуществ использования -calculi в качестве логического каркаса является то, что конструкции связывания, подобные универсальным квантификаторам, могут быть реализованы с использованием -binder каркаса. Обратите внимание, что большинство логических фреймворков явно слабые: фреймворки поддерживают рассуждения на уровне объекта, но недостаточны для выполнения многих мета-теоретических рассуждений, помимо того факта, что конкретное утверждение на уровне объекта является теоремой. На самом деле металл-логика обычно настолько слаба, что даже доказательство теоремы дедукции для объектной логики в стиле Гильберта невозможно. Конечно, ничто не мешает вам использовать более мощные теории типов в качестве логической основы.$\lambda$$\lambda$

По этим практическим и историческим причинам большинство логических структур, используемых сегодня, являются типизированными -calculi, то есть теориями типов. См. (3, 4) для более глубокого обсуждения логических структур.$\lambda$

1. Н. де Брюйн: Математический язык АВТОМАТ, его использование и некоторые его расширения.

2. Р. Ф. Харпер, Ф. Хонселл, Г. Плоткин: основа для определения логики .

3. Ф. Пфеннинг: Логические основы.

4. Ф. Пфеннинг: Логические основы - краткое введение .