Интуиционистская теория типов

Интуиционистская теория типов (также известная как конструктивная теория типов или теория типов Мартина-Лёфа , последняя сокращенно MLTT ) — это теория типов и альтернативная основа математики .Интуиционистская теория типов была создана Пером Мартином-Лёфом , шведским математиком и философом , который впервые опубликовал ее в 1972 году. Существует несколько версий теории типов: Мартин-Лёф предложил как интенсиональные , так и экстенсиональные варианты теории, а также ранние импредикативные версии, несостоятельность, показанная парадоксом Жирара , уступила место предикативным версиям. Однако во всех версиях сохраняется основная конструкция конструктивной логики с использованием зависимых типов .

Дизайн

Мартин-Лёф разработал теорию типов на принципах математического конструктивизма . Конструктивизм требует, чтобы любое доказательство существования содержало «свидетеля». Таким образом, любое доказательство того, что «существует простое число больше 1000», должно идентифицировать конкретное число, которое одновременно является простым и больше 1000. Интуиционистская теория типов достигла этой цели, усвоив интерпретацию БХК . Интересным следствием является то, что доказательства становятся математическими объектами, которые можно исследовать, сравнивать и манипулировать ими.

Конструкторы типов интуиционистской теории типов были созданы для обеспечения взаимно однозначного соответствия логическим связкам. Например, логическая связка, называемая импликацией ( $A\implies B$) соответствует типу функции ( $A\to B$). Это соответствие называется изоморфизмом Карри–Говарда . Предыдущие теории типов также следовали этому изоморфизму, но Мартин-Лёф был первым, кто распространил его на логику предикатов , введя зависимые типы.

Теория типов

Интуиционистская теория типов имеет три конечных типа, которые затем составляются с использованием пяти различных конструкторов типов. В отличие от теорий множеств , теории типов не строятся на основе логики, подобной логике Фреге . Таким образом, каждая особенность теории типов выполняет двойную функцию как функции математики и логики.

Если вы не знакомы с теорией типов и знакомы с теорией множеств, краткое изложение таково: типы содержат термины точно так же, как множества содержат элементы. Термины принадлежат к одному и только одному типу. Такие термины, как $2+2$ и $2\cdot 2$ вычислить («свести») до канонических терминов, таких как 4. Подробнее см. в статье о теории типов .

Тип 0, тип 1 и тип 2

Существует три конечных типа: Тип 0 содержит 0 термов. Тип 1 содержит 1 канонический термин. А тип 2 содержит 2 канонических термина.

Поскольку тип 0 содержит 0 терминов, его также называют пустым типом . Он используется для обозначения всего, что не может существовать. Это также написано $\bot$ и представляет собой нечто недоказуемое. (То есть доказательство этого не может существовать.) В результате отрицание определяется как его функция: $\neg A:=A\to \bot$.

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

Наконец, тип 2 содержит 2 канонических термина. Это представляет собой определенный выбор между двумя ценностями. Он используется для логических значений , но не для предложений.

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

Конструктор типа Σ

Σ-типы содержат упорядоченные пары. Как и в случае с типичными упорядоченными парными (или двухкортежными) типами, Σ-тип может описывать декартово произведение , $A\times B$, двух других типов, $A$ и $B$. Логично, что такая упорядоченная пара будет служить доказательством $A$ и доказательство $B$, поэтому можно увидеть такой тип, записанный как $A\wedge B$.

Σ-типы более эффективны, чем типичные типы упорядоченных пар, из-за зависимой типизации. В упорядоченной паре тип второго слагаемого может зависеть от значения первого слагаемого. Например, первый член пары может быть натуральным числом , а тип второго члена может быть последовательностью действительных чисел длины, равной первому члену. Такой тип будет записан:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

