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

98

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
Tom Crockett
źródło
zamknięcie ~ = zbiór aksjomatów
Apocalisp
+1 To pytanie i wszystkie wartościowe odpowiedzi i komentarze nauczyły mnie więcej o CHI niż tego, czego mogłem się nauczyć przez internet.
Alexandre C.,
25
@Paul Nathan:goto | jumping to conclusions
Joey Adams,
Myślę, że zbiorem wszystkich poprawnych programów byłby model
Daniil
1
fst / snd | eliminacja koniunkcji, lewo / prawo | wprowadzenie do dysjunkcji
Tony Morris,

Odpowiedzi:

34

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

RD1
źródło
dziękuję za dostarczenie mniej trywialnych przykładów (taki był duch pierwotnego pytania), chociaż przyznaję, że kilka z nich jest ponad moją głową… czy terminy „konieczność” i „możliwość” są precyzyjnie zdefiniowane w logice? jak przekładają się na swoje odpowiedniki obliczeniowe?
Tom Crockett
2
Mogę wskazać opublikowane artykuły dla każdego z nich, więc są one precyzyjnie zdefiniowane. Logika modalna jest szeroko badana (od czasów Arystotelesa) i odnosi się do różnych modeli prawdy - „A jest z konieczności prawdziwe” oznacza „w każdym możliwym świecie A jest prawdziwe”, podczas gdy „A jest prawdopodobnie prawdziwe” oznacza „A jest prawdziwe w jednym możliwym świecie” . Możesz udowodnić takie rzeczy jak „(koniecznie (A -> B) i prawdopodobnie A) -> prawdopodobnie B”. Reguły wnioskowania modalnego bezpośrednio dają konstrukcje wyrażeń, reguły typowania i redukcji, jak zwykle w CH. Zobacz: en.wikipedia.org/wiki/Modal_logic and cs.cmu.edu/~fp/papers/mscs00.pdf
RD1
2
@pelotom: Może zechcesz poczytać trochę o innych rodzajach logiki . Zwykła logika klasyczna często nie jest przydatna w tym kontekście - wspomniałem o logice intuicjonistycznej w mojej odpowiedzi, ale logika modalna i liniowa są nawet „dziwniejsze”, ale też naprawdę niesamowite.
CA McCann
1
Dzięki za wskazówki, wygląda na to, że mam trochę do czytania!
Tom Crockett
2
@ RD1: Myślisz, że to źle, spędziłem tyle czasu na myśleniu w Haskellu, że muszę mentalnie tłumaczyć formuły logiki predykatów na sygnatury typów, zanim nabiorą sensu. :( Nie wspominając o tym, że prawo wykluczonego środka i takich zaczyna wydawać się naprawdę zagmatwane i być może podejrzane.
CA McCann
26

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.

CA McCann
źródło
Dzięki za sprostowanie, usunąłem „fałsz” jako synonim nieterminacji. +1 za podwójną negację <=> CPS!
Tom Crockett
Nie do końca rozumiem intuicję związaną z reprezentowaniem ¬p jako P -> Falsity. Rozumiem, dlaczego to działa (¬p ≡ p → ⊥), ale nie mam wersji kodu. P -> ⊥powinno być zamieszkane właśnie wtedy, gdy Pnie 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?
Antal Spector-Zabusky
1
@Antal SZ: Intuicja to oczywiście logika intuicyjna! Ale tak, faktycznie napisanie takiej funkcji jest trudne. Widzę w Twoim profilu, że znasz Haskella, więc może myślisz o algebraicznych typach danych i dopasowywaniu wzorców? Weź pod uwagę, że niezamieszkany typ nie może mieć żadnych konstruktorów, a zatem nie może mieć nic do dopasowania wzorca. Musiałbyś napisać „funkcję” bez treści, co nie jest legalnym Haskellem. W rzeczywistości, o ile mi wiadomo, nie ma sposobu na zapisanie w Haskell wyrażenia typu zanegowanego bez użycia wyjątków czasu wykonania lub niezakończenia.
CA McCann
1
@Antal SZ: Z drugiej strony, jeśli równoważna logika jest spójna, wszystkie funkcje muszą być całkowite, np. Wszystkie dopasowania wzorców muszą być wyczerpujące. Aby więc napisać funkcję bez wzorców, typ parametru nie może mieć żadnych konstruktorów, np. Musi być niezamieszkany. Dlatego taka funkcja byłaby legalna - a więc jej własny typ zamieszkany - dokładnie i tylko wtedy, gdy jej argument jest niezamieszkany. Dlatego funkcja P -> Falsityjest równoważna Pbyciu fałszem.
CA McCann
Aha, myślę, że rozumiem. Wersja f x = x, którą bawiłem P = ⊥, 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śli Pjest niezamieszkany, wszystko działa? To trochę dziwne, ale myślę, że to widzę. Wydaje się to dość dziwnie współgrać z moją definicją Xortypu… Muszę o tym pomyśleć. Dzięki!
Antal Spector-Zabusky
15

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

Frank Atanassow
źródło
[1] - tak, powinienem był być bardziej szczegółowy. Miałem na myśli raczej „strukturalną rekursję” niż nieograniczoną rekursję, która, jak sądzę, jest tym samym, co „spasowanie”. [3] - istnieje w językach zależnie wpisywanych
Tom Crockett
[1] Faktem jest, że jeśli wywołanie funkcji rekurencyjnej (modus ponens) nie powoduje zakończenia programu, parametry (hipotezy) podane dla wywołania lub środowiska MUSZĄ być różne między tymi wywołaniami. Zatem rekurencja polega po prostu na wielokrotnym stosowaniu tego samego twierdzenia. Jeśli jest coś specjalnego, to zwykle jest to zwiększanie / zmniejszanie liczb (krok indukcyjny) i sprawdzanie z istniejącym przypadkiem (przypadek podstawowy), który odpowiada - Matematycznej indukcji w logice.
Earth Engine
Bardzo podoba mi się ten wykres, ale nie powiedziałbym „nie dotyczy”, ponieważ logika spójna nie jest jedynym rodzajem logiki, podobnie jak kończenie programów nie jest jedynym rodzajem programu. Funkcja niezakończająca odpowiadałaby „argumentowi kołowemu” i jest doskonałą ilustracją izomorfizmu Curry-Howarda: „śledzenie” argumentu kołowego wprowadza nas w nieskończoną pętlę.
Joey Adams,
14
function composition      | syllogism
Apocalisp
źródło
13

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.

Antal Spector-Zabusky
źródło
1
+1 za wskazanie, że Albo jest włącznie, albo. Zauważ, że (albo aa) jest twierdzeniem (dla wszystkich a).
Apocalisp
Pytanie dot. 2 (b): jaka jest różnica między typem funkcji, którego jedyny mieszkaniec jest niezakończony, a niezamieszkanym typem funkcji? Na przykład, gdybym zadeklarował typ B bez konstruktorów, a następnie zdefiniowałbym funkcję A-> B w ten sposób: fun (a: A): B: = f (a) to sprawdziłoby się w wielu językach, nawet jeśli jest niemożliwe jest kiedykolwiek zwrócenie B. Więc funkcja jest „zamieszkana” w pewnym sensie, ale jej „mieszkaniec” jest absurdem… więc tak naprawdę nie jest w ogóle zamieszkana. Mam nadzieję, że to ma jakiś sens :)
Tom Crockett
3
Dna nie są dowodami. „Jest absurdalne i niemożliwe do przypuszczenia, że ​​niepoznawalne i nieokreślone powinno zawierać i określać.” - Aristoteles
Apocalisp
2
@Tom: Żeby wyjaśnić kwestię braku zakończenia, jeśli logika jest spójna, wszystkie programy kończą się . Brak zakończenia występuje tylko w systemach typów reprezentujących niespójne logiki lub równoważnie w systemach typów dla języków kompletnych według Turinga.
CA McCann
1
Apocalisp: 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żanie f :: 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ą?
Antal Spector-Zabusky
12

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.

Tikhon Jelvis
źródło
8

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.

James Iry
źródło
4

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.

wren romano
źródło
4

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

Daniil
źródło
Dzięki za wgląd!
paulotorrens
4
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.

Earth Engine
źródło