Вопросы с тегом «type-theory»

19
Зачем двоеточию обозначать, что значение принадлежит типу?

Пирс (2002) вводит отношение типирования на странице 92, записывая: Отношение типа для арифметических выражений, написанное «t: T», определяется набором правил вывода, назначающих типы терминам и сноска говорит, что символ часто используется вместо:. Мой вопрос просто, почему теоретики типов...

18
Funsplit и полярность Pi-типов

В недавнем потоке в списке рассылки Агда, вопрос - законов выскочил, в котором Питер Hancock сделал заставляющий думать замечание .ηη\eta Насколько я понимаю, законы приходят с отрицательными типами, т.е. связующие, правила введения которых обратимы. Чтобы отключить для функций, Хэнк предлагает...

18
Неявный или явный подтип

Эта страница утверждает, что многие языки не используют неявный подтип (структурная эквивалентность), предпочитая явный / объявленный подтип (декларационная эквивалентность) Я в основном использовал языки программирования, которые используют явные подтипы . Каковы преимущества неявного...

18
Доказать доказательство неуместности в Coq?

Есть ли способ доказать следующую теорему в Coq? Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2. РЕДАКТИРОВАТЬ : Попытка дать краткое объяснение «что такое доказательство неуместности» (поправьте меня, если я ошибаюсь или неточен) Основная идея заключается в том, что в мире...

18
Классификация типизированных / нетипизированных лямбда-исчислений

Может кто-нибудь объяснить кратко (если это возможно!) Или отослать меня к ссылке, обобщающей различия между нетипизированным лямбда-исчислением и более распространенным типизированным лямбда-исчислением? Я особенно ищу заявления об их выразительной силе, эквивалентности логическим / арифметическим...

17
Почему невозможно объявить индуктивный принцип для церковных цифр

Представьте себе, мы определили натуральные числа в лямбда-исчислении с зависимой типизацией как церковные цифры. Они могут быть определены следующим образом: SimpleNat = (R : Set) → R → (R → R) → R zero : SimpleNat zero = λ R z _ → z suc : SimpleNat → SimpleNat suc sn = λ R z s → s (sn R z s)...

17
Какова категориальная семантика подтипов?

Начиная с Curry-Howard-Lambek, было триединство теорий типов, логик и категорий. Мне любопытно, какую категоричную семантику вы получаете, когда добавляете (принудительный) подтип в теорию типов - кажется, что это не очень изучалось, если вообще. В целом, добавление коэрцитивного подтипирования в...

16
Ищу Скотта оригинальную бумагу LCF

Доступна ли следующая рукопись публично? Дана Скотт, 1969, Теория вычислимых функций высшего типа . Неопубликованные заметки семинара, 7 страниц, Оксфордский университет. Эта статья обсуждается в разделе 8.1.2, Типы как множества , в Cardone & Hindley, 2006 История лямбда-исчисления и...

16
Формализация теории гомотопического типа в Идрисе

Глядя на блог по теории гомотопических типов, можно легко найти множество библиотек, формализующих большую часть теории гомотопических типов в Agda и Coq. Кто-нибудь знает, есть ли подобная попытка формализовать HoTT в Идрисе...

16
Можем ли мы доказать слабую нормализацию для системы F индукцией по трансфинитному ординалу

Слабая нормализация для простого типизированного лямбда-исчисления может быть доказана (Тьюринг) индукцией по . Расширенное лямбда-исчисление с рекурсорами на натуральные числа (Генцен) имеет слабую стратегию нормализации по индукции на ϵ 0 .ω2ω2\omega^2ϵ0ϵ0\epsilon_0 А как насчет системы F (или...

16
Какова роль предикативности в индуктивных определениях в теории типов?

Мы часто хотим определить объект соответствии с некоторыми правилами вывода. Эти правила обозначают производящую функцию F , которая, когда она монотонна, возвращающую мере неподвижную точку М F . Возьму А : = μ F , чтобы быть «индуктивным определением» А . Кроме того, монотонность F позволяет нам...

15
Как можно мотивировать реляционную параметричность?

Есть ли какой-то естественный способ понять сущность реляционной семантики для параметрического полиморфизма? Я только начал читать о понятии реляционной параметричности, а именно «Типах, абстракциях и параметрическом полиморфизме» Джона Рейнольдса, и у меня возникают проблемы с пониманием...

15
Почему конструктивисты не слишком заботятся о call / cc

Итак, некоторое время назад я сначала попросил кого-то сказать мне, что call / cc может разрешить объекты доказательства для классических доказательств путем реализации закона Пирса. Недавно я немного подумал над этой темой и не могу найти в ней недостаток. Однако я не могу видеть, чтобы кто-то еще...

15
Может ли булева алгебра быть выражена в просто типизированной лямбда-какклус?

Таким образом, булева алгебра может быть выражена в нетипизированном лямбда-исчислении . true = \t. \f. t; false = \t. \f. t; not = \x. x false true; and = \x. \y. x y false; or = \x. \y. x true y; Также булева алгебра может быть закодирована в Системе F следующим образом : CBool = All X.X -> X...

15
Структуры данных в языке программирования с линейными типами

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

15
Доказательство теории бипродуктов?

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

14
Относительная согласованность PA и некоторые теории типов

Для теории типов под последовательностью я подразумеваю, что у нее есть тип, который не заселен. Из сильной нормализации лямбда-куба следует, что система FFF и система FωFωF_\omega согласованы. MLTT + индуктивные типы также имеют доказательство нормализации. Однако все они должны быть достаточно...

14
Логические соотношения для предиктивной системы в предикативной мета-теории

Логические отношения для непредсказуемых языков, таких как Система F, похоже, критически полагаются на непредсказуемость внешней логики. В частности, интерпретация для типа Форалла будет определяться в терминах всех типизированных отношений. В непредсказуемой системе (например, CiC / Coq) это...

14
В книге Hott, является ли большинство типов формирователей избыточными? И если так, то почему?

В главе 1 и Приложении A к книге Hott представлены несколько семейств примитивных типов (типы юниверсов, зависимые типы функций, типы зависимых пар, типы копроизведения, пустой тип, тип блока, тип натурального числа и типы идентификаторов), образующие основу для теории гомотопического типа. Однако...