Język programowania, który może implementować tylko obliczalne funkcje bijectywne?

Czy istnieją języki programowania (lub logika), które mogą implementować (lub wyrażać) funkcję tylko i tylko wtedy, gdy jest obliczalną funkcją bijectywną? $f:\mathbb{N}\to \mathbb{N}$ $f$

— Chao Xu
źródło

Ktoś udowodnił mi, że nie można stworzyć języka, który akceptuje tylko programy kończące. Ponieważ twoje pytanie jest dość podobne, myślę, że nie.

— FUZxxl

Wydaje się mało prawdopodobne, aby istniał taki język programowania, myślę, że mógłbyś spróbować go wymusić, ale wtedy nie byłbyś w stanie robić prostych rzeczy, takich jak sortowanie, przynajmniej nie bez jego okropnej złożoności i bolesności.

— Luke Mathieson

@FUZxxl To nie przechwytuje wielu programów kończących, W rzeczywistości nawet funkcja f (x) = 1 jest niemożliwa do wyrażenia w tym języku. Mam również wrażenie, że tego rodzaju funkcje są przechwytywane przez całkowite programowanie funkcjonalne, ponieważ każda funkcja jest funkcją całkowitą.

— Chao Xu,

@FUZxxl, nie sądzę, że to prawda, ale taki język musiałby być ograniczony. Na przykład język, który byłby równoważny skończonym automatom deterministycznym, miałby zagwarantowane zakończenie, ale byłby bardzo ograniczony w zakresie tego, co mógłby obliczyć.

— jmite

@FUZxxl, szczegóły takiego oświadczenia są ważne. Łatwo jest zaprojektować język programowania, w którym kończy się każdy program. Inną sprawą jest zaprojektowanie języka, w którym będziemy mogli wyrazić każdą funkcję obliczalną.

— Vijay D

Nie ma takiego języka.

Spójrz jednak na Boomerang . Jest to język do pisania bijectów między łańcuchami. Nie wiem, jak szeroka jest w niej klasa map, ale jestem pewien, że dowiesz się, jeśli trochę poszukasz.

Uzasadnione jest wymaganie od języka programowania, aby zestaw prawidłowych programów był rozpoznawalny przez interpretera lub kompilator, tj. Aby był zestawem obliczalnym obliczalnie. Załóżmy, że mamy język programowania, którego zestaw poprawnych programów można było wyliczyć i który dokładnie zaimplementował wszystkie obliczalne bijections . Oznaczałoby to, że możemy obliczalnie wyliczyć wszystkie obliczalne bijectacje (po prostu wyliczyć wszystkie prawidłowe programy w tym języku programowania), ale nie jest to możliwe w kolejnym twierdzeniu. $\mathbb{N} \to \mathbb{N}$

Twierdzenie: że to obliczalna sekwencja obliczalnych bijectów. Następnie jest obliczalny bijection, który nie znajduje się w sekwencji. $f_0, f_1, f_2, \ldots$

Dowód. Konstruujemy bijection w następujący sposób. W celu określenia wartości i , patrzymy na : $g : \mathbb{N} \to \mathbb{N}$ $g(2 k)$ $g(2 k + 1)$ $f_k(2 k)$

Jeśli , a następnie zestaw oraz , $f_k(2 k) = 2 k$ $g(2 k) = 2 k + 1$ $g(2 k + 1) = 2 k$
Jeśli następnie zestaw i . $f_k(2 k) \neq 2 k$ $g(2 k) = 2 k$ $g(2 k + 1) = 2 k + 1$

Oczywiście, dla każdego , różni się od ponieważ . Co więcej, jest obliczalny i jest to bijection, ponieważ jest on własną odwrotnością. CO BYŁO DO OKAZANIA. $k \in \mathbb{N}$ $g$ $f_k$ $g(2 k) \neq f_k(2 k)$ $g$

— Andrej Bauer
źródło

Dlaczego w ogóle potrzebujesz tej sztuczki i ? Korzystanie powinno wystarczyć.

2 k

$2k$

2 k + 1

$2k+1$

g (k) = f_{k} (k) + 1

$g(k)=f_k(k)+1$

— FUZxxl,

@FUZxxl: jeśli użyjesz wynikowa funkcja nie będzie narzucająca się

f_{k} (k) + 1

$f_k(k)+1$

— Vor

Musisz upewnić się, że jest bijective.

g

$g$

— Andrej Bauer

Wstępne stwierdzenie jest błędne, w literaturze jest wiele takich języków.

— Nathaniel

Z drugiej strony twój dowód wydaje się wiarygodny. Być może jestem jakoś zdezorientowany. Muszę uważnie przeczytać artykuł Axelsena i Glucka (patrz moja odpowiedź), aby dowiedzieć się, co się tutaj dzieje.

— Nathaniel