Используя терминологию теории множеств, это похоже на индексированное непересекающееся объединение множеств. В случае обычного декартова произведения вид второго слагаемого не зависит от значения первого слагаемого. Таким образом, тип, описывающий декартово произведение ${\mathbb {N} }\times {\mathbb {R} }$ написано:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }$

Здесь важно отметить, что значение первого слагаемого $n$, не зависит от типа второго слагаемого, ${\mathbb {R} }$.

Σ-типы можно использовать для создания более длинных зависимо типизированных кортежей, используемых в математике, а также записей или структур, используемых в большинстве языков программирования. Примером трехкортежа с зависимой типизацией являются два целых числа и доказательство того, что первое целое число меньше второго целого числа, описываемое типом:

$\sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}$

Зависимая типизация позволяет Σ-типам выполнять роль квантора существования . Утверждение «существует $n$ типа ${\mathbb {N} }$, такой, что $P(n)$ доказано» становится типом упорядоченных пар, где первым элементом является значение $n$ типа ${\mathbb {N} }$ а второй пункт является доказательством $P(n)$. Обратите внимание, что тип второго пункта (доказательства $P(n)$) зависит от значения в первой части упорядоченной пары ( $n$). Его тип будет:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

Конструктор типа Π

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

Например, тип функции, которая по натуральному числу $n$, возвращает вектор, содержащий $n$ действительные числа записаны:

$\prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)$

Когда тип вывода не зависит от входного значения, тип функции часто просто записывается с помощью $\to$. Таким образом, ${\mathbb {N} }\to {\mathbb {R} }$ — это тип функций преобразования натуральных чисел в действительные числа. Такие П-типы соответствуют логической импликации. Логичное предложение $A\implies B$ соответствует типу $A\to B$, содержащий функции, которые принимают доказательства A и возвращают доказательства B. Более последовательно этот тип можно было бы записать так:

$\prod _{a{\mathbin {:}}A}B$

П-типы также используются в логике для количественной оценки универсальности . Утверждение «для каждого $n$ типа ${\mathbb {N} }$, $P(n)$ доказано» становится функцией от $n$ типа ${\mathbb {N} }$ доказательствам $P(n)$. Таким образом, учитывая значение $n$ функция генерирует доказательство того, что $P(\,\cdot \,)$ имеет место для этого значения. Тип будет

$\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

= конструктор типа

=-типы создаются из двух терминов. Учитывая два термина типа $2+2$ и $2\cdot 2$, вы можете создать новый тип $2+2=2\cdot 2$. Термины этого нового типа представляют собой доказательство того, что пара сводится к одному и тому же каноническому термину. Таким образом, поскольку оба $2+2$ и $2\cdot 2$ вычислить канонический член $4$, будет терм типа $2+2=2\cdot 2$. В интуиционистской теории типов существует единственный способ введения =-типов — посредством рефлексивности :

$\operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).$

Можно создавать =-типы, такие как $1=2$ где термины не сводятся к одному и тому же каноническому термину, но вы не сможете создавать термины этого нового типа. Фактически, если бы вы смогли создать термин $1=2$, вы можете создать термин $\bot$. Помещение этого в функцию создаст функцию типа $1=2\to \bot$. С $\ldots \to \bot$ как интуиционистская теория типов определяет отрицание, вы бы получили $\neg (1=2)$ или, наконец, $1\neq 2$.

Равенство доказательств является областью активных исследований в теории доказательств и привело к развитию теории гомотопических типов и других теорий типов.

Индуктивные типы

Основная статья: Индуктивный тип

Индуктивные типы позволяют создавать сложные самореферентные типы. Например, связанный список натуральных чисел — это либо пустой список, либо пара натурального числа и другого связанного списка. Индуктивные типы можно использовать для определения неограниченных математических структур, таких как деревья , графики и т. д. Фактически, тип натуральных чисел может быть определен как индуктивный тип, либо $0$ или преемник другого натурального числа.

