Czego Idris nie może zrobić, rezygnując z kompletności Turinga?

35

Wiem, że Idris ma typy zależne, ale nie jest kompletny. Czego nie może zrobić, rezygnując z kompletności Turinga i czy wiąże się to z posiadaniem typów zależnych?

Wydaje mi się, że jest to dość specyficzne pytanie, ale nie wiem zbyt wiele o typach zależnych i pokrewnych systemach typów.

Kałamarnica
źródło
2
Myślę, że szukasz konkretnego przykładu? Nie znam Idris, ale w Isabelle / HOL nie możesz pisać (a raczej kompilować) funkcji, które nie zawsze kończą się (gorzej, musisz podać dowód zakończenia ).
Raphael
Coś w tym stylu tak - nie byłem do końca pewien, czy będzie coś niszowego, na przykład nie można zakodować języka z pewnymi właściwościami w systemie pisma lub czy byłby on nieco bardziej ogólny (np. Jak powiedziałeś , wszystkie funkcje muszą zostać zakończone)
Squidly
1
Zgadnij, że to błędne założenie pochodzi od Edwina Brady'ego, mówiącego, że Idris jest „Pacman ukończony”. Myślę, że jego głównym punktem mówiąc „Pacman skompletowany” zamiast „Turing zakończony” jest to, że chce podkreślić znaczenie łatwej kompilacji języków przez ludzki mózg, a nie tylko maszyny! .. głupie języki, takie jak BrainFuck, są z pewnością Turing zakończony, ale ludzki mózg może potrzebować sporo czasu, aby zrozumieć kod napisany w BrainFuck, a zatem opracowanie, a nawet ważniejsze utrzymanie , programu Pacman w BrainFuck wymaga sporego wysiłku.
Michelrandahl
@Mitzh Nie bardzo. Myślę, że to dlatego, że źle zrozumiałem coś, co słyszałem, jak mówił podczas rozmowy.
Squidly

Odpowiedzi:

50

Idris kończy Turinga! Sprawdza całkowitość (zakończenie przy programowaniu z danymi, produktywność podczas programowania z kodami), ale nie wymaga, aby wszystko było całkowite.

Co ciekawe, posiadanie danych i danych jest wystarczające do modelowania kompletności Turinga, ponieważ można napisać monadę dla funkcji częściowych. Zrobiłem to wiele lat temu w Coq - prawdopodobnie jest to teraz bitrotted, ale tutaj jest jednak: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

Aby uruchomić takie rzeczy, potrzebujesz jednej ucieczki, ale Idris pozwala ci to zrobić.

Idris nie ograniczy funkcji częściowych na poziomie typu, aby utrzymać decydowanie o sprawdzeniu typu. Ponadto tylko dowody można w uzasadniony sposób uznać za programy ogółem.

Edwin Brady
źródło
4
Sam człowiek. Czym jest wydajność w tym kontekście?
Squidly
5
Podwójne do terminacji: podczas gdy definicja indukcyjna musi zakończyć się (poprzez wykorzystanie wszystkich jej danych), definicja koindukcyjna musi być produktywna - w praktyce oznacza to, krótko mówiąc, że każde wywołanie rekurencyjne musi być strzeżone przez konstruktora. To wyjaśnienie jest najczystsze (ymmv): adam.chlipala.net/cpdt/html/Coinductive.html
Edwin Brady
14

Po pierwsze, zakładam, że już słyszałeś o tezie Churcha-Turinga , która stwierdza, że ​​wszystko, co nazywamy „obliczeniem”, jest czymś, co można zrobić za pomocą maszyny Turinga (lub dowolnego z wielu innych równoważnych modeli). Tak więc język kompletny Turinga to taki, w którym można wyrazić dowolne obliczenia. I odwrotnie, język niekompletny Turinga to taki, w którym istnieje pewne obliczenia, których nie można wyrazić.

Ok, to nie było zbyt pouczające. Podam przykład. Jest jedna rzecz, której nie można zrobić w żadnym niekompletnym języku Turinga: nie można napisać symulatora maszyny Turinga (w przeciwnym razie można zakodować dowolne obliczenia na symulowanej maszynie Turinga).

Ok, to wciąż nie było zbyt pouczające. prawdziwe pytanie brzmi: jakiego użytecznego programu nie można napisać w języku niekompletnym Turinga? Cóż, nikt nie wymyślił definicji „użytecznego programu”, który obejmuje wszystkie programy, które ktoś gdzieś napisał w przydatnym celu, i które nie obejmują wszystkich obliczeń maszyn Turinga. Zatem zaprojektowanie niekompletnego języka Turinga, w którym można pisać wszystkie przydatne programy, jest nadal bardzo długoterminowym celem badawczym.

Obecnie istnieje kilka bardzo różnych rodzajów niekompletnych języków Turinga i różnią się tym, czego nie potrafią. Istnieje jednak wspólny temat: języki Turing-complete muszą zawierać sposób warunkowego zakończenia lub kontynuowania pracy na czas, który nie jest ograniczony rozmiarem programu, oraz sposób na wykorzystanie przez program ilości pamięci zależnej od danych wejściowych . Konkretnie, większość imperatywnych języków programowania zapewnia te umiejętności odpowiednio poprzez pętle while i dynamiczną alokację pamięci. Większość funkcjonalnych języków programowania zapewnia te umiejętności poprzez rekurencję i zagnieżdżanie struktury danych.

