Z izomorfizmem Curry-Howarda zetknąłem się stosunkowo późno w moim życiu programistycznym i być może przyczynia się to do tego, że jestem nim całkowicie zafascynowany. Oznacza to, że dla każdej koncepcji programowania istnieje dokładny odpowiednik w logice formalnej i na odwrót. Oto „podstawowa” lista takich analogii, prosto z mojej głowy:
program/definition | proof
type/declaration | proposition
inhabited type | theorem/lemma
function | implication
function argument | hypothesis/antecedent
function result | conclusion/consequent
function application | modus ponens
recursion | induction
identity function | tautology
non-terminating function | absurdity/contradiction
tuple | conjunction (and)
disjoint union | disjunction (or) -- corrected by Antal S-Z
parametric polymorphism | universal quantification
A więc, odpowiadając na moje pytanie: jakie są niektóre z bardziej interesujących / niejasnych implikacji tego izomorfizmu? Nie jestem logikiem, więc jestem pewien, że tylko zarysowałem tę listę.
Na przykład, oto kilka pojęć związanych z programowaniem, dla których nie znam zwięzłych nazw w logice:
currying | "((a & b) => c) iff (a => (b => c))"
scope | "known theory + hypotheses"
A oto kilka logicznych koncepcji, których nie do końca sprecyzowałem w terminach programowania:
primitive type? | axiom
set of valid programs? | theory
Edytować:
Oto kilka innych odpowiedników zebranych z odpowiedzi:
function composition | syllogism -- from Apocalisp
continuation-passing | double negation -- from camccann
źródło
goto | jumping to conclusions
Odpowiedzi:
Ponieważ wyraźnie poprosiłeś o najbardziej interesujące i niejasne:
Możesz rozszerzyć CH na wiele interesujących logik i formuł logicznych, aby uzyskać naprawdę szeroką gamę odpowiedników. Tutaj starałem się skupić na niektórych bardziej interesujących, a nie na niejasnych, a także na kilku fundamentalnych, które jeszcze się nie pojawiły.
EDYCJA: Odniesienie, które poleciłbym każdemu, kto chciałby dowiedzieć się więcej o rozszerzeniach CH:
„Osądowa rekonstrukcja logiki modalnej” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - to świetne miejsce do rozpoczęcia, ponieważ zaczyna się od podstawowych zasad, a większość z nich ma być dostępne dla nie-logików / teoretyków języka. (Jestem drugim autorem, więc jestem stronniczy).
źródło
Trochę mętnisz sprawy dotyczące nieterminacji. Fałsz jest reprezentowany przez niezamieszkane typy , które z definicji nie mogą być niezakończone, ponieważ nie ma niczego takiego do oceny.
Brak zakończenia reprezentuje sprzeczność - niespójną logikę. Niespójna logika oczywiście pozwoli ci udowodnić wszystko , łącznie z fałszem.
Ignorując niespójności, systemy typów zwykle odpowiadają logice intuicjonistycznej i są z konieczności konstruktywistyczne , co oznacza, że niektóre elementy logiki klasycznej nie mogą być wyrażone bezpośrednio, jeśli w ogóle. Z drugiej strony jest to przydatne, ponieważ jeśli typ jest ważnym dowodem konstrukcyjnym, wówczas termin tego typu jest sposobem na skonstruowanie wszystkiego, czego udowodniłeś istnienie .
Główną cechą konstruktywizmu jest to, że podwójna negacja nie jest równoznaczna z brakiem negacji. W rzeczywistości negacja rzadko jest prymitywem w systemie typów, więc zamiast tego możemy ją przedstawić jako implikującą fałsz, np .
not P
Staje sięP -> Falsity
. Podwójna negacja byłaby zatem funkcją z typem(P -> Falsity) -> Falsity
, co oczywiście nie jest równoważne z czymś tylko typuP
.Jest jednak w tym interesujący zwrot! W języku z parametrycznym polimorfizmem zmienne typu obejmują wszystkie możliwe typy, w tym niezamieszkane, więc typ w pełni polimorficzny, taki jak
∀a. a
w pewnym sensie jest prawie fałszywy. A co, jeśli napiszemy podwójną prawie negację za pomocą polimorfizmu? Dostajemy typ, który wygląda tak:∀a. (P -> a) -> a
. Czy to jest równoważne z czymś w rodzajuP
? Rzeczywiście , wystarczy zastosować to do funkcji tożsamości.Ale o co chodzi? Po co pisać taki typ? Czy to coś znaczy w zakresie programowania? Cóż, możesz myśleć o niej jako o funkcji, która już
P
gdzieś ma coś typu i wymaga, abyś nadał jej funkcję, która przyjmujeP
jako argument, a całość jest polimorficzna w typie wyniku końcowego. W pewnym sensie reprezentuje zawieszone obliczenia czekające na dostarczenie reszty. W tym sensie te zawieszone obliczenia można składać razem, przekazywać, wywoływać, cokolwiek. Powinno to brzmieć znajomo dla fanów niektórych języków, takich jak Scheme czy Ruby - ponieważ oznacza to, że podwójna negacja odpowiada stylowi przekazywania kontynuacjiiw rzeczywistości typ, który podałem powyżej, jest dokładnie kontynuacją monady w Haskell.źródło
P -> Falsity
. Rozumiem, dlaczego to działa (¬p ≡ p → ⊥), ale nie mam wersji kodu.P -> ⊥
powinno być zamieszkane właśnie wtedy, gdyP
nie jest, prawda? Ale czy ta funkcja nie powinna być zawsze zamieszkana? A właściwie nigdy, ponieważ nie możesz zwrócić wystąpienia⊥
? Nie do końca widzę w tym warunkowość. Jaka jest tu intuicja?P -> Falsity
jest równoważnaP
byciu fałszem.f x = x
, którą bawiłemP = ⊥
, była podobna do tej , która byłaby natychmiastowa iff , ale najwyraźniej nie była wystarczająco ogólna. Więc chodzi o to, że aby zwrócić bezwartościowy typ, nie potrzebujesz ciała; ale aby funkcja była definiowalna i całkowita, nie potrzebujesz żadnych przypadków , więc jeśliP
jest niezamieszkany, wszystko działa? To trochę dziwne, ale myślę, że to widzę. Wydaje się to dość dziwnie współgrać z moją definicjąXor
typu… Muszę o tym pomyśleć. Dzięki!Twój wykres nie jest całkiem poprawny; w wielu przypadkach mylisz typy z terminami.
[1] Logika języka funkcjonalnego kompletnego według Turinga jest niespójna. Rekursja nie ma odpowiednika w spójnych teoriach. W niespójnej logice / nieuzasadnionej teorii dowodu można nazwać to regułą, która powoduje niespójność / brak podstaw.
[2] Ponownie, jest to konsekwencja kompletności. Byłby to dowód antyteorematu, gdyby logika była spójna - a zatem nie może istnieć.
[3] Nie istnieje w językach funkcyjnych, ponieważ wykluczają one cechy logiczne pierwszego rzędu: cała kwantyfikacja i parametryzacja odbywa się na formułach. Jeśli miał możliwości pierwszego rzędu, nie byłoby rodzajem inny niż
*
,* -> *
itp .; rodzaj elementów domeny dyskursu. Na przykład, wFather(X,Y) :- Parent(X,Y), Male(X)
,X
iY
zakres, w dziedzinie mowy (nazwaćDom
) iMale :: Dom -> *
.źródło
źródło
Naprawdę podoba mi się to pytanie. Nie wiem zbyt wiele, ale mam kilka rzeczy (wspomaga artykuł w Wikipedii , który ma kilka zgrabnych tabel i takie samo):
Myślę, że typy sum / typy związków ( np.
data Either a b = Left a | Right b
) Są równoważne rozłączeniu włączającemu . I chociaż nie jestem zbyt dobrze zaznajomiony z Curry-Howardem, myślę, że to pokazuje. Rozważ następującą funkcję:Jeśli dobrze rozumiem, typ mówi, że ( a ∧ b ) → ( a ★ b ), a definicja mówi, że to prawda, gdzie ★ jest albo włączające, albo wyłączające, albo, w zależności od tego, co
Either
reprezentuje. MaszEither
wyłączne reprezentowanie lub, ⊕; jednak ( a ∧ b ) ↛ ( a ⊕ b ). Na przykład ⊤ ∧ ⊤ ≡ ⊤, ale ⊤ ⊕ ⊥ ≡ ⊥ i ⊤ ↛ ⊥. Innymi słowy, jeśli zarówno a, jak i b są prawdziwe, to hipoteza jest prawdziwa, ale wniosek jest fałszywy, a więc implikacja ta musi być fałszywa. Jednak wyraźnie ( a ∧ b ) → ( a ∨ b ), ponieważ jeśli oba a i b są prawdziwe, to przynajmniej jedno jest prawdziwe. Tak więc, jeśli dyskryminowane związki są jakąś formą dysjunkcji, muszą być różnorodne. Myślę, że jest to dowód, ale nie wahaj się wyrzucić mnie z tego pojęcia.Podobnie, twoje definicje tautologii i absurdu jako, odpowiednio, funkcji tożsamości i funkcji nie kończących się, są nieco dziwne. Prawdziwa formuła jest reprezentowana przez typ jednostki , który jest typem, który ma tylko jeden element (
data ⊤ = ⊤
; często pisany()
i / lubUnit
w funkcjonalnych językach programowania). Ma to sens: skoro ten typ jest gwarantowana do zamieszkania, a ponieważ istnieje tylko jeden możliwy mieszkaniec, to musi być prawda. Funkcja tożsamości reprezentuje po prostu szczególną tautologię, którą a → a .Twój komentarz na temat funkcji nie kończących się jest, w zależności od tego, co dokładnie miałeś na myśli, mniejszy. Curry-Howard działa w systemie typów, ale brak zakończenia nie jest tam kodowany. Według Wikipedii , do czynienia z braku rozwiązania jest problem, jak dodawanie produkuje sprzeczne logiki ( np mogę określić
wrong :: a -> b
przezwrong x = wrong x
, a tym samym „udowodnić”, że → b dla dowolnego A i B ). Jeśli to właśnie miałeś na myśli mówiąc o „absurdzie”, to masz całkowitą rację. Jeśli zamiast tego miałeś na myśli fałszywe stwierdzenie, to zamiast tego potrzebujesz dowolnego niezamieszkanego typu, np. Czegoś zdefiniowanego przezdata ⊥
- to jest typ danych bez możliwości jego skonstruowania. Gwarantuje to, że nie ma żadnych wartości, więc musi być niezamieszkany, co jest równoważne z fałszem. Myślę, że prawdopodobnie mógłbyś również użyća -> b
, ponieważ jeśli zabronimy funkcji niezakończonych, to również jest niezamieszkany, ale nie jestem w 100% pewien.Wikipedia podaje, że aksjomaty są kodowane na dwa różne sposoby, w zależności od tego, jak interpretujesz Curry-Howard: albo w kombinatorach, albo w zmiennych. Myślę, że widok kombinatora oznacza, że podstawowe funkcje, które otrzymujemy, kodują rzeczy, które możemy powiedzieć domyślnie (podobnie do sposobu, w jaki modus ponens jest aksjomatem, ponieważ zastosowanie funkcji jest prymitywne). Myślę , że widok zmiennych może w rzeczywistości oznaczać to samo - w końcu kombinatory to tylko zmienne globalne, które są określonymi funkcjami. Jeśli chodzi o typy pierwotne: jeśli myślę o tym poprawnie, to myślę, że typy pierwotne to byty - obiekty prymitywne, o których próbujemy udowodnić.
Zgodnie z moją klasą logiki i semantyki fakt, że ( a ∧ b ) → c ≡ a → ( b → c ) (a także, że b → ( a → c )) nazywa się prawem równoważności eksportu, przynajmniej w naturalnej dedukcji dowody. Nie zauważyłem wtedy, że to po prostu curry - szkoda, że nie, bo to super!
Choć teraz mamy drogę do reprezentowania integracyjnego alternatywę, nie mamy sposobu reprezentowania wyłączne różnorodność. Powinniśmy umieć posłużyć się definicją wyłącznej dysjunkcji, aby ją przedstawić: a ⊕ b ≡ ( a ∨ b ) ∧ ¬ ( a ∧ b ). Nie wiem, jak napisać negację, ale wiem, że ¬ p ≡ p → ⊥ i zarówno implikacja, jak i fałsz są łatwe. Powinniśmy zatem być w stanie przedstawić wyłączną dysjunkcję poprzez:
To definiuje
⊥
pusty typ bez wartości, co odpowiada fałszowi;Xor
Następnie określono, że zawiera oba ( a ) lub b ( i ) i funkcja ( WPŁYW NA ) z (a, b) ( i ) do dna typu ( fałszywego ).Nie mam jednak pojęcia, co tooznacza.( Edycja 1: Teraz rozumiem, zobacz następny akapit!)Ponieważ nie ma wartości typu(czy istnieją?), Nie mogę pojąć, co to oznaczałoby w programie.Czy ktoś zna lepszy sposób myślenia o tej lub innej definicji?Either
( Edycja 1: tak, camccann .)(a,b) -> ⊥
Edycja 1: Dzięki odpowiedzi Camccanna (a dokładniej komentarzom, które zostawił, aby mi pomóc), myślę, że rozumiem, co się tutaj dzieje. Aby skonstruować wartość typu
Xor a b
, musisz podać dwie rzeczy. Po pierwsze, świadek istnienia elementu alboa
albob
jako pierwszego argumentu; to znaczy aLeft a
lub aRight b
. Po drugie, dowód, że nie ma elementów obu typówa
ib
- innymi słowy,(a,b)
niezamieszkany dowód - jako drugi argument. Skoro będziesz mógł napisać funkcję tylko(a,b) -> ⊥
wtedy, gdy(a,b)
jest niezamieszkana, co to oznacza, że tak jest? Oznaczałoby to, że jakaś część obiektu typu(a,b)
nie można było zbudować; innymi słowy, że co najmniej jeden, a ewentualnie oba,a
ib
są niezamieszkanej, jak dobrze! W tym przypadku, jeśli myślimy o dopasowywaniu wzorców, nie byłoby możliwe dopasowanie do wzorca takiej krotki: zakładając, żeb
jest to niezamieszkane, co byśmy napisali, co mogłoby pasować do drugiej części tej krotki? W związku z tym nie możemy dopasować do niego wzorców, co może pomóc ci zrozumieć, dlaczego powoduje to, że jest niezamieszkany. Otóż jedynym sposobem na uzyskanie funkcji całkowitej, która nie przyjmuje żadnych argumentów (tak jak ta musi, ponieważ(a,b)
jest niezamieszkana) jest uzyskanie wyniku również typu niezamieszkanego - jeśli myślimy o tym z perspektywy dopasowania wzorców, oznacza to, że nawet jeśli funkcja nie ma przypadków, nie ma możliwej treści może mieć jedno i drugie, więc wszystko jest w porządku.Wiele z tego sprawia, że myślę na głos / udowadniam (miejmy nadzieję) rzeczy w locie, ale mam nadzieję, że jest to przydatne. Naprawdę polecam artykuł w Wikipedii ; Nie przeczytałem tego szczegółowo, ale zawarte w nim tabele są naprawdę fajnym podsumowaniem i jest bardzo dokładne.
źródło
Either a a
nie powinno być twierdzeniem:Either ⊥ ⊥
jest nadal niezamieszkany. TOM: Jak powiedział Camccann, konsekwencja oznacza wygaśnięcie. Tak więc spójny system typów nie pozwoli ci na wyrażanief :: a -> b
, więc typ byłby niezamieszkany; niespójny system typów miałby mieszkańca jako typ, ale taki, który nie zostałby rozwiązany. camccann: Czy istnieją niespójne systemy typów, które nie są kompletne według Turinga, zajmując jakiś punkt pośredni w hierarchii? A może ten ostatni krok (dodanie ogólnej rekursji lub cokolwiek innego) jest dokładnie równoważny z niespójnością?Oto nieco niejasny przypadek, o którym jestem zaskoczony, że nie został poruszony wcześniej: „klasyczne” funkcjonalne programowanie reaktywne odpowiada logice temporalnej.
Oczywiście, chyba że jesteś filozofem, matematykiem lub obsesyjnym programistą funkcjonalnym, prawdopodobnie spowoduje to kilka dodatkowych pytań.
Po pierwsze: czym jest funkcjonalne programowanie reaktywne? Jest to deklaratywny sposób pracy z wartościami zmieniającymi się w czasie . Jest to przydatne do pisania rzeczy, takich jak interfejsy użytkownika, ponieważ dane wejściowe użytkownika to wartości zmieniające się w czasie. „Klasyczny” FRP ma dwa podstawowe typy danych: zdarzenia i zachowania.
Zdarzenia reprezentują wartości, które istnieją tylko w dyskretnych momentach. Klawisze są doskonałym przykładem: możesz myśleć o danych wejściowych z klawiatury jako o znaku w danym momencie. Każde naciśnięcie klawisza jest wówczas tylko parą zawierającą znak klawisza i godzinę jego naciśnięcia.
Zachowania to wartości, które istnieją nieustannie, ale mogą ulegać ciągłym zmianom. Położenie myszy jest doskonałym przykładem: jest to po prostu zachowanie współrzędnych x, y. W końcu mysz zawsze ma swoją pozycję i, koncepcyjnie, pozycja ta zmienia się w sposób ciągły, gdy poruszasz myszą. W końcu poruszanie myszą to pojedyncza, przeciągająca się czynność, a nie kilka dyskretnych kroków.
A czym jest logika temporalna? Właściwie jest to zbiór logicznych reguł postępowania ze zdaniami ujętymi ilościowo w czasie. Zasadniczo rozszerza normalną logikę pierwszego rzędu o dwa kwantyfikatory: □ i ◇. Pierwsza oznacza „zawsze”: czytaj □ φ jako „φ zawsze trzyma”. Druga to „ostatecznie”: ◇ φ oznacza, że „φ w końcu się utrzyma”. To jest szczególny rodzaj logiki modalnej . Następujące dwie prawa odnoszą się do kwantyfikatorów:
Zatem □ i ◇ są do siebie podwójne w taki sam sposób jak ∀ i ∃.
Te dwa kwantyfikatory odpowiadają dwóm typom w FRP. W szczególności □ odpowiada zachowaniom, a ◇ odpowiada zdarzeniom. Jeśli zastanowimy się, jak te typy są zamieszkane, powinno to mieć sens: zachowanie jest zamieszkane w każdym możliwym czasie, podczas gdy zdarzenie ma miejsce tylko raz.
źródło
W odniesieniu do relacji między kontynuacjami a podwójną negacją, typ połączenia / DW to prawo Peirce'a http://en.wikipedia.org/wiki/Call-with-current-continuation
CH jest zwykle określane jako zgodność między logiką intuicjonistyczną a programami. Jeśli jednak dodamy operator wywołania z kontynuacją prądu (callCC) (którego typ odpowiada prawu Peirce'a), otrzymamy zgodność między logiką klasyczną a programami z callCC.
źródło
Chociaż nie jest to prosty izomorfizm, ta dyskusja na temat konstruktywnego LEM jest bardzo interesującym wynikiem. W szczególności w części podsumowującej Oleg Kiselyov omawia, w jaki sposób użycie monad do eliminacji podwójnej negacji w logice konstruktywnej jest analogiczne do odróżnienia zdań rozstrzygalnych obliczeniowo (dla których LEM jest ważny w konstruktywnym otoczeniu) od wszystkich zdań. Pogląd, że monady rejestrują efekty obliczeniowe, jest stary, ale ten przykład izomorfizmu Curry-Howarda pomaga spojrzeć na to z odpowiedniej perspektywy i zrozumieć, co tak naprawdę „oznacza” podwójna negacja.
źródło
Obsługa kontynuacji najwyższej klasy pozwala na wyrażenie $ P \ lor \ neg P $. Sztuczka polega na tym, że niewywołanie kontynuacji i zakończenie z jakimś wyrażeniem jest równoznaczne z wywołaniem kontynuacji tym samym wyrażeniem.
Bardziej szczegółowy widok można znaleźć pod adresem : http://www.cs.cmu.edu/~rwh/courses/logic/www-old/handouts/callcc.pdf
źródło
Jedna rzecz, która jest ważna, ale nie została jeszcze zbadana, to związek 2-kontynuacji (kontynuacja, która przyjmuje 2 parametry) i udaru Sheffera . W klasycznej logice, uderzenie Sheffera może samodzielnie tworzyć kompletny system logiczny (plus kilka koncepcji nieoperatorskich). Co oznacza, że znajomy
and
,or
,not
mogą być realizowane wyłącznie za pomocą stoke Sheffera lubnand
.Jest to ważny fakt dotyczący zgodności z typami programowania, ponieważ sugeruje, że kombinator jednego typu może być użyty do utworzenia wszystkich innych typów.
Sygnatura typu 2-kontynuacji to
(a,b) -> Void
. Dzięki tej implementacji możemy zdefiniować 1-kontynuację (normalne kontynuacje) jako(a,a)
-> Void, typ produktu jako((a,b)->Void,(a,b)->Void)->Void
, typ sumy jako((a,a)->Void,(b,b)->Void)->Void
. To daje nam imponującą siłę wyrazu.Jeśli pójdziemy dalej, dowiemy się, że wykres egzystencjalny Piece jest równoważny z językiem, którego jedynym typem danych jest n-kontynuacja, ale nie widziałem żadnego istniejącego języka w tej formie. Myślę, że wymyślenie jednego może być interesujące.
źródło