Индуктивные типы определяют новые константы, такие как ноль. $0{\mathbin {:}}{\mathbb {N} }$ и функция-преемник $S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }$. С $S$ не имеет определения и не может быть оценен с помощью замены, такие термины, как $S0$и $SSS0$ стать каноническими членами натуральных чисел.

Доказательства индуктивных типов возможны благодаря индукции . Каждый новый тип индуктивности имеет свое собственное правило индуктивности. Чтобы доказать предикат $P(\,\cdot \,)$ для каждого натурального числа вы используете следующее правило:

${\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)$

Индуктивные типы в интуиционистской теории типов определяются в терминах W-типов, типа хорошо обоснованных деревьев. Более поздние работы по теории типов породили коиндуктивные типы, индукцию-рекурсию и индукцию-индукцию для работы с типами с более неясными видами самореференции. Более высокие индуктивные типы позволяют определять равенство между членами.

Типы юниверсов

Типы юниверсов позволяют писать доказательства для всех типов, созданных с помощью других конструкторов типов. Каждый термин во вселенной типа ${\mathcal {U}}_{0}$ может быть сопоставлен с типом, созданным с любой комбинацией $0,1,2,\Sigma ,\Pi ,=,$ и конструктор индуктивного типа. Однако, во избежание парадоксов, термина в ${\mathcal {U}}_{n}$ это соответствует ${\mathcal {U}}_{n}$ для любого ${\mathcal {n}}\in \mathbb {N}$.

Писать доказательства обо всех «мелких типах» и ${\mathcal {U}}_{0}$, вы должны использовать ${\mathcal {U}}_{1}$, который содержит термин для ${\mathcal {U}}_{0}$, но не для себя ${\mathcal {U}}_{1}$. Аналогично, для ${\mathcal {U}}_{2}$. Существует предикативная иерархия вселенных, поэтому для количественной оценки доказательства по любой фиксированной константе $k$ вселенные, вы можете использовать ${\mathcal {U}}_{k+1}$.

Типы юниверсов — сложная особенность теорий типов. Первоначальную теорию типов Мартина-Лёфа пришлось изменить, чтобы учесть парадокс Жирара . Более поздние исследования охватывали такие темы, как «супервселенные», « вселенные Мало » и непредикативные вселенные.

Суждения

Формальное определение интуиционистской теории типов записано с использованием суждений. Например, в утверждении «если $A$ это тип и $B$ тогда это тип $\textstyle \sum _{a:A}B$ есть тип» существуют суждения «является типом», «и» и «если... то...». Выражение $\textstyle \sum _{a:A}B$ не является приговором; это определяемый тип.

Этот второй уровень теории типов может сбивать с толку, особенно когда речь идет о равенстве. Существует суждение о равенстве терминов, которое могло бы сказать $4=2+2$. Это утверждение, что два термина сводятся к одному и тому же каноническому термину. Существует также суждение о равенстве типов, скажем, что $A=B$, что означает каждый элемент $A$ является элементом типа $B$ и наоборот. На уровне типа существует тип $4=2+2$ и он содержит термины, если есть доказательство того, что $4$ и $2+2$ уменьшить до того же значения. (Термины этого типа генерируются с использованием суждения о термине-равенстве.) Наконец, существует англоязычный уровень равенства, поскольку мы используем слово «четыре» и символ « $4$"для обозначения канонического термина $SSSS0$. Подобные синонимы Мартин-Лёф называет «определенно равными».

Описание судебных решений, приведенное ниже, основано на обсуждении дел Нордстрема, Петерссона и Смита.

Формальная теория работает с типами и объектами .

Тип объявляется:

• $A\ {\mathsf {Type}}$

Объект существует и находится в определенном типе, если:

• $a{\mathbin {:}}A$

Объекты могут быть равными

• $a=b$

и типы могут быть равными

• $A=B$

Объявляется тип, который зависит от объекта другого типа.

• $(x{\mathbin {:}}A)B$

и удаляется заменой

• $B[x/a]$, заменив переменную $x$ с объектом $a$ в $B$.

Объект, зависящий от объекта другого типа, можно сделать двумя способами.Если объект «абстрагирован», то пишется

• $[x]b$

и удаляется заменой

• $b[x/a]$, заменив переменную $x$ с объектом $a$ в $b$.

Объектно-зависимый объект также может быть объявлен как константа как часть рекурсивного типа. Пример рекурсивного типа:

• $0{\mathbin {:}}\mathbb {N}$
• $S{\mathbin {:}}\mathbb {N} \to \mathbb {N}$

Здесь, $S$ является постоянным объектом, зависящим от объекта. Это не связано с абстракцией.Константы типа $S$ можно удалить, определив равенство. Здесь связь со сложением определяется с использованием равенства и сопоставления с образцом для обработки рекурсивного аспекта. $S$:

${\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}$

$S$ манипулируется как непрозрачная константа — у нее нет внутренней структуры для замены.

Итак, объекты, типы и эти отношения используются для выражения формул в теории. Следующие стили суждений используются для создания новых объектов, типов и отношений из существующих:

$\Gamma \vdash \sigma \ {\mathsf {Type}}$	σ — корректный тип в контексте Γ.
$\Gamma \vdash t{\mathbin {:}}\sigma$	t — корректный терм типа σ в контексте Γ.
$\Gamma \vdash \sigma \equiv \tau$	σ и τ — равные типы в контексте Γ.
$\Gamma \vdash t\equiv u{\mathbin {:}}\sigma$	t и u являются оценочно равными терминами типа σ в контексте Γ.
$\vdash \Gamma \ {\mathsf {Context}}$	Γ — это хорошо сформированный контекст предположений о типизации.

По соглашению существует тип, который представляет все остальные типы. Это называется ${\mathcal {U}}$ (или $\operatorname {Set}$). С ${\mathcal {U}}$ является типом, его члены являются объектами. Есть зависимый тип $\operatorname {El}$ который сопоставляет каждый объект с соответствующим типом. В большинстве текстов $\operatorname {El}$ никогда не пишется. Из контекста высказывания читатель почти всегда может сказать, $A$ относится к типу или относится к объекту в ${\mathcal {U}}$ что соответствует типу.

Это полная основа теории. Все остальное производное.

Для реализации логики каждому предложению присваивается свой тип. Объекты этих типов представляют собой различные возможные способы доказательства предложения. Если доказательство утверждения отсутствует, то в типе нет объектов. Такие операторы, как «и» и «или», которые работают с предложениями, вводят новые типы и новые объекты. Так $A\times B$ это тип, который зависит от типа $A$ и тип $B$. Объекты этого зависимого типа определены как существующие для каждой пары объектов в $A$ и $B$. Если $A$ или $B$ не имеет доказательства и является пустым типом, тогда новый тип, представляющий $A\times B$ тоже пусто.

Это можно сделать для других типов (логических значений, натуральных чисел и т. д.) и их операторов.

Категориальные модели теории типов

Используя язык теории категорий , РЭГ Сили ввел понятие локально декартовой замкнутой категории (LCCC) как базовую модель теории типов. Хофманн и Дюбьер усовершенствовали это до категорий с семействами или категорий с атрибутами на основе более ранней работы Картмелла.

Категория с семействами — это категория C контекстов (в которой объекты являются контекстами, аморфизмы контекста являются заменами) вместе с функтором T : C ^на → Фам ( Сет ).

Fam ( Set ) — категория семейств Множеств, в которой объекты являются парами ⁠ $(A,B)$⁠ «индексного множества» A и функции B : X → A , а морфизмы — это пары функций f : A → A' и g : X → X' , такие, что B' _° g = f _° B — в других словами, f отображает B _a в B _{g ( a )} .

