Pytania otagowane jako typed-lambda-calculus

3
Czy wpisane obliczenia lambda wyrażają * wszystkie * algorytmy poniżej określonej złożoności?
Wiem, że złożoność większości odmian kalkulatorów lambda bez prymitywu kombinatora Y jest ograniczona, tzn. Można wyrazić tylko funkcje o ograniczonej złożoności, przy czym granica staje się większa wraz ze wzrostem ekspresyjności systemu typów. Pamiętam, że np. Rachunek konstrukcji może wyrażać co najwyżej podwójnie wykładniczą złożoność. Moje pytanie dotyczy tego, czy …
2
Jak zdobyć Rachunek Konstrukcji z innych punktów w Kostce Lambda?
CoC jest zwieńczeniem wszystkich trzech wymiarów Lambda Cube. To wcale nie jest dla mnie oczywiste. Wydaje mi się, że rozumiem poszczególne wymiary, a połączenie dowolnych dwóch wydaje się skutkować względnie prostym zjednoczeniem (może czegoś mi brakuje?). Ale kiedy patrzę na CoC, zamiast wyglądać jak połączenie wszystkich trzech, wygląda to zupełnie …
2
Czy istnieje typowany rachunek lambda, który jest spójny i kompletny Turinga?
Czy istnieje typowany rachunek lambda, w którym odpowiednia logika w korespondencji Curry-Howarda jest spójna i gdzie istnieją możliwe do wpisania wyrażenia lambda dla każdej funkcji obliczeniowej? Jest to wprawdzie pytanie nieprecyzyjne, pozbawione precyzyjnej definicji „typowanego rachunku lambda”. Zastanawiam się, czy istnieją (a) znane przykłady tego, lub (b) znane dowody niemożności …
1
Historyczna relacja między wpisaną metodą Lambda Calculus a Lisp?
Niedawno rozmawiałem z przyjacielem (który jest zwolennikiem silnie pisanych języków). Skomentował: Wynalazcy Lambda Calculus zawsze zamierzali go pisać na maszynie. Teraz widzimy, że Kościół był związany z tym po prostu wpisane rachunek lambda . Rzeczywiście wydaje się, że wyjaśnił on prosty typ rachunku Lambda, aby ograniczyć nieporozumienia dotyczące rachunku Lambda. …
3
Rachunek konstrukcji: skompresuj wyrażenie do jego najmniejszej postaci
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 niektórych przypadkach normalizacja może zredukować małe wyrażenie do …
1
Techniki dowodowe pokazujące, że sprawdzanie typu zależnego jest rozstrzygalne
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ść sprawdzania typów jest wymieniona jako następstwo silnej …
1
Algorytmy inwersji programów dla programów wyższego rzędu
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. Programowanie odwracalne (fizyczne i logiczne), częściowa ocena, weryfikacja, programowanie …
1
Zrozumienie dowodu silnej normalizacji rachunku konstrukcji
Mam trudności ze zrozumieniem dowodu silnej normalizacji dla rachunku konstrukcji. Staram się podążać za dowodem zawartym w pracy Hermana Geuversa „Krótki i elastyczny dowód silnej normalizacji dla rachunku konstrukcji”. Potrafię dobrze podążać za główną linią rozumowania. Konstrukcje Geuvers dla każdego typuTTT interpretacja [[T]]ξ[[T]]ξ[\![T]\!]_\xi na podstawie pewnej oceny zmiennych typu ξ(α)ξ(α)\xi(\alpha). …
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.