Idris jest silnie zainspirowany Agdą . Agda to język przeznaczony do dowodzenia twierdzeń . Teraz dowodzenie twierdzeń i uruchamianie programów są ze sobą ściśle powiązane , więc możesz pisać programy w Agdzie tak, jak dowodzisz twierdzenia. Intuicyjnie dowód twierdzenia „A implikuje B” jest funkcją, która przyjmuje dowód twierdzenia A jako argument i zwraca dowód twierdzenia B.

Ponieważ celem systemu jest udowodnienie twierdzeń, nie można pozwolić programiście pisać dowolnych funkcji. Wyobraź sobie, że język pozwolił ci napisać głupią funkcję rekurencyjną, która właśnie się wywołała:

oops : A -> B
oops x = oops x

Nie możesz pozwolić, by istnienie takiej funkcji przekonało cię, że A implikuje B, bo inaczej byłbyś w stanie udowodnić cokolwiek, a nie tylko prawdziwe twierdzenia! Zatem Agda (i podobne dowody twierdzeń) zabrania arbitralnej rekurencji. Pisząc funkcję rekurencyjną, musisz udowodnić, że zawsze się kończy , aby za każdym razem, gdy uruchomisz ją na dowodzie twierdzenia A, będziesz wiedział, że skonstruuje on dowód twierdzenia B.

Bezpośrednim praktycznym ograniczeniem Agdy jest to, że nie można pisać dowolnych funkcji rekurencyjnych. Ponieważ system musi być w stanie odrzucić wszystkie funkcje nie kończące się, nierozstrzygalność problemu zatrzymania (lub bardziej ogólnie twierdzenie Rice'a ) zapewnia, że ​​istnieją również funkcje kończące, które zostały odrzucone. Dodatkową trudnością praktyczną jest to, że musisz pomóc systemowi udowodnić, że twoja funkcja się kończy.

Trwa wiele badań nad ulepszeniem systemów dowodzenia w języku programowania bez uszczerbku dla ich gwarancji, że jeśli masz funkcję od A do B, jest to równie dobry dowód matematyczny, że A implikuje B. Rozszerzenie systemu na więcej kończenie funkcji jest jednym z tematów badawczych. Inne kierunki rozszerzenia obejmują radzenie sobie z takimi „rzeczywistymi” problemami, jak wejście / wyjście i współbieżność. Kolejnym wyzwaniem jest uczynienie tych systemów dostępnymi dla zwykłych śmiertelników (lub być może przekonanie zwykłych śmiertelników, że w rzeczywistości są dostępne).

Nie znam Idrisa. To podejście do wyzwań, o których właśnie wspomniałem. O ile rozumiem od pobieżnego spojrzenia na przedruk 2013 , Idris jest kompletem Turinga, ale zawiera sprawdzanie całości. Kontroler sumowania sprawdza, czy każda funkcja opatrzona słowem kluczowym totalkończy się. Fragment języka, który zawiera tylko programy Idris, w których każda funkcja jest suma, ma podobną moc ekspresyjną do Ardy (prawdopodobnie nie jest to dokładne dopasowanie z powodu różnic w teorii typów, ale wystarczająco blisko, abyś nie zauważył, chyba że celowo próbowałeś).

Aby zapoznać się z innymi przykładami języków, które nie są kompletne w Turinga na różne sposoby, zobacz Jakie są praktyczne ograniczenia niekompletnego języka, takiego jak Coq? (z którego ta odpowiedź pochodzi w dużej mierze).

Gilles „SO- przestań być zły”
źródło
3
„jaki użyteczny program nie może być napisany w języku niekompletnym Turinga?” Maszyna wirtualna Java.
David Richerby
@DavidRicherby Nie możesz? Czy JVM jest naprawdę kompletny w Turingu? Istnieje limit wielkości pojedynczego obiektu, czy możesz zorganizować przydzielenie i dostęp do nieograniczonej liczby obiektów? Na przykład w C odpowiedź wydaje się przecząca, ponieważ istnieje tylko skończenie wiele wartości wskaźnika.
Gilles „SO- przestań być zły”
Dla czytelników zainteresowanych tą częścią mamy kolejny post o tym, dlaczego nie może istnieć język programowania dla języków zawsze kończących.
Raphael
3
@Gilles Rozumiem twój punkt widzenia, ale czy nie jest to równoznaczne z powiedzeniem, że żaden rzeczywisty język programowania nie jest kompletny w Turingu? W końcu każda implementacja będzie napotykać na wspomniane bariery. To wydaje się być dość dużym słoniem w pokoju, biorąc pod uwagę to, co Idris traci, nie będąc kompletnym Turingiem. Czy na przykład traci więcej niż jakikolwiek inny język? Jeśli zabronisz nieograniczonej pamięci zewnętrznej (np. Program przestaje mówić „proszę włożyć następny / poprzedni dysk”), wówczas dowolny język nie jest w pełni Turing-complete, więc wszelkie pytania dotyczące tej sprawy są puste.
David Richerby
3
@DavidRicherby Moje komentarze (ale nie moja odpowiedź) są w trybie maniakiem teorii programowania. Jeśli weźmiesz formalną specyfikację SML (na przykład), możliwe jest zaprojektowanie (ale oczywiście nie zaimplementowanie w świecie fizycznym) implementacji języka, który może symulować wszystkie programy obliczalne. Nie jest tak w C, ponieważ skończoność pamięci jest wbudowana w język ( sizeof(void*)). W mojej odpowiedzi traktuję języki w wyidealizowany sposób, więc SML lub C można by uznać za kompletne Turinga.
Gilles „SO- przestań być zły”