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

В недавнем потоке в списке рассылки Агда, вопрос - законов выскочил, в котором Питер Hancock сделал заставляющий думать замечание .$\eta$

Насколько я понимаю, законы приходят с отрицательными типами, т.е. связующие, правила введения которых обратимы. Чтобы отключить для функций, Хэнк предлагает использовать специальный элиминатор funsplit вместо обычного правила приложения. Я хотел бы понять замечание Хэнка с точки зрения полярности.$\eta$$\eta$

Например, есть две презентации -types. Существует традиционный Martin-Löf сплит нейтрализатор, в позитивном стиле:$\Sigma$

$$\begin{array}{l} \Gamma \vdash f : (a : A)(b : B\: a) \to C (a , b) \\ \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \mathrm{split}\: f\: p : C\: p \end{array}$$

И есть отрицательная версия:

$$\begin{array}{l} \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \pi_0\: p : A \end{array} \qquad \begin{array}{l} \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \pi_1\: p : B[\pi_0\: p / a] \end{array}$$

Последнее представление позволяет легко получить для пар, т.е. для любой пары (где == обозначает равенство определений). С точки зрения доказуемости это различие не имеет значения: интуитивистски можно реализовать проекции с разбивкой или наоборот.$\eta$$(\pi_0 p , \pi_1 p) == p$$p$

Теперь, -типы обычно (и неоспоримый, я считаю) негативно воспринят:$\Pi$

$$\begin{array}{l} \Gamma \vdash f : \Pi a : A. B \\ \Gamma \vdash s : A \\ \hline \\ \Gamma \vdash f s : B[s / a] \end{array}$$

Что дает нам для функций: .$\eta$$\lambda x. f x == f$

