Jaka jest rola dwukolorowego rachunku konstrukcji?

Czytam więc trochę o opracowaniu, w szczególności algorytmach opartych na dwukolorowym rachunku budowy i jestem trochę zdezorientowany. Nie rozumiem, jaki dokładnie jest cel tego $CC^{bi}$ jest. Wydaje się być identyczny z $CC$ z wyjątkiem tego, że istnieje rozróżnienie między niejawnymi i jawnymi argumentami funkcji. W szczególności nie widzę, jak pozwala ci pisać $(id\; 0)$ zamiast $(id\; \mathbb{N}\; 0)$ . Jeśli przyjmiemy system globalnych definicji, wówczas

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

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

Czy reguły naprawdę na to pozwalają $(id\; 0)$ ? Oczywiście, że tak, ale nie widzę tego w relacji pisania. Czy coś brakuje? Czy rozumiem rolę $CC^{bi}$ nieprawidłowo?

Ponadto, czy nie utracono własności zbiegu? Wydaje mi się, że moim problemem jest to, że czytam o opracowaniu bez większego przeczytania $CC^{bi}$ przed tym. Jaki jest dobry artykuł, który go wprowadza i tylko on?

Edycja: Aby być bardziej szczegółowym, pytam jak $(id\; 0)$ jest akceptowane zamiast $(id\; \mathbb{N}\; 0)$ kiedy reguły są zarówno jawne, jak i niejawne $\Pi$ aplikacje są identyczne modulo sytnax. Nie widzę żadnej różnicy między $:$ i $|$ zasady dla obu wydają się takie same.

Edycja: Nie mówię o Implicit Calculus of Constructions, która jest inną teorią i ma różne reguły jawnego $\Pi$ (aplikacja vs. generacja).

Edycja: OK, chyba zaczynam to rozumieć, ale nie odpowiem na to pytanie, dopóki nie będę pewien. Gruntownie $(id\; 0)$ nie pisze sprawdzania, a tak naprawdę jest tylko rozwinięty $(id\; \mathbb{N}\; 0)$ tuż przed sprawdzaniem typu lub wykonywane jako dodatkowa odpowiedzialność algorytmu sprawdzania typu. Zasadniczo te ukryte rachunki mają być językami interfejsu (użytkownika), które są opracowywane w zwykłych (jawnych) rachunkach lub przynajmniej jawnym fragmencie ukrytych rachunków przed sprawdzeniem typu. Jeśli tak jest, to myślę, że widzę duży obraz. Czy ktoś może to potwierdzić?

— Anthony
źródło

Jak powiedziałem poniżej, twoja intuicja jest poprawna: dwukolorowy rachunek konstrukcji jest rachunkiem jawnym, w którym argumenty pominięte przez użytkownika, ale opracowane przez „front end” są wyraźnie zaznaczone. Również utrata konfluencji dla redukcji beta + eta jest prawdą, jeśli jest ograniczona tylko do wersji beta.

— cody

W Domniemana rachunku konstrukcji rozszerzającej Czysta systemów typu ze skrzyżowania rodzaj spoiwa i Subtyping Alexandre Miquel wprowadza podstawowe pojęcia dotyczące niejawnego rachunku konstrukcji, która moim zdaniem jest synonimem bicolored rachunku konstrukcji.

Chodzi o to, aby (między innymi) mieć rachunek bez bałaganu jawnych adnotacji typu wszędzie. Wnioskowanie typu jest jednak (bardzo prawdopodobne) nierozstrzygalne.

W tym rachunku, jeśli weźmiemy $id=\lambda x. x$ , to możesz wyprowadzić

⊢ ja re : \forall X : T. y p mi . X \to X

$\vdash id\colon \forall X\colon Type. X\rightarrow X$ po prostu używając kolejno produktu jawnego i ukrytych reguł produktu. Wtedy reguła tworzenia instancji dla produktu niejawnego pozwala

⊢ ja re : N. za t \to N. za t

$\vdash id\colon Nat\rightarrow Nat$ a więc

⊢ ja re 0 : N. za t

$\vdash id\ 0 \colon Nat$ System dopuszcza redukcję i konfluencję osobników, nawet na nietypowych warunkach (co w rzeczywistości nie działa w przypadku rachunków z adnotacjami abstrakcyjnymi). Wszystko to można znaleźć w pracy Aleksandra, która niestety jest po francusku. Obawiam się, że nie jestem pewien, czy mam lepsze odniesienie do tych wyników.

— cody
źródło

Pierwszą część twojej odpowiedzi znałem, ale myślę, że powinienem był uściślić w moim pierwotnym pytaniu. To znaczy, w jaki dokładnie sposób (id 0) jest dozwolony, jeśli id ma typ (\ Pi X | Typ. X -> X), ponieważ wydaje się, że reguła APP jest identyczna zarówno dla niejawnej, jak i jawnej \ Pi. W niejawnym rachunku konstrukcji, który w rzeczywistości jest inną teorią, tak nie jest, ponieważ jest on podzielony na APP i GEN. Aby sprawdzić, czy jest inaczej, sprawdź nagłówek „Rachunek z„ naprawdę niejawnymi ”argumentami” w dokumencie, do którego się odwoływałeś.

— Anthony

Odnośnie rozstrzygalności. Artykuł, do którego się odwołujesz, przypuszcza, że jego teoria jest nierozstrzygalna. Artykuł, do którego się odwołuje (wydaje mi się, że „oryginalny” dwukolorowy rachunek papieru konstrukcyjnego) jest rozstrzygalny, ale wyraźnie tego nie dowodzi. Przeczytałem to po opublikowaniu tego pytania i wydaje się, że zdecydowanie powinno być rozstrzygalne, a w zależności od ograniczeń składniowych zachować zbieżność. Z drugiej strony nadal tkwi moje pierwotne zamieszanie: \

— Anthony

Może powinieneś nam powiedzieć, na który papier patrzysz.

— cody

Ok, rzuciłem okiem na opracowanie i usuwanie w teorii typów autorstwa Marko Luthera, który, jak sądzę, jest twoim odniesieniem. W takim przypadku nie ma semantycznej różnicy między produktami jawnymi i dorozumianymi, a system dwukolorowy jest konserwatywnym rozszerzeniem rachunku konstrukcji. To, co się dzieje, polega na tym, że używasz opracowania, aby przyjąć termin bez wyraźnego argumentu, aby zamienić go w termin z pełną adnotacją: id !1 0opracowuje do id Nat 0. W tym tekście opracowanie omówione jest w części 4.

— cody

Tak, to jest papier, który zacząłem, po prostu nie zdałem części na temat używania

C C^{b i}

$CC^{bi}$ nie zdawałem sobie również sprawy z tego, jak rozwijał jedną teorię po kolei i że wcześniejsze zmiany są wykorzystywane jedynie jako pedagogika. Wybacz, że nie wspomniałem o tym wcześniej. Myślałem, że rachunek różniczkowy jest dobrze znany z jego nazwy poza papierem, który czytam.

— Anthony