Chciałbym tylko poznać kilka przykładów funkcji, które można obliczyć za pomocą niepisanego rachunku lambda, ale nie za pomocą wpisanego rachunku lambda. Jako że jestem początkującym, doceniłbym powtórzenie podstawowych informacji. Dzięki. Edycja: za pomocą kalkulatora lambda, miałem zamiar...
Próbowałem owinąć głowę wokół tego, co, dlaczego i jak rachunek, ale nie jestem w stanie poradzić sobie z „dlaczego to działa”?λλ\lambda „Intuicyjnie” dostaję model obliczeniowy Turing Machines (TM). Ale ta abstrakcja wprawia mnie w zakłopotanie.λλ\lambda Załóżmy, że bazy danych nie istnieją -...
Wiem, że Rachunek Konstrukcji jest silnie normalizujący, co oznacza, że każde wyrażenie ma normalną wartość, która nie może być beta, a jeszcze bardziej zmniejszona eta. W rzeczywistości jest to najbardziej wydajne wyrażenie, które oblicza tę samą wartość, co oryginalne wyrażenie. Ale w...
Problem reprezentowania zmiennych powiązanych w składni, a zwłaszcza podstawiania unikania przechwytywania, jest dobrze znany i ma wiele rozwiązań: zmienne nazwane z równoważnością alfa, wskaźniki de Bruijna, lokalna bezimienność, zbiory nominalne itp. Ale wydaje się, że istnieje inne dość...
W wielu podręcznikach łatwo jest przejrzeć dowody redukcji podmiotu i silnej normalizacji dla Systemu F, czasem też istnieją definicje Systemu F z parami, gdzie (t, r) jest terminem, a nie tylko kodowaniem. Pytanie brzmi: jakie byłoby odniesienie dla tego
W teorii złożoności definicja złożoności czasu i przestrzeni odnosi się do uniwersalnej maszyny Turinga: odpowiednio. liczba kroków przed zatrzymaniem i liczba dotkniętych komórek na taśmie. Biorąc pod uwagę tezę Kościoła-Turinga, powinno być możliwe zdefiniowanie złożoności również pod względem...
Jaka jest różnica nazywania calculus algebrą zamiast rachunku różniczkowego? Podnoszę to pytanie, ponieważ gdzieś przeczytałem wiersz „ λ- rachunek nie jest rachunkiem, ale algebrą” (iirc, przypisane Danie Scott). O co chodzi?
Tłumaczę książkę na temat LISP i oczywiście dotyka ona niektórych elementów rachunku. Zatem wzmiankowane jest pojęcie ekstensywności wraz z niektórymi modelami λ- rachunku, a mianowicie: P ω i D ∞ (tak, z nieskończonością u góry). I mówi się, że P ω jest ekstensjonalny podczas D ∞ nie...
Czytałem o dziedzicznej zamianie na prosty rachunek Lambda i na logiczną strukturę z odrębnymi terminami i typami. Zastanawiam się, czy są jakieś przykłady dziedzicznej substytucji w systemie o typie zależnym i hierarchii wszechświata? tzn. gdzie True:Set0:Set1:Set2True:Set0:Set1:Set2 True : Set_0...
Jedyną znaną mi definicją „rachunku różniczkowego” jest badanie granic, pochodnych, całek itp. W analizie. W jakim sensie rachunek lambda (lub rzeczy takie jak rachunek mu) jest „rachunkiem”? Jak to się ma do rachunku różniczkowego w
Jaki jest związek między prostym typem rachunku lambda a logiką wyższego rzędu? Pod Curry-Howardem wydaje się, że prosty typ rachunku lambda odpowiada logice zdań. Jak to się ma do logiki wyższego rzędu? Według tego poradnika Geuversa: http://typessummerschool07.cs.unibo.it/courses/geuvers-1.pdf...
Następujący termin λ, tutaj w formie normalnej: sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l)) (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c)) Implementuje algorytm sortowania dla list zakodowanych w kościele. Oznacza to, że wynik: sort...
Z artykułu na temat strategii oceny w Wikipedii: Pojęcie strategii redukcji w rachunku lambda jest podobne, ale wyraźne. Z artykułu na temat strategii redukcji na Wikipedii: Jest podobny, ale nieznacznie różni się od pojęcia strategii oceny w informatyce. Jakie jest subtelne rozróżnienie...
Następujący termin (przy użyciu indeksów bruijn): BADTERM = λ((0 λλλλ((((3 λλ(((0 3) 4) (1 λλ0))) λλ(((0 4) 3) (1 0))) λ1) λλ1)) λλλ(2 (2 (2 (2 (2 (2 (2 (2 0))))))))) Po zastosowaniu do numeru kościoła Nszybko ocenia się w normalnej formie u kilku istniejących ewaluatorów, w tym naiwnych . Jeśli...
Od jakiegoś czasu interesowałem się różnymi tematami, takimi jak logika kombinacyjna, rachunek lambda, programowanie funkcjonalne i studiowałem je. Jednak w przeciwieństwie do „teorii obliczeń”, która stara się odpowiedzieć na pytanie „obliczalności”, tj. Rzeczy, które można / nie można obliczyć z...
Kombinatory interakcji były wcześniej proponowane jako cel kompilacji dla rachunku λ. Ten papier implementuje pełny rachunek λ. Wiadomo również, że możliwe jest zoptymalizowanie kodowania sieci interakcji rachunku λ dla podzbioru terminów λ, który jest typowy dla EAL. W tym artykule...
Termin inwersja programu ma wiele odcieni znaczenia, ale prawdopodobnie zaczął się od pracy J. McCarthy'ego z 1956 r. Inwersja funkcji zdefiniowanych przez maszyny Turinga w kontekście sztucznej inteligencji. Do tej pory odkryto wiele połączeń między inwersją programu a innymi polami, np....
Jest to inspirowane tym pytaniem. Niech będzie zbiorem wszystkich kombinacji, które mają tylko dwie powiązane zmienne. Czy kombinatorycznie kompletny?C.dodo\mathcal{C}dodo\mathcal{C} Uważam, że odpowiedź jest przecząca, jednak nie udało mi się znaleźć odniesienia do tego. Byłbym również...
Jestem w sytuacji, w której muszę pokazać, że sprawdzanie typu ma decydujący wpływ na rachunek różniczkowy, nad którym pracuję. Do tej pory udało mi się udowodnić, że system silnie się normalizuje, a zatem równość definicyjna jest rozstrzygalna. W wielu źródłach, które czytam, rozstrzygalność...
W Zaawansowanych tematach w typach i językach programowania w rozdziale o podstrukturalnych systemach typów wspomniano, że „starannie spreparowany” rachunek afiniczny lambda z kombinatorem rekurencyjnym dla list może wpisywać tylko terminy, które mają wielomianowy czas działania (nie przedstawić...