Индукция-индукция - Induction-induction

,

Эта статья поднимает множество проблем. Пожалуйста помоги Улучши это или обсудите эти вопросы на страница обсуждения. (Узнайте, как и когда удалить эти сообщения-шаблоны) Эта статья нужны дополнительные цитаты для проверка. Пожалуйста помоги улучшить эту статью к добавление цитат в надежные источники. Материал, не полученный от источника, может быть оспорен и удален. Найдите источники: «Индукция-индукция»  – Новости  · газеты  · книги  · ученый  · JSTOR (Сентябрь 2018 г.) (Узнайте, как и когда удалить этот шаблон сообщения) Эта статья может быть слишком техническим для большинства читателей, чтобы понять. Пожалуйста помогите улучшить это к сделать понятным для неспециалистов, не снимая технических деталей. (Сентябрь 2018 г.) (Узнайте, как и когда удалить этот шаблон сообщения) Эта статья или раздел могло быть скопировал и вставил из другого места, возможно в нарушение Политика Википедии в отношении авторских прав. Пожалуйста ознакомтесь https://cs.stackexchange.com/questions/64130/what-is-induction-induction/64139  (DupDet · CopyVios) и исправить это отредактировав эту статью, чтобы удалить любой несвободный контент, защищенный авторским правом, и правильно указав бесплатный контент, или пометив контент для удаления. Убедитесь, что предполагаемый источник нарушения авторских прав не является Зеркало Википедии. (Ноябрь 2018 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

В интуиционистская теория типов (ITT), некоторая дисциплина внутри математическая логика, индукционно-индукционный предназначен для одновременного объявления некоторого индуктивного типа и некоторого индуктивного предиката над этим типом.

An индуктивное определение задается правилами генерации элементов некоторого типа. Затем можно определить некоторый предикат для этого типа, предоставив конструкторы для формирования элементов предиката, например, индуктивно по способу генерации элементов типа. Индукция-индукция обобщает эту ситуацию, так как можно одновременно определить тип и предикат, потому что правила генерации элементов типа ${ displaystyle A: { mathsf {Тип}}}$ разрешено ссылаться на предикат ${ displaystyle B: от A до { mathsf {Type}}}$.

Индукция-индукция может использоваться для определения более крупных типов, включая различные конструкции вселенной в теории типов.^[1] и предельные конструкции в теории категорий / топосов.

Пример 1

Представьте тип ${ displaystyle A}$ имея следующие конструкторы, обратите внимание на раннюю ссылку на предикат ${ displaystyle B}$ :

• ${ displaystyle aa: A}$
• ${ Displaystyle ell ell: prod _ {x: A} B (x) to A;}$

и одновременно представить сказуемое ${ displaystyle B}$ как имеющие следующие конструкторы:

• ${ displaystyle { mathsf {Tru}}: B (аа)}$
• ${ displaystyle { mathsf {Fal}}: B (аа)}$
• если ${ displaystyle x: A}$ и ${ displaystyle y: B (x)}$ тогда ${ displaystyle { mathsf {Zer}}: B ( ell ell (x, y))}$
• если ${ displaystyle x: A}$ и ${ displaystyle y: B (x)}$ и ${ Displaystyle Z: B ( ell ell (х, y))}$ тогда ${ displaystyle { mathsf {Suc}} (z): B ( ell ell (x, y))}$.

Пример 2

Простым распространенным примером является преобразователь типа Вселенная а ля Тарский. Создает какой-то индуктивный тип ${ displaystyle U: { mathsf {Тип}}}$ и некоторый индуктивный предикат ${ displaystyle T: U to { mathsf {Type}}}$. Для каждого типа в теории типов (кроме ${ displaystyle U}$ сам!), будет какой-то элемент ${ displaystyle U}$ который можно рассматривать как некоторый код для этого соответствующего типа; Предикат ${ displaystyle T}$ индуктивно кодирует каждый возможный тип в соответствующий элемент ${ displaystyle U}$ ; и построение новых кодов в ${ displaystyle U}$ потребует ссылки на тип декодирования более ранних кодов через предикат ${ displaystyle T}$ .

Смотрите также

• Индукция-рекурсия - для одновременного объявления некоторого индуктивного типа и некоторой рекурсивной функции на этом типе.

Рекомендации

внешняя ссылка

• Список публикаций Питера Дайбьера по индукции и индукции-рекурсии