Каппа-исчисление

В математической логике , теории категорий и информатика , каппа-исчисление - это формальная система определения первого порядка функций .

В отличие от лямбда-исчисления , каппа-исчисление не имеет функции высшего порядка ; его функциине первоклассные объекты . Каппа-исчисление может бытьрассматривается как «переформулировка фрагмента первого порядка типизированноголямбда-исчисление».

Поскольку его функции не являются первоклассными объектами, оценка каппаматематические выражения не требуют закрытия .

Определение

Приведенное ниже определение было адаптировано на основе диаграмм Хасэгавы на страницах 205 и 207.

Грамматика

Каппа-исчисление состоит из типов и выражений, заданныхграмматика ниже:

$\tau =1\mid \tau \times \tau \mid \ldots$

$e=x\mid id_{\tau }\mid !_{\tau }\mid \operatorname {lift} _{\tau }(e)\mid e\circ e\mid \kappa x:1{\to }\tau .e$

Другими словами,

• 1 это тип
• Если $\tau _{1}$ и $\tau _{2}$ тогда это типы $\tau _{1}\times \tau _{2}$ это тип.
• Каждая переменная является выражением
• Если τ — тип, то $id_{\tau }$ это выражение
• Если τ — тип, то $!_{\tau }$ это выражение
• Если τ — тип, а e — выражение, то $\operatorname {lift} _{\tau }(e)$ это выражение
• Если $e_{1}$ и $e_{2}$ тогда это выражения $e_{1}\circ e_{2}$ это выражение
• Если x — переменная, τ — тип, а e — выражение, то $\kappa x{:}1{\to }\tau \;.\;e$ это выражение

The $:1{\to }\tau$ и индексы id , ! , и $\operatorname {lift}$ являютсяиногда опускаются, если их можно однозначно определить изконтекст.

Сопоставление часто используется как сокращение для комбинации $\operatorname {lift}$ и состав:

$e_{1}e_{2}\ {\overset {\operatorname {def} }{=}}\ e_{1}\circ \operatorname {lift} (e_{2})$

Правила набора текста

В представлении здесь используются секвенции ( $\Gamma \vdash e:\tau$), а не гипотетические суждения, чтобы облегчить сравнение с просто типизированным лямбда-исчислением. Для этого требуется дополнительное правило Var, которого нет в Hasegawa.

В каппа-исчислении выражение имеет два типа: тип источника и тип цели . Обозначения $e:\tau _{1}{\to }\tau _{2}$ используется для указания того, что выражение e имеет тип источника ${\tau _{1}}$ и тип цели ${\tau _{2}}$.

Выражениям в каппа-исчислении присваиваются типы в соответствии со следующими правилами:

${x{:}1{\to }\tau \;\in \;\Gamma } \over {\Gamma \vdash x:1{\to }\tau }$	(был)
${} \over {\vdash id_{\tau }\;:\;\tau \to \tau }$	(Идентификатор)
${} \over {\vdash !_{\tau }\;:\;\tau \to 1}$	(Хлопнуть)
${\Gamma \vdash e_{1}{:}\tau _{1}{\to }\tau _{2}\;\;\;\;\;\;\Gamma \vdash e_{2}{:}\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{\to }\tau _{3}}$	(Комп)
${\Gamma \vdash e{:}1{\to }\tau _{1}} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}$	(Поднимать)
${\Gamma ,\;x{:}1{\to }\tau _{1}\;\vdash \;e:\tau _{2}{\to }\tau _{3}} \over {\Gamma \vdash \kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}}$	(Каппа)

Другими словами,

• Было: если предположить $x:1{\to }\tau$ позволяет вам сделать вывод, что $x:1{\to }\tau$
• Id: для любого типа τ , $id_{\tau }:\tau {\to }\tau$
• Взрыв: любого типа τ для $!_{\tau }:\tau {\to }1$
• Comp: если целевой тип $e_{1}$ соответствует типу источника $e_{2}$ они могут быть составлены так, чтобы сформировать выражение $e_{2}\circ e_{1}$ с типом источника $e_{1}$ и целевой тип $e_{2}$
• Лифт: если $e:1{\to }\tau _{1}$, затем $\operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})$
• Каппа: если мы сможем заключить, что $e:\tau _{2}\to \tau _{3}$ в предположении, что $x:1{\to }\tau _{1}$ мы можем заключить, , то без этого предположения что $\kappa x{:}1{\to }\tau _{1}\,.\,e\;:\;\tau _{1}\times \tau _{2}\to \tau _{3}$

