Języki programowania dla wydajnych obliczeń

Niemożliwe jest napisanie języka programowania, który zezwala wszystkim maszynom, które zatrzymują się na wszystkich wejściach i żadnych innych. Wydaje się jednak, że łatwo jest zdefiniować taki język programowania dla dowolnej standardowej klasy złożoności. W szczególności możemy zdefiniować język, w którym możemy wyrazić wszystkie wydajne obliczenia i tylko wydajne obliczenia.

Na przykład, dla czegoś takiego jak : wybierz swój ulubiony język programowania, a po napisaniu programu (odpowiadającego Turing Machine ) dodaj trzy wartości do nagłówka: liczba całkowita i liczba całkowita oraz domyślne wyjście . Po skompilowaniu programu wypisz maszynę Turinga która otrzymała dane wejściowe rozmiaru uruchamia$P$$M'$$c$$k$$d$$M$$x$$n$$M'$ na dla c n k kroków. Jeśli M ′ nie zatrzyma się przed wykonaniem kroków c n k , wypisz domyślne wyjście $x$$c n^k$$M'$$c n^k$$d$. O ile się nie mylę, te języki programowania pozwolą nam wyrazić wszystkie obliczenia w i nic więcej. Jednak ten proponowany język z natury nie jest interesujący.$P$

Moje pytanie: czy istnieją języki programowania, które przechwytują podzbiory funkcji obliczeniowych (takich jak wszystkie wydajnie obliczalne funkcje) w nie-trywialny sposób? Jeśli nie, czy istnieje ku temu powód?

Jednym z języków próbujących wyrażać tylko wielomianowe obliczenia czasu jest rachunek różniczkowy lambda . Jego system typów jest zakorzeniony w logice liniowej. Ostatnia teza dotyczy wielomianowych obliczeń czasowych i stanowi dobre podsumowanie ostatnich zmian opartych na tym podejściu. Martin Hofmann pracuje nad tym tematem od dłuższego czasu. Starszą listę odpowiednich artykułów można znaleźć tutaj ; Wiele jego prac kontynuuje w tym kierunku.

Inne prace polegają na sprawdzeniu, czy program używa pewnej ilości zasobów, przy użyciu typów zależnych lub języka asemblowanego .

Jeszcze inne podejścia oparte są na formalnych rachunkach ograniczonych zasobami , takich jak warianty rachunku otoczenia.

Podejścia te mają właściwość polegającą na tym, że dobrze napisane programy spełniają określone ograniczenia zasobów. Zasób związany może być czasem lub przestrzenią i ogólnie może zależeć od wielkości danych wejściowych.

Wczesne prace w tym obszarze polegają na silnie normalizującym rachunku różniczkowym, co oznacza, że ​​wszystkie dobrze napisane programy zostają zatrzymane. System F , czyli polimorficzny rachunek lambda, silnie się normalizuje. Nie ma operatora punktu stałego, ale mimo to jest dość wyrazisty, choć nie sądzę, że wiadomo, z jaką klasą złożoności odpowiada. Z definicji każdy rachunek normalizujący silnie wyraża pewną klasę obliczeń kończących.

Język programowania Charity jest dość ekspresyjnym językiem funkcjonalnym, który zatrzymuje się na wszystkich wejściach. Nie wiem, jaką klasę złożoności może wyrazić, ale funkcję Ackermanna można zapisać w Charity.

Spójrz na artykuł Guillaume Bonfante, który zaproponował dwie charakterystyki dla Logspace i czasu wielomianowego przy użyciu języków programowania.

Guillaume Bonfante, Niektóre języki programowania dla Logspace i Ptime, AMAST 2006, LNCS 4019, ss. 66-80, 2006

Chciałbym również wspomnieć o teorii niejawnej złożoności jako podejściu do tego, ponieważ widziałem, że pojawia się ona w kilku dość powiązanych pytaniach. Cytując tę odpowiedź Neela Krishnaswamiego :

Podstawową techniką jest powiązanie klas złożoności z podsystemami logiki liniowej (tzw. „Lekka logika liniowa”), przy założeniu, że eliminacja cięć w systemie logicznym powinna być kompletna dla danej klasy złożoności (np. LOGSPACE, PTIME itp.). Następnie za pośrednictwem Curry-Howarda poznajesz język programowania, w którym dokładnie programy w danej klasie są wyraźne.

Dziwi mnie, że nikt nie wspominał o prymitywnej rekurencji. Ograniczając się do ograniczonych pętli (tj. Liczba iteracji dla każdej pętli musi zostać obliczona przed rozpoczęciem pętli), wynikowy program jest pierwotnie rekurencyjny, a zatem całkowity. Douglas Hofstadter zaproponował język programowania BLOOP, który zezwala na wszystkie i tylko prymitywne funkcje rekurencyjne.

Zobacz także Pola języka programowania PTIME i twórczości Japaridze na PTIME arytmetyka np http://arxiv.org/abs/0902.2969