Является ли индукция пути конструктивной?

17

Я читаю книгу HoTT, и мне тяжело с индукцией пути.

Когда я смотрю на тип в разделе 1.12.1 : у меня нет проблем с пониманием того, что это значит (я просто написал тип из памяти, чтобы проверить это).

ind=A:C:x,y:A(x=Ay)U((x:AC(x,x,reflx))x,y:Ap:x=AyC(x,y,p)),

У меня возникла следующая проблема: Мое первое впечатление состояло в том, что это последнее выражение не определяет результирующую функцию а просто заявляет ее недвижимость .

with the equalityind=A(C,c,x,x,reflx):≡c(x)
f:x,y:Ap:x=AyC(x,y,p),

Это в отличие от предыдущих примеров принципов индукции , или \ text {ind} _ \ mathbb {N} - там являются определение уравнения для этих элементов - мы на самом деле знаем , как построить результирующую функцию, учитывая помещение. Что согласуется с «конструктивностью» теории типов, изложенной в этой главе.indA×BindA+BindN

Возвращаясь к ind=A , я с подозрением отнесся к тому факту, что (похоже) он не определен. Заявление о том, что элемент f просто существует, казалось, не соответствует остальной части главы. И действительно, раздел 1.12.1, кажется, подчеркивает, что мое впечатление неверно, и мы на самом деле определили

... функция F: \ prod_ {х, у: А} \ prod_ {р: х = _Ay} С (х, у, р), определяется индукцией пути из C: \ prod_ {х: A} C ( x, x, \ text {refl} _x) , который, кроме того, удовлетворяет f (x, x, \ text {refl} _x): \ эквивалент c (x) ...f:x,y:Ap:x=AyC(x,y,p),
c:x:AC(x,x,reflx)
f(x,x,reflx):≡c(x)

Это оставляет меня в замешательстве, но я чувствую, что этот момент очень важен для всех дальнейших событий. Так с каким из двух чтений для я должен идти? Или, возможно, мне не хватает какой-то важной тонкости, и ответ «нет»? ind=A

Костя
источник
Кстати, на самом деле это не специфический для HoTT вопрос, а более общий вопрос о «зависимых типах».
Коди

Ответы:

12

Это иллюзия, что правила вычислений «определяют» или «конструируют» объекты, о которых они говорят. Вы правильно заметили, что уравнение для не «определяет» его, но не заметило, что то же самое верно и в других случаях. Рассмотрим принцип индукции для единицы типа , который представляется особенно явно «детерминированным». В соответствии с разделом 1.5 книги HoTT у нас есть с уравнение Это "определить" или "построить"ind=A1

ind1:C:1TypeC()x:1P(x)
ind1(C,c,)=c.
ind1ind1«делает»? Например, установите и a = 42 и рассмотрите, что мы могли бы сказать о i n d 1 ( C , 42 , e ) для данного выражения e типа . Ваша первая мысль может быть, что мы можем уменьшить это до потому что " является единственным элементом ". Но, если быть точным, уравнение для применимо, только если мы покажем , что невозможно, когдаC(x)=Na=42
ind1(C,42,e)
e1421ind1ee является переменной, например. Мы можем попытаться выбраться из этого и сказать, что нас интересуют только вычисления с закрытыми членами, поэтому следует закрыть.e

Разве это не тот случай, когда каждый замкнутый член типа существу равен ? На самом деле это зависит от неприятных деталей и сложных доказательств нормализации. В случае HOTT ответ «нет» , потому что е не может содержать экземпляры унивалентностью Axiom, и это не ясно , что делать , чтобы об этом (это открытая проблема в HOTT).e1e

Мы можем обойти проблемы с univalance, рассматривая вариант теории типа , который действительно имеет хорошие свойства , так что каждые замкнутые термы типа является субъективно равны . В этом случае было бы справедливо сказать , что мы действительно знаем , как вычислить с I п д 1 , но:1ind1

  1. То же самое будет иметь место для типа идентичности, потому что каждый замкнутый член типа идентичности будет равняться субъективно некоторой , и так , то уравнение для я п д = будет сказать нам , как вычислить.refl(a)ind=A

  2. Просто потому, что мы знаем, как вычислять с закрытыми членами типа, это не значит, что мы на самом деле что-то определили, потому что есть нечто большее, чем тип с закрытыми членами , как я пытался объяснить однажды.

Например, теорию типа Мартин-Лёф (без типов идентичности) можно интерпретировать домен теоретически таким образом , что содержит два элемента и , где соответствует к и к не-прекращению. Увы, поскольку в теории типов нет способа записать не заканчивающееся выражение, не может быть названо. Следовательно, уравнение для я п d 1 ничего не говорят нам , как вычислить на (два очевидных варианта бытия «охотно» и «ленивую»).1ind1

С точки зрения разработки программного обеспечения, я бы сказал, у нас есть путаница между спецификацией и реализацией . Аксиомы HoTT для типов идентичности являются спецификацией . Уравнение не говорит нам, как вычислить или как построить i n d = C , а скорее что однако я нind=C(C,c,x,x,refl(x))c(x)ind=C "реализовано", мы требуем, чтобы оно удовлетворяло уравнению. Это отдельный вопрос, можно ли получить такое i n d = C конструктивным образом.ind=Cind=C

