Jakie są najciekawsze równoważniki wynikające z izomorfizmu Curry-Howarda?

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

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.

evaluation             | proof normalisation/cut-elimination
variable               | assumption
S K combinators        | axiomatic formulation of logic   
pattern matching       | left-sequent rules 
subtyping              | implicit entailment (not reflected in expressions)
intersection types     | implicit conjunction
union types            | implicit disjunction
open code              | temporal next
closed code            | necessity
effects                | possibility
reachable state        | possible world
monadic metalanguage   | lax logic
non-termination        | truth in an unobservable possible world
distributed programs   | modal logic S5/Hybrid logic
meta variables         | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus            | linear logic

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).

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 PStaje 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 typu P.

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. aw 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 rodzaju P? 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ż Pgdzieś ma coś typu i wymaga, abyś nadał jej funkcję, która przyjmuje Pjako 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.

Twój wykres nie jest całkiem poprawny; w wielu przypadkach mylisz typy z terminami.

function type              implication
function                   proof of implication
function argument          proof of hypothesis
function result            proof of conclusion
function application RULE  modus ponens
recursion                  n/a [1]
structural induction       fold (foldr for lists)
mathematical induction     fold for naturals (data N = Z | S N)
identity function          proof of A -> A, for all A
non-terminating function   n/a [2]
tuple                      normal proof of conjunction
sum                        disjunction
n/a [3]                    first-order universal quantification
parametric polymorphism    second-order universal quantification
currying                   (A,B) -> C -||- A -> (B -> C), for all A,B,C
primitive type             axiom
types of typeable terms    theory
function composition       syllogism
substitution               cut rule
value                      normal proof

[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, w Father(X,Y) :- Parent(X,Y), Male(X), Xi Yzakres, w dziedzinie mowy (nazwać Dom) i Male :: Dom -> *.

function composition      | syllogism

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):

1. 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ę:

   andImpliesOr :: (a,b) -> Either a b
   andImpliesOr (a,_) = Left a
   

   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 Eitherreprezentuje. Masz Eitherwyłą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.

2. 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 / lub Unitw 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 -> bprzez wrong 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.

3. 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ć.

4. 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!

5. 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:

   data ⊥
   data Xor a b = Xor (Either a b) ((a,b) -> ⊥)
   

   To definiuje ⊥pusty typ bez wartości, co odpowiada fałszowi; XorNastę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 to oznacza . ( 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(a,b) -> ⊥ ( Edycja 1: tak, camccann .)

   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 albo aalbo bjako pierwszego argumentu; to znaczy a Left alub a Right b. Po drugie, dowód, że nie ma elementów obu typów ai b- 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, ai bsą 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, że bjest 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.

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.

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.

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.

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

2-continuation           | Sheffer stoke
n-continuation language  | Existential graph
Recursion                | Mathematical Induction

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, notmogą być realizowane wyłącznie za pomocą stoke Sheffera lub nand.

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.