Функтор T присваивает контексту G множество ⁠ $Ty(G)$⁠ типов, и для каждого ⁠ $A:Ty(G)$⁠ , набор ⁠ $Tm(G,A)$⁠ терминов.Аксиомы функтора требуют, чтобы они гармонично сочетались с заменой. Замена, как правило,записанный в форме Af или af , где A — тип в ⁠ $Ty(G)$⁠ и a - термин в ⁠ $Tm(G,A)$⁠ , а f — заменаот Д до Г. ​Здесь ⁠ $Af:Ty(D)$⁠ и ⁠ $af:Tm(D,Af)$⁠ .

Категория C должна содержать конечный объект (пустой контекст) и конечный объект формы.продукта, называемого пониманием или расширением контекста, в котором правый элемент является типом в контексте левого элемента.Если G — контекст и ⁠ $A:Ty(G)$⁠ , то должен быть объект ⁠ $(G,A)$⁠ финал средиконтексты D с отображениями p : D → G , q : Tm ( D,Ap ).

Логическая структура, такая как у Мартина-Лёфа, принимает формуусловия закрытия контекстно-зависимых наборов типов и терминов: должен существовать тип, называемыйЗадайте, и для каждого набора свой тип, что типы должны замыкаться по формам зависимой суммы ипродукт и так далее.

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

Экстенсиональный и интенсиональный

Фундаментальное различие заключается в теории экстенсионального и интенсионального типа. В теории экстенсионального типа дефинициональное (т. е. вычислительное) равенство не отличается от пропозиционального равенства, которое требует доказательства. Как следствие, проверка типов становится неразрешимой в теории экстенсиональных типов, поскольку программы в этой теории могут не завершиться. Например, такая теория позволяет задать тип Y-комбинатору ; подробный пример этого можно найти в книге Нордстёма и Петерссона «Программирование в теории типов Мартина-Лёфа» . Однако это не мешает теории экстенсиональных типов быть основой практического инструмента; например, Nuprl основан на теории экстенсиональных типов.

в интенсиональной теории типов проверка типов разрешима В отличие от этого , но представление стандартных математических понятий несколько более громоздко, поскольку интенсиональные рассуждения требуют использования сетоидов или подобных конструкций. Существует множество распространенных математических объектов, с которыми сложно работать или которые невозможно представить без этого, например, целые числа , рациональные числа и действительные числа . Целые и рациональные числа можно представить без сетоидов, но с этим представлением сложно работать. Без этого действительные числа Коши представить невозможно.

Теория гомотопических типов работает над решением этой проблемы. Это позволяет определять высшие индуктивные типы , которые определяют не только конструкторы первого порядка ( значения или точки ), но и конструкторы более высокого порядка, т.е. равенства между элементами ( пути ), равенства между равенствами ( гомотопии ), до бесконечности .

Реализации теории типов

Различные формы теории типов были реализованы как формальные системы, лежащие в основе ряда помощников по доказательству . Хотя многие из них основаны на идеях Пера Мартина-Лёфа, многие имеют дополнительные функции, дополнительные аксиомы или другую философскую основу. Например, система Nuprl основана на теории вычислительных типов. и Coq основан на исчислении (ко)индуктивных конструкций . Зависимые типы также используются в дизайне таких языков программирования , как ATS , Cayenne , Epigram , Agda , и Идрис .

Теории типа Мартина-Лёфа

Пер Мартин-Лёф построил несколько теорий типов, которые были опубликованы в разное время, некоторые из них намного позже, чем когда препринты с их описанием стали доступны специалистам (в частности, Жан-Иву Жирару и Джованни Самбену). В приведенном ниже списке предпринята попытка перечислить все теории, описанные в печатной форме, и обрисовать ключевые особенности, отличающие их друг от друга. Все эти теории имели зависимые произведения, зависимые суммы, непересекающиеся объединения, конечные типы и натуральные числа. Все теории имели одинаковые правила приведения, которые не включали η-редукцию ни для зависимых произведений, ни для зависимых сумм, за исключением MLTT79, где добавляется η-редукция для зависимых произведений.

