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...
Mamy logikę Hoare'a. Dlaczego wciąż jest możliwe, że algorytm ma rację, ale nie ma dowodów na jego poprawność? Załóżmy, że algorytm jest wyrażony w C. Następnie możemy argumentować krok po kroku, że robi to, co powinien. Więc moje pytanie brzmi: Podaj przykład algorytmu, który jest odpowiedni,...
Znam mało teorii typów zależnych. Z wikipedii: Typ zależny to typ, którego definicja zależy od wartości. I z mojego kursu teorii typów przypominam, że typ zależny to: Rodzina typów indeksowana według typu. Ale mam wątpliwości co do typów zależnych i typów udoskonalania oraz logiki...
Czy problemy typu „obecność na imprezie” można rozwiązać w Prologu? Na przykład: Łopian Muldoon i Carlotta Pinkstone powiedzieli, że przybędą, jeśli przyjdzie Albus Dumbledore. Albus Dumbledore i Daisy Dodderidge powiedzieli, że przybędą, jeśli przyjdzie Carlotta Pinkstone. Albus Dumbledore,...
Zacząłem czytać coraz więcej prac naukowych dotyczących języków. Uważam to za bardzo interesujące i dobry sposób, aby dowiedzieć się więcej o programowaniu w ogóle. Zazwyczaj jednak pojawia się sekcja, z którą zawsze się zmagam (na przykład część trzecia tego ), ponieważ brakuje mi teoretycznego...
Czy ktoś kiedykolwiek napisał system (oprogramowanie lub szczegółowe wyjaśnienie na papierze z prostymi przykładami), który generuje programy komputerowe? Wprowadzam i tworzy program, który wyświetla liczby pierwsze mniejsze niż 10. P r i m e ( x ) jest po prostu zdefiniowany jako 1 < x ∧ ∄...
xorbrama, teraz muszę zbudować tę bramę, używając tylko 4 nandbram a b out 0 0 0 0 1 1 1 0 1 1 1 0 the xor = (a and not b) or (not a and b), czyli A¯¯¯¯B+AB¯¯¯¯A¯B+AB¯\begin{split}\overline{A}{B}+{A}\overline{B}\end{split} Znam odpowiedź, ale jak uzyskać schemat bramy ze...
Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i zamieszczam serię pytań na temat tego procesu, zaczynając tutaj . Ciągle czytam o algorytmie unifikacji . Co to jest i dlaczego jest tak ważne dla silników wnioskowania ? Dlaczego jest tak ważny dla...
Próbowałem wymyślić system, który oceniałby regulaminy organizacji w celu ustalenia ich podstawowej logiki. Myślę, że system predykatów pierwszego rzędu działałby w celu reprezentowania reguł, które mogłyby być przetłumaczone z tekstu za pomocą tagowania części mowy i innych technik NLP. Czy...
Uczę się samodzielnie Automated Theorem Proving / Solver SMT / Proof Assistants i zamieszczam serię pytań na temat tego procesu, zaczynając tutaj . Dlaczego automatyczne dowodzenia twierdzeń, tj. ACL2 i solwery SMT, nie potrzebują ludzkiej pomocy, podczas gdy asystenci dowodzenia, tj. Isabelle i...
Kombinator Y ma typ . Według korespondencji Curry-Howarda, ponieważ typ ( a → a ) → a jest zamieszkały, musi odpowiadać prawdziwemu twierdzeniu. Jednak a → a jest zawsze prawdziwe, więc wydaje się, że typ kombinatora Y odpowiada twierdzeniu a , co nie zawsze jest prawdziwe. Jak to może być?( a → a...
Jestem samoukiem, asystentem ds. Dowodów i postanowiłem zacząć od kilku podstawowych dowodów i podążać swoją drogą. Ponieważ dowody są oparte na innych dowodach, a zatem tworzą hierarchię, czy istnieje repozytorium hierarchii dowodów? Wiem, że mogę wybrać konkretnego asystenta proofów i...
Pracuję nad kompilatorem dla języka konkatenatywnego i chciałbym dodać obsługę wnioskowania typu. Rozumiem Hindleya-Milnera, ale nauczyłem się teorii typów, więc nie jestem pewien, jak ją dostosować. Czy następujący system jest dźwiękowy i można go w sposób zdecydowanie wywnioskować? Termin jest...
Próbuję owinąć głowę wokół dowodu kompletności NP, który wydaje się obracać wokół SAT / 3CNF-SAT. Może jest późna godzina, ale obawiam się, że nie mogę wymyślić formuły 3CNF, której nie można spełnić (prawdopodobnie brakuje mi czegoś oczywistego). Czy możesz podać mi przykład takiej...
Kolejność aplikacji: Zawsze w pełni oceniaj argumenty funkcji przed oceną samej funkcji, na przykład - (λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(λx.x2(λx.(x+1) 2)))→(λx.x2(2+1))→ (λx.x2(3))→ 32 → 9(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x....
Oto kontekst ( Struktura i interpretacja programów komputerowych , sekcja 1.1.8, pod nagłówkiem „Nazwy lokalne”): Formalny parametr procedury ma bardzo szczególną rolę w definicji procedury, ponieważ nie ma znaczenia, jaką nazwę ma parametr formalny. Taka nazwa nazywa się zmienną powiązaną i...
Rozumiem znaczenie, jakie informatycy lub inżynierowie związani z opracowywaniem oprogramowania powinni rozumieć jako podstawy badania logiki podstawowej. Ale czy są jakieś zadania / zadania, które wyraźnie wymagają wiedzy na ich temat, inne niż zadania wymagające jakiejkolwiek reprezentacji...
Jestem programistą z automatami, ale nie logiką. Przeczytałem w artykułach, że te dwa są ze sobą ściśle powiązane. Deterministyczne automaty skończone (DFA), automaty drzewa i automaty z widocznym przesunięciem w dół są powiązane z logiką Monadic drugiego rzędu (MSO). Chociaż rozumiem automaty i...
Załóżmy, że mamy prosty język, który składa się z terminów: truetrue\mathtt{true} falsefalse\mathtt{false} jeśli są warunkami, to podobnie jest zi ft1,t2,t3t1,t2,t3t_1,t_2,t_3ift1thent2elset3ift1thent2elset3\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 Załóżmy teraz następujące...
Myślałem o dowodach i natknąłem się na ciekawą obserwację. Tak więc dowody są równoważne programom za pomocą izomorfizmu Curry'ego-Howarda, a dowody kołowe odpowiadają nieskończonej rekurencji. Wiemy jednak z problemu zatrzymania, że ogólne testowanie, czy dowolny program powróci na zawsze, jest...