Наконец, я немного устал от того, как вы используете слово «конструктивный». Похоже, вы думаете, что «конструктивный» такой же, как «определенный». В соответствии с этой интерпретацией Оракул Остановки является конструктивным, поскольку его поведение определяется требованием, которое мы к нему предъявляем (а именно, что он выдает 1 или 0 в зависимости от того, останавливается ли данная машина). Вполне возможно описать объекты, которые существуют только в неконструктивной обстановке. И наоборот, вполне возможно конструктивно говорить о свойствах и других вещах, которые на самом деле не могут быть вычислены. Вот один из них: отношение определенное как H ( n , d )HN×{0,1} конструктивно, т. е. нет ничего плохого в этом определении с конструктивной точки зрения. Так уж сложилось, что конструктивно нельзя показать, что H является тотальным отношением, а его характеристическое отображение χ H : N × { 0 , 1 } P r o p не учитывается через b o o l

ЧАС(N,d)(dзнак равно1Nмашина останавливается)(dзнак равно0N-я машина расходится)
ЧАСχH:N×{0,1}Propboolпоэтому мы не можем «вычислить» его значения.

Приложение: Название вашего вопроса "Является ли индукция пути конструктивной?" Уточнив разницу между «конструктивным» и «определенным», мы можем ответить на вопрос. Да, индукция пути известна как конструктивная в определенных случаях:

  1. Если мы ограничимся теорией типов без однолистности, чтобы мы могли показать сильную нормализацию, то индукция пути и все остальное будет конструктивным, поскольку существуют алгоритмы, выполняющие процедуру нормализации.

  2. Существуют модели реализуемости теории типов, которые объясняют, как каждый замкнутый член в теории типов соответствует машине Тьюринга. Однако эти модели удовлетворяют аксиоме Штрейхера K, которая исключает однолистность.

  3. Существует перевод теории типов (опять же без однолистности) в конструктивную теорию множеств CZF. Еще раз, это подтверждает аксиому К. Штрейхера.

  4. Внутри моделей реализуемости есть группоидная модель, которая позволяет нам интерпретировать теорию типов без К. Стрейхера. Это предварительная работа Стива Аводи и меня.

Нам действительно нужно разобраться в конструктивном статусе Univalence.

Андрей Бауэр
источник
Я считаю, что этот ответ сейчас (частично) устарел
WorldSEnder
Действительно, в то же время теория кубического типа дала положительный ответ: существует конструктивная модель теории однолистного типа.
Андрей Бауэр
7

Я не HoTT человек, но я добавлю свои два цента.

Предположим , что мы хотели , чтобы сделать функцию Как мы это делаем? Хорошо, предположим, что нам даны любые x , y : A и доказательство их равенства p : x = A y . Поскольку я ничего не знаю о произвольном типе A , я ничего не знаю о «структуре» x , y

fA:x,y:Ap:x=AyC(x,y,p)
x,y:Ap:x=AyAx,y, Тем не менее, я знаю кое-что о конкретном типе равенства: у него есть один конструктор, Следовательно, p r e f l a для некоторого a : A , но это заставит х = а = у . Следовательно, если бы у нас был элемент C ( x , x , r e f l x ) для любого
refla:a=Aa, for any a:A
preflaa:Ax=a=yC(x,x,reflx) ; то есть если бы у нас была функция b a s e C : x : A C ( x , x , r e f l x ) (для нашего конкретного C ), то наша функция f A может быть определена следующим образом: f A ( x , y , p ) : = b a s e C ( x , x , p )x:A
baseC:x:AC(x,x,reflx)
CfA
fA(x,y,p):=baseC(x,x,p)
,

Избавление от подписчиков приводит к общему индуктивному определению.

Надеюсь, это поможет!


eEE

Муса Аль-Хасси
источник
1
Возможно, вы можете в этом разобраться, или, по крайней мере, беспокоиться о своей текущей интуиции, просмотрев math.andrej.com/2013/08/28/the-elements-of-an-inductive-type, где я пытаюсь объяснить, почему вредно думать, что закрытые термины типа - это все, что есть для типа.
Андрей Бауэр
2
refl
3

A×BA×B

pair : ABA×B
f A×Bpair

pairf:A×BCAB

f:ABC
fA×B
(ABC)(A×BC)
indA×B

f pair(a,b)ff

f(pair(a,b)) := f a b
яNdA×В е' пaяр(a,б) знак равно е' a б
знак равно

Итак, вы видите, что определение элиминатора для индуктивного типа с данными конструкторами происходит в 2 этапа:

  1. яNd

  2. яNd


знак равноAИкс,Y:Aп:Иксзнак равноYСпИксзнак равноY рееL(Z)Z

е:ΠИкс,Y:A,Иксзнак равноYС
е':ΠZ:A,С
рееL(Z)С

ее'

е Z Z рееL(Z)знак равное' Z

A×Взнак равноA

Коди
источник