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

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.

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.

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).