Говорят, что КО является кульминацией всех трех измерений лямбда-куба. Это не очевидно для меня вообще. Я думаю, что я понимаю отдельные измерения, и комбинация любых двух, кажется, приводит к относительно простому объединению (возможно, я что-то упускаю?). Но когда я смотрю на CoC, вместо того, чтобы выглядеть как комбинация всех трех, это выглядит как совершенно другая вещь. Из какого измерения происходят Type, Prop и small / large типы? Куда исчезли зависимые продукты? И почему акцент делается на предложениях и доказательствах, а не на типах и программах? Есть ли что-то эквивалентное, что фокусируется на типах и программах?
Изменить: В случае, если это не ясно, я прошу объяснить, как CoC эквивалентно прямому объединению измерений лямбда-куба. И есть ли фактическое объединение всех трех где-то, где я могу изучать (то есть с точки зрения программ и типов, а не доказательств и предложений)? Это в ответ на комментарии к вопросу, а не на какие-либо текущие ответы.
soft-question
. Я не вижу здесь действительно технического вопроса. Возможно, вы можете быть более конкретным относительно того, что вы спрашиваете?Ответы:
Во-первых, чтобы повторить один из пунктов Коди, исчисление индуктивных конструкций (на котором основано ядро Кока) очень отличается от исчисления конструкций. Лучше всего начинать с теории типов Мартина-Лёфа с вселенных, а затем добавить опору сортировки внизу иерархии типов. Это совершенно другой зверь, чем оригинальный CoC, который лучше всего рассматривать как зависимую версию F-омеги. (Например, CiC имеет теоретико-множественные модели, а CoC - нет.)
Тем не менее, лямбда-куб (членом которого является CoC) обычно представляется как система чистого типа по соображениям экономии в количестве правил ввода. Рассматривая сортировки, типы и термины как элементы одной и той же синтаксической категории, вы можете записать гораздо меньше правил, и ваши доказательства также станут немного менее избыточными.
Тем не менее, для понимания может быть полезно четко разделить различные категории. Мы можем ввести три синтаксические категории, виды (ранжированные по метавариабельной переменной
k
), типы (ранжированные по метавариабельнойA
) и термины (ранжированные по метавариабельной)e
). Тогда все восемь систем можно понимать как вариации того, что разрешено на каждом из трех уровней.λ → (Лямбда-исчисление простого типа)
Это базовое типизированное лямбда-исчисление. Есть один вид
∗
, который является видом типов. Сами типы являются атомарными типамиp
и функциональными типами.A → B
. Термины - это переменные, абстракции или приложения.λω_ (STLC + операторы старшего типа)
STLC разрешает абстракцию только на уровне терминов. Если мы добавим его на уровне типов, то добавим новый вид
k → k
который представляет собой тип функций уровня типа, а также абстракциюλa:k.A
и приложение.A B
на уровне типов. Так что теперь у нас нет полиморфизма, но у нас есть операторы типа.Если память служит, эта система не обладает большей вычислительной мощностью, чем STLC; это просто дает вам возможность сокращать типы.
λ2 (Система F)
Вместо добавления операторов типа мы могли бы добавить полиморфизм. На уровне типов, мы добавляем
∀a:k. A
полиморфный тип, а на уровне мы добавляем абстракцию над типамиΛa:k. e
и типом приложения.e [A]
.Эта система намного более мощная, чем STLC - она так же сильна, как арифметика второго порядка.
λω (Система F-омега)
Если у нас есть оба типа операторов и полиморфизм, мы получаем F-омега. Эта система является более или менее теорией типов ядра большинства современных функциональных языков (таких как ML и Haskell). Он также значительно более мощный, чем система F - он эквивалентен по силе арифметике более высокого порядка.
λP (LF)
Вместо полиморфизма мы могли бы пойти в направлении зависимости от простейшего типа лямбда-исчисления. Если вы позволили типу функции разрешить использование ее аргумента в возвращаемом типе (т.е.
Πx:A. B(x)
вместо записиA → B
), то вы получите λP. Чтобы сделать это действительно полезным, мы должны расширить набор видов с помощью операторов типа, которые принимают термины в качестве аргументовΠx:A. k
, и поэтому мы должны добавить соответствующую абстракциюΛx:A.B
и приложениеA [e]
на уровне типов.Эту систему иногда называют LF, или Edinburgh Logical Framework.
Он обладает такой же вычислительной мощью, как и простейшее лямбда-исчисление.
λP2 (без специального имени)
Мы также можем добавить полиморфизм к λP, чтобы получить λP2. Эта система используется не часто, поэтому у нее нет определенного имени. (Одна статья, которую я прочитал и которая использовала ее, - « Индукция Германа Гойвера» не выводится в теории зависимых типов второго порядка .)
Эта система имеет ту же силу, что и система F.
λPω_ (без специального имени)
Мы могли бы также добавить операторы типа к λP, чтобы получить λPω_. Это включает в себя добавление типа
Πa:k. k'
для операторов типа, а также соответствующую абстракциюΛx:A.B
и приложение на уровне типа.A [e]
.Поскольку снова нет скачка в вычислительной мощности по сравнению с STLC, эта система также должна стать прекрасной основой для логической структуры, но никто этого не сделал.
λPω (исчисление конструкций)
Наконец, мы получаем λPω, исчисление конструкций, взяв λPω_ и добавив полиморфный тип прежнего
∀a:k.A
и абстракцию уровня терминаΛa:k. e
и применениеe [A]
для него.Типы этой системы гораздо более выразительны, чем в F-омеге, но имеют одинаковую вычислительную мощь.
источник
Я часто хотел попытаться суммировать каждое измерение куба и то, что он представляет, поэтому я попробую это сделать.λ
Но сначала, вероятно, следует попытаться распутать различные проблемы. Интерактивный доказатель теорем Coq основан на основной теории типов, которую иногда с любовью называют исчислением индуктивных конструкций со вселенными . Вы заметите, что это нечто большее, чем просто «Исчисление конструкций», и, действительно, там гораздо больше вещей, чем просто CoC. В частности, я думаю, что вы не уверены, какие именно функции есть в самом CoC. В частности, различие Set / Prop и юниверсы не отображаются в CoC.
Я не буду давать полный обзор систем Pure Type здесь, но важное правило (для функциональных PTS, таких как CoC) заключается в следующем
где являются элементы фиксированного множества S из рода , и пара ( ы , K ) находится в фиксированном множестве R пара S , называется правилом .s,k S (s,k) R S
Решающее понимание, что тщательный выбор из и R сделать огромные различия в том , что тип продукта Π х : . Б на самом деле представляет!S R Πx:A.B
В частности, в исчислении конструкций, множество сортов есть { * , ◻ } часто называют Prop и типа (хотя эта терминология немного запутанным для пользователя Coq по причинам , я расскажу чуть позже), а полная набор правил: R = { ( ∗ , ∗ ) , ( ◻ , ◻S
Итак, у нас есть 4 правила, которые соответствуют 4 различным целям:
: типы функций(∗,∗)
Я объясню каждый из них более подробно.
Прежде всего заметим , что я буду писать вместо П х : А .A→B Πx:A.B x B
С этими дополнительными сортировками и правилами вы получаете что-то не PTS, а что-то близкое. Это (почти) Расширенное исчисление конструкций , которое ближе к основанию Coq. Большая недостающая часть здесь - индуктивные типы, которые я не буду обсуждать здесь.
Изменить: есть довольно хороший справочник, который описывает различные функции языков программирования в рамках PTS, описывая PTS, который является хорошим кандидатом для промежуточного представления функционального языка программирования:
Хенк: типизированный промежуточный язык , С.П. Джонс и Э. Мейер.
источник