Какова роль двухцветного исчисления конструкций?

Итак, я читаю немного о разработке, в частности, алгоритмах, основанных на двухцветном исчислении конструкции, и я немного запутался. Я не понимаю, какова цель . Кажется, он идентичен за исключением того, что существует различие между неявными и явными аргументами для функций. В частности, я не вижу, как он позволяет писать вместо . Если мы примем систему глобальных определений, то $CC^{bi}$ $CC$ $(id\; 0)$ $(id\; \mathbb{N}\; 0)$

$id : (\Pi A\; |\; \mathsf{Type}\; . (\Pi x : A\; . A))$

а также

$id = (\lambda A\; |\; \mathsf{Type}\; . (\lambda x : A . x))$ .

Правила действительно позволяют ? Конечно, синтаксис есть, но я не вижу его в типизации. Я что-то пропустил? Я неправильно понимаю роль ? $(id\; 0)$ $CC^{bi}$

Кроме того, не потеряно ли свойство слияния? Думаю, моя проблема в том, что я читаю о разработке, не читая много о до этого. Какая хорошая статья, которая представляет это и это один? $CC^{bi}$

Изменить: Чтобы быть более точным, я спрашиваю, как принимается вместо когда правила для явного и неявного приложения идентичны по модулю sytnax , Я не вижу разницы между иправила для обоих кажутся одинаковыми. $(id\; 0)$ $(id\; \mathbb{N}\; 0)$ $\Pi$ $:$ $|$

Изменить: я не говорю о неявном исчислении конструкций, который является другой теорией и имеет разные правила для явных (приложение против поколения.) $\Pi$

Изменить: Хорошо, я думаю, что я начинаю понимать это, но я не буду отвечать на этот вопрос, пока я не уверен. По сути не проверяет тип, и фактически он просто разработан для непосредственно перед проверкой типа или выполнен как вторичная ответственность алгоритма проверки типа. По сути, эти неявные исчисления предназначены для языков интерфейса (пользовательского), которые разрабатываются в обычные (явные) исчисления или, по крайней мере, в явный фрагмент неявных исчислений перед проверкой типов. Если это так, то я думаю, что вижу общую картину. Может кто-нибудь, пожалуйста, подтвердите это? $(id\; 0)$ $(id\; \mathbb{N}\; 0)$

type-theory lambda-calculus type-inference dependent-type Энтони
источник

Как я уже говорил ниже, ваша интуиция верна: двухцветное исчисление конструкций является явным исчислением, в котором аргументы, опущенные пользователем, но разработанные «внешним интерфейсом», явно помечены. Кроме того, слияние теряется при сокращении бета + эта, но верно, если оно ограничено только бета.

Коди

В «Неявном исчислении конструкций, расширяющем системы чистого типа с помощью связующего и подтипов типов пересечений» , Александр Микель представляет основные понятия для неявного исчисления конструкций, которые, как я полагаю, являются синонимом двухцветного исчисления конструкций.

Суть в том, чтобы (помимо всего прочего) иметь исчисление без беспорядка явных аннотаций типов везде. Вывод типа (весьма вероятно) неразрешим.

В этом исчислении, если мы возьмем , тогда вы можете получить просто используя явный продукт и неявные правила продукта в последовательности. Тогда правило инстанцирования для неявного продукта позволяет и т. Д. Система допускает сокращение и слияние даже на нетипизированных терминах (что на самом деле не подходит для исчислений с аннотациями абстракции). ). Все это можно найти в диссертации Александра, к сожалению, на французском языке. Не уверен, что у меня есть лучший справочник для этих результатов, хотя я боюсь. $id=\lambda x. x$

⊢ i d : \forall X : T y p e . X \to X

$\vdash id\colon \forall X\colon Type. X\rightarrow X$

⊢ i d : N a t \to N a t

$\vdash id\colon Nat\rightarrow Nat$

⊢ i d 0 : N a t

$\vdash id\ 0 \colon Nat$

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

Первую часть вашего ответа я знаю, но думаю, что должен был быть более конкретным в своем первоначальном вопросе. То есть как именно (id 0) допускается, если id имеет тип (\ Pi X | Type. X -> X), потому что кажется, что правило APP одинаково как для неявного, так и для явного \ Pi. В неявном исчислении конструкций, которое на самом деле является другой теорией, это не так, потому что оно разделено на APP и GEN. Чтобы убедиться, что это не так, проверьте заголовок «Исчисление с« действительно неявными »аргументами» в статье, на которую вы ссылались.

Энтони

По поводу разрешимости. Документ, на который вы ссылаетесь, предполагает, что его теория неразрешима. В статье, на которую она ссылается (я полагаю, «оригинальное» двухцветное исчисление бумаги конструкций), утверждается, что она разрешима, но явно не доказывает это. Я прочитал его после того, как опубликовал этот вопрос, и кажется, что он определенно должен быть разрешимым и в зависимости от синтаксических ограничений сохранять слияние. С другой стороны, я все еще застрял в своем первоначальном замешательстве: \

Энтони

Может быть, вы должны сказать нам, на какую бумагу вы смотрите.

Коди

Хорошо, я взглянул на разработку и стирание в теории типов Марко Лютера, который, как я полагаю, является вашей ссылкой. В этом случае нет семантической разницы между явным и неявным произведением, и действительно, двухцветная система является консервативным расширением исчисления конструкций. Что происходит, так это то, что вы используете разработку, чтобы взять термин без явного аргумента, чтобы превратить его в полностью аннотированный термин: id !1 0уточняется до id Nat 0. В этом тексте проработка

описана

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

C C^{b i}

$CC^{bi}$

Энтони

Какова роль двухцветного исчисления конструкций?

Ответы: