rachunek kappa

W logice matematycznej , teorii kategorii i informatyce rachunek kappa jest formalnym systemem definiowania funkcji pierwszego rzędu .

W przeciwieństwie do rachunku lambda , rachunek kappa nie ma funkcji wyższego rzędu ; jego funkcje nie są obiektami pierwszej klasy . Rachunek kappa można uznać za „przeformułowanie fragmentu pierwszego rzędu wpisanego rachunku lambda”.

Ponieważ jego funkcje nie są obiektami pierwszej klasy, ocena wyrażeń rachunku różniczkowego kappa nie wymaga domknięć .

Definicja

Poniższa definicja została zaadaptowana z diagramów na stronach 205 i 207 Hasegawy.

Gramatyka

Rachunek kappa składa się z typów i wyrażeń podanych w poniższej gramatyce:

${\ Displaystyle \ tau = 1 \ mid \ tau \ razy \ tau \ mid \ ldots}$

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

Innymi słowy,

• 1 jest typem
• τ ${\ Displaystyle \ tau _ {1}}$ i ${\ Displaystyle \ tau _ {2}}$ są typami, to $\ Displaystyle \ tau _ {1} \ razy \ tau _ {2} }}$ jest typem.
• Każda zmienna jest wyrażeniem
• Jeśli τ jest typem, to ${\ displaystyle id_ {\ tau}}$ jest wyrażeniem
• Jeśli τ jest typem, to ${\ displaystyle! _ {\ tau}}$ jest wyrażeniem
• Jeśli τ jest typem, a e jest wyrażeniem, to winda jest wyrażeniem. $} _ {\ tau} (e)}$
• mi ${\ displaystyle e_ {1}}$ i ${\ displaystyle e_ {2}}$ są wyrażeniami, to ${\ displaystyle e_ {1} \ circ e_ {2}}$ wyrażeniem
• Jeśli x jest zmienną, τ jest typem, a e jest wyrażeniem, to ${\ Displaystyle \ kappa x {:} 1 {\ do} \ tau \;. \; e}$ jest wyrażeniem

The ${\ Displaystyle: 1 {\ do} \ tau}$ i indeksy dolne id , ! i $,$ gdy można je jednoznacznie określić na podstawie kontekstu.

Zestawienie jest często używane jako skrót dla kombinacji ${\ displaystyle \ operatorname {lift}}$ i kompozycji:

${\ Displaystyle e_ {1} e_ {2} \ {\ overset {\ nazwa operatora {def}}}}} \ e_ {1} \ circ \ nazwa operatora {lift} (e_{2})}$

Zasady pisania

Prezentacja tutaj wykorzystuje sekwencje ( $,$ aby ułatwić porównanie z prostym typem Wymaga to dodatkowej reguły Var, która nie występuje w Hasegawie

W rachunku kappa wyrażenie ma dwa typy: typ jego źródła i typ jego celu . Mi $\ Displaystyle e: \ tau _ {1} {\ do} \ tau _ {2}}$${\ Displaystyle {\ tau _ {1}}}$ jest używane do wskazania, że ​​wyrażenie e ma typ źródła i typ docelowy ${\ displaystyle {\ tau _ {2}}}$ .

Wyrażeniom w rachunku kappa przypisuje się typy według następujących zasad:

${\ Displaystyle {x {:} 1 {\ do} \ tau \; \ w \; \ Gamma} \ ponad {\ Gamma \ vdash x: 1 {\ do }\tau }}$	(Wartość)
${\ Displaystyle {} \ ponad {\ vdash id _ {\ tau} \;: \; \ tau \ do \ tau}}$	(ID)
${\ Displaystyle {} \ ponad {\ vdash! _ {\ tau} \;: \; \ tau \ do 1}}$	(Huk)
${\ Displaystyle {\ Gamma \ vdash e_ {1} {:} \ tau _{1}{\do }\tau _{2}\;\;\;\;\;\;\Gamma \vdash e_{2}{:}\tau _{2}{\do }\tau_ {3}} \over {\Gamma \vdash e_{2}\circ e_{1}:\tau _{1}{\to }\tau _{3}}}$	(komp.)
${\ Displaystyle {\ Gamma \ vdash e {:} 1 {\ do} \ tau _ {1 }} \over {\Gamma \vdash \operatorname {lift} _{\tau _{2}}(e)\;:\;\tau _{2}\to (\tau _{1}\times \tau _{2})}}$	(Winda)
${\ Displaystyle {\ Gamma, \; x {:} 1 {\ do} \ tau _ {1} \; \ vdash \; e: \ tau _ {2} {\ do }\tau _{3}} \ponad {\Gamma \vdash \kappa x{:}1{\do }\tau _{1}\,.\,e\;:\;\tau _{1} \times \tau _{2}\do \tau _{3}}}$	(kapa)

Innymi słowy,

• Var: przy założeniu ${\ Displaystyle x: 1 {\ do} \ tau}$ pozwala stwierdzić, że ${\ Displaystyle x: 1 {\ do} \ tau}$
• Id: dla dowolnego typu τ , ${\ Displaystyle id_ {\ tau}: \ tau {\ do} \ tau}$
• Bang: dla dowolnego typu τ , ${\ Displaystyle! _ {\ tau}: \ tau {\ do} 1}$
• Komp: jeśli typ docelowy pasuje do typu źródłowego ${\ displaystyle e_ {2}$$}$ mogą być skomponowane w celu utworzenia wyrażenia $2} \ circ e_ {1}}$$\ displaystyle e_$ z typem źródła ${\ displaystyle e_ {1}} i$${\ displaystyle e_ {2}}$ docelowym mi
• mi : $\ Displaystyle e: 1 {\ do} \ tau _ {1}}$${\ Displaystyle \ operatorname {lift} _{\tau _{2}}(e):\tau _{2}{\to }(\tau _{1}\times \tau _{2})}$ to
• Kappa: jeśli możemy stwierdzić, że ${\ Displaystyle e: \ tau _ {2} \ do \ tau _ {3}}$ przy założeniu, że ${\ Displaystyle x: 1 {\to }\tau _{1}} , to$ bez tego założenia możemy wnioskować , że ${\ Displaystyle \ kappa x {:} 1 {\ do} \ tau _ {1} \,. \, e \;: \; \ tau _ {1} \ razy \ tau _ {2} \ do \ tau _ {3}}$

Równości

Rachunek Kappa przestrzega następujących równości:

• Neutralność: Jeśli ${\ Displaystyle f: \ tau _ {1} {\ do} \ tau _ {2}}$ wtedy ${\ Displaystyle f {\ circ} id_ {\ tau _ {1}} = f}$${\ Displaystyle f = id_ {\ tau _ {2}} {\ circ} f}$ fa
• Asocjatywność: Jeśli ${\ Displaystyle f: \ tau _ {1} {\ do} \ tau _ {2}}$ , ${\ Displaystyle g: \ tau _ {2 } {\ do} \ tau _ {3}}$ i ${\ Displaystyle h: \ tau _ {3} {\ do} \ tau _ {4}}$ , a następnie ${\ Displaystyle (h {\ circ} g) {\ circ} f = h {\ circ} (g {\ circ} f)}$ .
• Końcowość: Jeśli ${\ Displaystyle f {:} \ tau {\ do} 1}$ i ${\ Displaystyle g {:} \ tau {\ do} 1}$ wtedy ${\ styl wyświetlania f=g}$
• Redukcja podnoszenia: ${\ Displaystyle (\ kappa xf) \ circ \ nazwa operatora {winda} _ {\ tau} (c) = f [ c/x]}$
• Redukcja Kappa: ${\ Displaystyle \ kappa x . (h \ circ \ nazwa operatora {winda} _ {\ tau} (x)) = h}$ jeśli x nie jest wolne w h

Ostatnie dwie równości to reguły redukcji rachunku różniczkowego, przepisując je od lewej do prawej.

Nieruchomości