Тем не менее, в этом письме Хэнк вспоминает элиминатор funsplit (Программирование в теории типов ML, [http://www.cse.chalmers.se/research/group/logic/book/], стр. 56). Это описывается в логической структуре:

$$\begin{array}{l} f \in \Pi(A, B) \\ C(v)\: Set [v \in \Pi(A, B)] \\ d(y) \in C(\lambda(y)) [y(x) \in B(x) [x \in A]] \\ \hline \\ \mathrm{funsplit}(f, d) \in C(f) \end{array}$$

Интересно, что Nordstrom et al. мотивировать это определение, сказав, что «[эта] альтернативная неканоническая форма основана на принципе структурной индукции». Это утверждение сильно пахнет позитивом: функции будут «определены» их конструктором .$\lambda$

Тем не менее, я не могу достаточно точно описать это правило в естественной дедукции (или, что еще лучше, в последовательном исчислении). (Ab) использование логического каркаса для введения представляется здесь решающим.$y$

Итак, является ли funsplit позитивным представлением -типов? Есть ли у нас что-то похожее в (независимом) исчислении секвенций? Как бы это выглядело?$\Pi$

Насколько распространено / любопытно это для теоретиков доказательства в этой области?

Представление функциональной элиминации с использованием определенно не является обычным явлением в большинстве методов теории типов. Однако я считаю, что эта форма действительно является «позитивным» представлением об устранении функциональных типов. Проблема здесь в том, что вам нужна форма соответствия шаблону высшего порядка, см., Например, Дейл Миллер .$\mathrm{funsplit}$

Позвольте мне переформулировать ваше правило более понятным для меня способом:

$$\begin{array}{l} \Gamma\vdash f : \Pi x:A. B \\ \Gamma, z:\Pi x:A. B\vdash C : Set\\ \Gamma, [x:A]F(x):B\vdash e : C\{\lambda x:A.F(x)/z\}\\ \hline \\ \mathrm{match}\ f\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e : C\{f/z\} \end{array}$$

Там , где представляет собой мета-переменная типа в контексте .B x : $F$$B$$x:A$

Правило переписывания становится:

$$\mathrm{match}\ \lambda x:A.t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e\quad \rightarrow\quad e\{t\{u/x\}/F(u)\}$$

Это позволяет вам определить приложение как:

$$\mathrm{app}(t,u)=\mathrm{match}\ t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow F(u)$$

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

Однако есть место, где в литературе присутствует положительное / отрицательное различие: формулировка предикатов логических отношений . Два возможных определения (в унарном случае)

$$[\![\Pi x:A.B]\!] = \{t\mid \forall u\in [\![ A]\!], tu \in[\![B]\!]_{x\mapsto u} \}$$

и

$$[\![\Pi x:A.B]\!] = \{t\mid t\rightarrow^* \lambda x.t', \forall u\in[\![A]\!], t'\{u/x\}\in[\![B]\!]_{x\mapsto u}\}$$

Вторая версия менее распространена, но ее можно найти, например, в Dowek и Werner .

Вот немного другой взгляд на ответ Фредрика. Как правило, случайные церковные кодировки типов удовлетворяют соответствующим законам , но не удовлетворяют законам .$\beta$$\eta$

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

л 1 л 1 : ∃ х : Х

$$\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha$$ Теперь, обратите внимание , что легко определимы: Однако вы не можете определить вторую проекцию - попробуйте! Вы можете определить только слабый элиминатор для этого, поэтому я написал это с экзистенциальным.$\pi_1$тг 2 : П р : ( ∃ х : Х $$\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)$$ $\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$

Однако вторая проекция реализуема , и в параметрической модели вы можете показать, что она также имеет правильное поведение. (См. Мой недавний проект с Дереком Дрейером о параметричности в исчислении конструкций, чтобы узнать больше об этом.) Поэтому я думаю, что проекция фундаментально требует некоторых сильных свойств экстенсиональности, чтобы иметь смысл.$\pi_2$

В терминах последовательного исчисления слабый элиминатор имеет правило, которое выглядит примерно так:

pΓ′CΓ,x:X,y:Y[x]

$$\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C} {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}$$ Здесь неявные условия правильной формы подразумевают, что не может быть свободным в или . Если мы ослабим это условие, мы получим правило разделения, которое имеет левое правило, которое выглядит как Эта замена очень напоминает мне правило исключения Жирара / Шредера-Хейстера для равенства. Я задала вопрос$p$$\Gamma'$$C$ $$\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C} {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}$$ об этом правиле некоторое время назад, и Дэвид Баэлде и Гопалан Надатур дают современную версию в своей статье LICS 2012 « Объединение модуля вычета и логики определений с фиксированной точкой» . Я думаю, что Конор МакБрайд потратил некоторое время на размышления о связи между типом идентичности и равенством Шредера-Хейстера, так что вы можете захотеть увидеть, что он думает.

Ричард Гарнер написал хорошую статью о применении против funsplit, О силе зависимых продуктов в теории типов Мартина-Лёфа (APAL 160 (2009)), в которой также обсуждается природа высшего порядка правила funsplit (со ссылкой на Питер Шредер-Хейстер. Естественное продолжение естественного дедукции (JSL 49 (1984))).

Ричард показывает, что при наличии типов идентичности (а также правил формирования и введения для типов ) funsplit является взаимозависимым с правилом приложения выше + пропозициональная эта, то есть следующие два правила: $\Pi$

$$\frac{m : \Pi(A,B)}{\eta(m) : \mathsf{Id}_{\Pi(A,B)}(m, \lambda x . m\cdot x)} \qquad (\Pi\text{-Prop-$\eta$)}$$ $$\frac{x : A \vdash f(x) : B(x)}{\eta(\lambda(f)) = \mathsf{refl}(\lambda(f)) : \mathsf{Id}_{\Pi(A,B)}(\lambda(f), \lambda (f))} \qquad (\Pi\text{-Prop-$\eta$-Comp)}$$

То есть, если у вас есть funsplit, вы можете определить application и как указано выше, чтобы . Что еще интереснее, если у вас есть приложение и правила предложения, то вы можете определить funsplit.$\eta$$(\Pi\text{-Prop-$\eta$-Comp})$

Кроме того, funsplit строго сильнее приложения: правила пропационного эта не определимы в теории с единственным применением - следовательно, фунсплит не определим, так как тогда и правила пропа будут также. Интуитивно понятно, что это потому, что правила приложения дают вам немного больше времени: в отличие от funsplit (и т. Д.), Они не сообщают вам, что такое функции, а только то, что их можно применять к аргументам. Я считаю, что аргумент Ричарда можно повторить и для типов , чтобы показать тот же результат для против проекций.$\Sigma$$\mathsf{split}$

Обратите внимание, что если бы у вас были определенные правила eta, вы бы наверняка использовали их и пропозиционально (с ). Таким образом, я думаю, что ваши утверждения «[...] которые дают нам для функций» и «[...] эта последняя презентация облегчает получение для пар» неверны. Agda, однако, реализует как для функций, так и для пар (если определена как запись), но это не следует только из приложения.$\eta(m) := \mathsf{refl}(m)$$\eta$$\eta$$\eta$$\Sigma$