MLTT71 была первой теорией типов, созданной Пером Мартином-Лёфом. Она появилась в препринте в 1971 году. У нее была одна вселенная, но эта вселенная имела само по себе имя, т.е. это была теория типов с, как ее называют сегодня, «Тип в типе». Жан-Ив Жирар показал, что эта система была непоследовательной, и препринт так и не был опубликован.

MLTT72 был представлен в препринте 1972 года, который сейчас опубликован. В этой теории была одна вселенная V и не было типов идентичности (=-типов). Вселенная была « предикативной » в том смысле, что зависимый продукт семейства объектов из V над объектом, которого не было в V, таким как, например, сам V, не предполагался находящимся в V. Вселенная была а-ля Рассела Principia Mathematica , т. е. можно было бы написать напрямую «TεV» и «tεT» (Мартин-Лёф использует знак «ε» вместо современного «:») без дополнительного конструктора, такого как «El».

MLTT73 было первым определением теории типов, опубликованным Пером Мартином-Лёфом (оно было представлено на логическом коллоквиуме '73 и опубликовано в 1975 году). ). Существуют типы идентичности, которые он описывает как «предложения», но поскольку реального различия между предложениями и остальными типами не вводится, смысл этого неясен. Есть то, что позже получит название J-элиминатора, но пока без названия (см. с. 94–95). В этой теории существует бесконечная последовательность вселенных V ₀ , ..., V _n , ... . Вселенные предикативны, в духе Рассела, и некумулятивны . Действительно, следствие 3.10 на с. 115 говорит, что если AεV _m и BεV _n таковы, что A и B конвертируемы, то m = n . Это означает, например, что в этой теории будет сложно сформулировать аксиому однолистности есть сжимаемые типы _{— в каждом из Vi} , но неясно, как объявить их равными, поскольку не существует тождественных типов, связывающих _Vi и V _j для i ≠ j .

MLTT79 был представлен в 1979 году и опубликован в 1982 году. В этой статье Мартин-Лёф представил четыре основных типа суждений теории зависимых типов, которая с тех пор стала фундаментальной в изучении метатеории таких систем. Он также ввел в нее контексты как отдельное понятие (см. с. 161). Существуют тождественные типы с J-элиминатором (который уже появился в MLTT73, но не имел там этого названия), а также с правилом, делающим теорию «экстенсиональной» (с. 169). Есть W-типы. Существует бесконечная последовательность предикативных вселенных, которые накапливаются .

Библиополис обсуждается теория типов . : в книге «Библиополис» 1984 года но он в некоторой степени открыт и, похоже, не представляет собой определенный набор вариантов, поэтому с ним не связана какая-либо конкретная теория типов.

См. также

• Интуиционистская логика
• Типизированное лямбда-исчисление

Ссылки

• Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Самбин, Джон. Неаполь: Библиополис. ISBN  978-8870881059 . ОСЛК   12731401 .

Дальнейшее чтение

• Согласно заметкам Мартина-Лёфа, записанным Джованни Самбином (1980)
• Нордстрем, Бенгт; Петерсон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа . Издательство Оксфордского университета. ISBN  9780198538141 .
• Томпсон, Саймон (1991). Теория типов и функциональное программирование . Аддисон-Уэсли. ISBN  0-201-41667-0 .
• Гранстрем, Йохан Г. (2011). Трактат по интуиционистской теории типов . Бег. ISBN  978-94-007-1735-0 .

Внешние ссылки

• Проект ЕС «Типы»: Учебные пособия – конспекты лекций и слайды с Летней школы «Типы» 2005 г.
• n-Категории - Эскиз определения - письмо Джона Баэза и Джеймса Долана Росс Стрит , 29 ноября 1995 г.