Typ 1 można uznać za typ jednostki . Z tego powodu dowolne dwie funkcje, których typ argumentu jest taki sam, a typ wyniku to 1 , powinny być równe – ponieważ istnieje tylko jedna wartość typu 1 , obie funkcje muszą zwracać tę wartość dla każdego argumentu ( Terminality ).

Wyrażenia typu $\ Displaystyle 1 {\ do} \ tau}$ traktować jako „stałe” lub wartości „typu podłoża”; dzieje się tak, ponieważ 1 jest typem jednostki, a zatem funkcja tego typu jest z konieczności funkcją stałą. Zauważ $pewnego$ ma typ dla τ . Jest to podstawowy mechanizm, który zapewnia, że ​​wszystkie funkcje są pierwszego rzędu.

Semantyka kategoryczna

Rachunek kappa ma być wewnętrznym językiem kategorii kontekstowo pełnych .

Przykłady

Wyrażenia z wieloma argumentami mają typy źródeł, które są drzewami binarnymi „niezrównoważonymi w prawo”. Na przykład funkcja f z trzema argumentami typu A, B i C oraz typem wyniku D będzie miała typ

${\ Displaystyle f: A \ razy (B \ razy (C \ razy 1)) \ do D}$

Jeśli zdefiniujemy lewe zestawienie asocjacyjne $do$ skrót dla $c))}$ to - zakładając, że za $\ Displaystyle a: 1 {\ do} A}$ , ${\ Displaystyle b: 1 {\ do} B}$ i ${\ Displaystyle c: 1 {\ do} C}$ - możemy zastosować tę funkcję:

$c \;: \; 1 \ do D}$

Ponieważ wyrażenie $1$ typ źródłowy , jest to „wartość podstawowa” i może zostać przekazane jako argument do Jeśli ${\ Displaystyle g: (D \ razy E) {\ do} F}$ , to

${\ Displaystyle g \; (f \; a \; b \; c) \;: \; E \ do F}$

$jak$ funkcja w :

${\ Displaystyle f \; a \;: \; B \ razy (C \ razy 1) \ do D}$

są zaangażowane żadne wyższe typy (tj. ${\ Displaystyle (\ tau {\ do} \ tau) {\ do} \ tau} .$ Zauważ, że ponieważ typem źródłowym fa nie jest 1 , następujące wyrażenie nie może zostać poprawnie wpisane przy dotychczasowych założeniach:

${\ Displaystyle h \; (f \; a)}$

Ponieważ kolejne zastosowanie jest używane dla wielu argumentów, nie jest konieczna znajomość liczby funkcji , aby określić jej typ; na przykład, jeśli wiemy, że to wyrażenie $: 1 {\ do} C}$

jc

jest dobrze wpisany, o ile j ma typ

${\ Displaystyle (C \ razy \ alfa) {\ do} \ beta}$ dla pewnego α

i β . Ta właściwość jest ważna przy obliczaniu głównego typu wyrażenia, co może być trudne przy próbie wykluczenia funkcji wyższego rzędu z typowanych rachunków lambda poprzez ograniczenie gramatyki typów.

Historia

Barendregt pierwotnie wprowadził termin „kompletność funkcjonalna” w kontekście algebry kombinatorycznej. Rachunek Kappa powstał w wyniku wysiłków Lambeka zmierzających do sformułowania odpowiedniego odpowiednika kompletności funkcjonalnej dla dowolnych kategorii (patrz Hermida i Jacobs, sekcja 1). Hasegawa rozwinął później rachunek kappa w użyteczny (choć prosty) język programowania, w tym arytmetykę na liczbach naturalnych i prymitywną rekurencję. Połączenia ze strzałami zostały później zbadane przez Powera, Thielecke i innych.

Warianty

Możliwe jest eksplorowanie wersji rachunku kappa z typami podstrukturalnymi, takimi jak typy liniowe , afiniczne i uporządkowane . Te rozszerzenia wymagają wyeliminowania lub ograniczenia ${\ displaystyle! _ {\ tau}}$ wyrażenie. W takich okolicznościach × nie jest prawdziwym iloczynem kartezjańskim i jest zwykle zapisywany jako ⊗ , aby to wyjaśnić.