Равенства

Каппа-исчисление подчиняется следующим равенствам:

• Нейтралитет: если $f:\tau _{1}{\to }\tau _{2}$ затем $f{\circ }id_{\tau _{1}}=f$ и $f=id_{\tau _{2}}{\circ }f$
• Ассоциативность: Если $f:\tau _{1}{\to }\tau _{2}$, $g:\tau _{2}{\to }\tau _{3}$, и $h:\tau _{3}{\to }\tau _{4}$, затем $(h{\circ }g){\circ }f=h{\circ }(g{\circ }f)$.
• Терминальность: Если $f{:}\tau {\to }1$ и $g{:}\tau {\to }1$ затем $f=g$
• Лифт-Уменьшение: $(\kappa x.f)\circ \operatorname {lift} _{\tau }(c)=f[c/x]$
• Каппа-редукция: $\kappa x.(h\circ \operatorname {lift} _{\tau }(x))=h$ если x не свободен в h

Последние два равенства представляют собой правила редукции исчисления:переписываем слева направо.

Свойства

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

Выражения с типом $1{\to }\tau$ можно рассматривать как «константы» или значения «типа земли»; это потому, что 1 — это тип единицы, и поэтому функция этого типа обязательно является постоянной функцией. Обратите внимание, что правило каппы допускает абстракции только в том случае, если абстрагируемая переменная имеет тип $1{\to }\tau$ для некоторого τ . Это базовый механизм, который гарантирует, что все функции имеют первый порядок.

Категориальная семантика

Каппа-исчисление задумано как внутренний язык контекстуально полные категории.

Примеры

Выражения с несколькими аргументами имеют исходные типы, которые«правонесбалансированные» бинарные деревья. Например, функция f с тремяаргументы типов A, B и C и тип результата D будут иметь тип

$f:A\times (B\times (C\times 1))\to D$

Если мы определим левоассоциативное сопоставление $f\;c$ как аббревиатурадля $(f\circ \operatorname {lift} (c))$, тогда – предполагая, что $a:1{\to }A$, $b:1{\to }B$, и $c:1{\to }C$ – мы можем применить эту функцию:

$f\;a\;b\;c\;:\;1\to D$

Поскольку выражение $f\;a\;b\;c$ имеет исходный тип 1 , это «основное значение» и может быть передано в качестве аргумента другой функции. Если $g:(D\times E){\to }F$, затем

$g\;(f\;a\;b\;c)\;:\;E\to F$

Очень похоже на каррированную функцию типа $A{\to }(B{\to }(C{\to }D))$ в лямбда-исчислении, частичноевозможно применение:

$f\;a\;:\;B\times (C\times 1)\to D$

Однако никакие более высокие типы (т.е. $(\tau {\to }\tau ){\to }\tau$) участвуют. Обратите внимание: поскольку исходный тип fa не равен 1 , следующее выражение не может быть правильно типизировано при упомянутых до сих пор предположениях:

$h\;(f\;a)$

Поскольку последовательное применение используется для несколькихаргументов не обязательно знать арность функции впорядок определения его типизации; например, если мы знаем, что $c:1{\to }C$ тогда выражение

Джей Си

хорошо типизирован, пока j имеет тип

$(C\times \alpha ){\to }\beta$ для некоторого α

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

История

Первоначально представлен Барендрегт термин«функциональная полнота» в контексте комбинаторной алгебры.Каппа-исчисление возникло благодаря усилиям Ламбека. сформулировать соответствующий аналог функционалаполнота для произвольных категорий (см. Hermida and Jacobs, раздел 1). Позже у Хасэгавы развилась каппа.исчисления в удобный (хотя и простой) язык программирования, включающийарифметика над натуральными числами и примитивная рекурсия. Соединения со стрелками позже были расследованы Пауэром, Тилеке и другими.

Варианты

Можно изучить версии каппа-исчисления с помощью субструктурные типы, такие как линейный , аффинный ,и упорядоченные типы. Эти расширения требуют устранения илиограничение $!_{\tau }$ выражение. В таких обстоятельствахоператор типа × не является настоящим декартовым произведением,и обычно пишется ⊗, чтобы это было ясно.