Pytania otagowane jako lambda-calculus

System formalny Kościoła używany w obliczeniach, językach programowania i teorii dowodów do reprezentowania skutecznych funkcji, programów i ich obliczeń oraz dowodów.

3
Czy jakieś znane CCC są zamknięte w ramach probabilistycznej operacji powerdomain?
Odpowiednio, czy istnieje znana semantyka denotacyjna dla probabilistycznych funkcjonalnych języków programowania wyższego rzędu? Konkretnie, czy istnieje model domenowy czystego nietypowego -kalkultu rozszerzony o symetryczną operację losowego wyboru binarnego.λλ\lambda Motywacja Kartezjańskie zamknięte kategorie zapewniają semantykę wyższego rzędu -calculi. Probabilistyczne powerdomains zapewniają semantykę programom stochastycznym. CCC zamknięty w ramach probabilistycznej operacji powerdomain …
1
Czy rachunek afiniczny lambda może rozwiązać każdy problem w P?
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ć dowód ze względu na złożoność). Byłoby to bardzo interesujące, gdybyśmy mogli rozwiązać każdy …
1
Odwołanie do niezdefiniowanego modułu ciągłości funkcjonalnej w PCF?
Czy ktoś może wskazać mi odniesienie do niezdefiniowalności modułu ciągłości funkcjonalnej w PCF? \ newcommand {\ bool} {\ mathsf {bool}}\newcommand{\N}{\mathbb{N}} \newcommand{\bool}{\mathsf{bool}} Andrej Bauer napisał bardzo fajny post na blogu , w którym szczegółowo omawia niektóre problemy, ale streszczę tylko trochę jego postu, aby nadać kontekst temu pytaniu. Baire'a przestrzeń jest …
1
Na jakie „pytanie” stara się odpowiedzieć teoria języka programowania?
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 różnymi ograniczeniami, staram się znaleźć analogię do „teorii programowania” Wikipedia …
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). …
1
Sprzeczność między drugim twierdzeniem Gödela o niekompletności a własnością Church-Rosser CIC?
Z jednej strony drugie twierdzenie Gödela o niekompletności stwierdza, że ​​żadna spójna teoria formalna, która jest wystarczająco silna, aby wyrazić dowolne podstawowe stwierdzenia arytmetyczne, nie może udowodnić swojej spójności. Z drugiej strony właściwość Churcha-Rossera systemu formalnego (przepisywania) mówi nam, że jest on spójny w tym sensie, że nie wszystkie równania …
2
Jaka jest korzyść z zapisu Krivine?
Widziałem, jak niektórzy ludzie używają notacji Krivine'a do aplikacji funkcji podczas prezentacji składni dla -calculus. Na przykład -term (z normalną konwencją, że aplikacja funkcji kojarzy się z lewą stroną, więc w rzeczywistości oznacza to ) jest napisane (z podobną konwencją, że w rzeczywistości oznacza ). Nie widzę sensu posiadania kolejnej …
1
Prosty dowód, że rozstrzygalność typowalności w systemie F ( ) implikuje rozstrzygalność sprawdzania typu?
Załóżmy, że nie znamy wyniku Joe B. Wellsa z 1994 roku, że zarówno typowość, jak i sprawdzanie typów są nierozstrzygalne w Systemie F (AKA ). W rachunku Lambda z typami Barendregta (1992) znalazłem dowód z powodu Maleckiego 1989, że sprawdzanie typów implikuje typowość. To dlatego, żeλ 2λ2)\lambda 2 istnieje taki, …
1
Jaka jest rola dwukolorowego rachunku konstrukcji?
Czytam więc trochę o opracowaniu, w szczególności algorytmach opartych na dwukolorowym rachunku budowy i jestem trochę zdezorientowany. Nie rozumiem, jaki dokładnie jest cel tegododob jadodobjaCC^{bi}jest. Wydaje się być identyczny zdodododoCCz wyjątkiem tego, że istnieje rozróżnienie między niejawnymi i jawnymi argumentami funkcji. W szczególności nie widzę, jak pozwala ci pisać( i …
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.