Pytania dotyczące logiki matematycznej i jej zastosowania w informatyce
Słyszałem o indukcji (strukturalnej). Pozwala budować struktury skończone z mniejszych i zapewnia zasady dowodowe dla uzasadnienia takich struktur. Pomysł jest wystarczająco jasny. A co z koindukcją? Jak to działa? Jak można powiedzieć coś rozstrzygającego o nieskończonej strukturze? Są...
Na stronie Wikipedii dla Fixed Point Combinators jest napisany dość tajemniczy tekst Kombinator Y jest przykładem tego, co powoduje, że rachunek Lambda jest niespójny. Dlatego należy to traktować podejrzliwie. Można jednak bezpiecznie rozważyć kombinator Y, gdy jest on zdefiniowany tylko w...
Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i piszę serię pytań na temat tego procesu, zaczynając tutaj. Zauważ, że te tematy nie są łatwe do zrozumienia bez tła w logice (matematycznej). Jeśli masz problemy z podstawowymi terminami, przeczytaj je, na przykład...
Być może należałoby przeprosić za zadanie kolejnego pytania na temat warunków wstępnych, ale byłem zdezorientowany co do punktów wyjścia. Spotkałem różne terminy, takie jak „logika modalna”, „logika czasowa”, „logika pierwszego rzędu”, „logika drugiego rzędu” i „logika wyższego rzędu”. Co...
Wiele podręczników obejmuje typy przecięć w rachunku lambda. Reguły pisania dla przecięcia można zdefiniować w następujący sposób (na górze zwykłego rachunku lambda z podtypami): Γ⊢M:T1Γ⊢M:T2Γ⊢M:T1∧T2(∧I)Γ⊢M:⊤(⊤I)Γ⊢M.:T.1Γ⊢M.:T.2)Γ⊢M.:T.1∧T.2)(∧ja)Γ⊢M.:⊤(⊤ja) \dfrac{\Gamma \vdash M : T_1 \quad...
Kombinator stałoprzecinkowy FIX (znany również jako kombinator Y) w (niepoprawnym) rachunku lambda ( ) jest zdefiniowany jako:λλ\lambda FIX≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))≜λf.(λx.f (λy.x x y)) (λx.f (λy.x x y))\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y....
Wikipedia, jak również inne źródła, które znalazłem, wskazują voidtyp C jako typ jednostki, a nie typ pusty. Uważam to za mylące, ponieważ wydaje mi się, że voidlepiej pasuje do definicji typu pustego / dolnego. voidO ile wiem, nie zamieszkują żadnych wartości . Funkcja z typem zwracanym void...
Mam zestaw par. Każda para ma taką postać (x, y), że x, y należą do liczb całkowitych z zakresu [0,n). Jeśli więc n wynosi 4, to mam następujące pary: (0,1) (0,2) (0,3) (1,2) (1,3) (2,3) Mam już pary. Teraz muszę zbudować kombinację za pomocą n/2par, tak aby żadna liczba całkowita nie była...
Większość z nas zna zgodność między logiką kombinacyjną a rachunkiem lambda . Ale nigdy nie widziałem (może nie spojrzałem wystarczająco głęboko) odpowiednika „typowanych kombinatorów”, odpowiadającego po prostu typowanemu rachunku lambda. Czy coś takiego istnieje? Gdzie można znaleźć informacje na...
Wydaje mi się, że „implikacja” w języku angielskim nie oznacza tego samego, co operator logiczny „implikuje”, podobnie jak słowo „LUB” w większości przypadków oznacza „Wyłączne OR” w naszym codziennym użyciu języka. Weźmy dwa przykłady: Jeśli dzisiaj jest poniedziałek, jutro jest wtorek. To...
Logika konstruktywistyczna to system, który usuwa Prawo Akceptowanego Środka, a także Podwójną Negację, jako aksjomaty. Jest opisany na Wikipedii tutaj i tutaj . W szczególności system nie dopuszcza dowodu sprzeczności. Zastanawiam się, czy ktoś wie, jak to wpływa na wyniki dotyczące maszyn...
Szukam prostego rachunku, który obsługuje rozumowanie na temat refleksji , a mianowicie introspekcji i manipulacji uruchomionymi programami. Czy istnieje nietypowe rozszerzenie -calculus, które umożliwia konwersję -terms do postaci, którą można manipulować składniowo, a następnie...
Chciałbym wiedzieć, czy istnieje zasada, aby to udowodnić. Na przykład, jeśli użyję prawa dystrybucyjnego, dostanę tylko (A∨A)∧(A∨¬B)(ZA∨ZA)∧(ZA∨¬b)(A \lor A) \land (A \lor \neg B)
Według mojej wiedzy istnieją trzy główne algebry procesowe, które zainspirowały szeroki zakres badań nad formalnymi modelami współbieżności. To są: CCS i -calculus oba autorstwa Robina Milneraππ\pi CSP Tony Hoare i ACP: Jan Bergstra i Jan Willem Klop Wydaje się, że wszyscy trzej mają do dzisiaj...
W skrypcie, który obecnie czytam na rachunku lambda, równoważność beta jest zdefiniowana następująco: ββ\beta -equivalence ≡β≡β\equiv_\beta jest najmniejszym równoważności, który zawiera →β→β\rightarrow_\beta . Nie mam pojęcia co to znaczy. Czy ktoś może to wyjaśnić w prostszy sposób? Może z...
Rozważ typ indukcyjny, który ma pewne rekurencyjne zdarzenia w zagnieżdżonej, ale ściśle dodatniej lokalizacji. Na przykład drzewa ze skończonymi rozgałęzieniami z węzłami używającymi ogólnej struktury danych listy do przechowywania elementów potomnych. Inductive LTree : Set := Node : list LTree...
Jak mogę wyrazić bramkę AND używając tylko bramek
Uczę się samodzielnie Automated Theorem Proving / SMT solvers / Proof Assistants i piszę serię pytań na temat tego procesu, zaczynając tutaj . Jakie są odpowiednie dowody zautomatyzowanego twierdzenia? Znalazłem Przegląd dostawców twierdzeń Czy to wciąż aktualne? Które są nadal bardzo aktywne,...
Dobrze wiadomo, że kombinatory S i K tworzą zestaw podstawowy dla rachunku kombinatorycznego, w tym sensie, że wszystkie inne kombinatory można wyrazić za ich pomocą. Istnieje również podstawa Curry'ego B, C, K, W, która ma tę samą właściwość. Musi istnieć nieskończona liczba takich baz, ale nie...
Niedawno myślałem o ważności dowodu sprzeczności. Przez kilka ostatnich dni czytałem o intuicyjnej logice i twierdzeniach Godela, aby sprawdzić, czy dostarczyłyby mi odpowiedzi na moje pytania. W tej chwili wciąż mam pytania (być może związane z nowym materiałem, który czytam) i liczyłem na kilka...