Czy twierdzenie smn to ta sama koncepcja co curry?

Studiuję twierdzenie smn, a koncepcja przypominała mi curry.

Z artykułu w Wikipedii o twierdzeniu smn :

twierdzenie mówi, że dla danego języka programowania i dodatnich liczb całkowitych m i n istnieje szczególny algorytm, który przyjmuje jako dane wejściowe kod źródłowy programu z m + n dowolnymi zmiennymi, wraz z m wartościami. Ten algorytm generuje kod źródłowy, który skutecznie zastępuje wartości pierwszych m wolnych zmiennych, pozostawiając resztę zmiennych wolnych.

Z artykułu o curry :

Intuicyjnie curry mówi „jeśli naprawisz niektóre argumenty, otrzymasz funkcję pozostałych argumentów”

Wydaje mi się, że ten sam pomysł jest dla mnie. Jedynym powodem, dla którego nie jestem pewien, jest to, że materiały, które natknąłem się na smn, nie wspominają o curry (i vice versa), więc chciałem się z nimi skonsultować, aby upewnić się, że naprawdę je otrzymam.

computability

— emanek
źródło

W rzeczy samej. Niektóre dowody obliczeniowe mają smak jagnięcia. Twierdzenie smn, z grubsza, pozwala udawać, że indeksy funkcji rekurencyjnych są terminami lambda, tak że biorąc pod uwagę możemy stworzyć nieformalne i twierdzą, że jest pierwotną rekurencyjną. Nawet drugi dowód twierdzenia o rekurencji (wykorzystujący smn) jest kombinatorem kumulatora stałoprzecinkowego w przebraniu, ukrytym za zastosowaniami . Kluczową kwestią jest to, że nawet jeśli zdefiniowano wyliczenie wyliczając, powiedzmy, TM (lub Java, lub ...), nadal możemy udawać, że mamy lambdas!

ϕ_{i} (-, -)

$\phi_i(-,-)$

g (x) = # λ y . ϕ_{i} (x, y)

$g(x) = \#\lambda y. \phi_i(x,y)$

g

$g$

s ()

$s()$

ϕ_{i}

$\phi_i$

— chi

Cóż, smn tworzy instrukcję egzystencjalną, podczas gdy istnienie funkcji curry zapewnia „kompilator”. Ale pomysł jest taki sam.

— Raphael

Tak, to jest to samo.

Curry to koncepcja z rachunku. Jest to transformacja między i . Pomyśl o tym jak „jeśli mamy funkcję dwóch argumentów typu i , wówczas możemy naprawić pierwszy argument (typu ), a otrzymamy funkcję pozostałego argumentu (typu )”. W rzeczywistości ta transformacja jest izomorfizmem. Dokonują tego matematycznie precyzyjne modele matematyczne (typowanego) rachunku, które są kartezjańskimi kategoriami zamkniętymi . $\lambda$ $A \times B \to C$ $A \to (B \to C)$ $A$ $B$ $A$ $B$ $\lambda$

Istnieje kategoria zestawów numerowanych. Zestaw numerowany jest parą gdzie jest zbiorem, a jest częściowym przypuszczeniem, tj. Mapą liczb na , która również może być niezdefiniowana. Jeśli mówimy, że jest to kod o . W teorii obliczalności istnieje wiele przykładów. Ilekroć kodujemy jakieś informacje za pomocą liczby, otrzymujemy zestaw numerowany. Na przykład istnieje standardowa numeracja $(A, \nu_A)$ $A$ $\nu_A : \mathbb{N} \to A$ $A$ $\nu_A(n) = x$ $n$ $x$ częściowych funkcji obliczalnych, tak że jest liczbą obliczoną przez częściową funkcję obliczalną zakodowaną przez gdy zastosowana do . (Wynik może być niezdefiniowany.) $\varphi$ $\varphi_n(k)$ $n$ $k$

Morfizm zbiorów numerowanych to zrealizowana mapa , co oznacza, że istnieje takie że dla wszystkich w dziedzinie . To wygląda na skomplikowane, ale mówi tylko tyle, że $f : (A, \nu_A) \to (B, \nu_B)$ $n \in \mathbb{N}$ $f(\nu_A(k)) = \nu_B(\varphi_n(k))$ $k$ $\nu_A$ $\varphi_n$ robi kodom, co robi z elementami. Jest to matematyczny sposób powiedzenia, że „program implementuje funkcję ”. $f$ $\phi_n$ $f$

Oto punkt zwrotny: kategoria zestawów numerowanych jest kartezjańska zamknięta. Możemy zatem zinterpretować w nim wpisany calulus i zapytać, jaki program realizuje operację curry. Odpowiedź brzmi: program podany przez twierdzenie smn. $\lambda$

— Andrej Bauer
źródło

Ciekawy. Czy ta kategoria jest ściśle związana z

wydaje się indukować PER.

P E R (A)

$PER(A)$

ν_{A}

$\nu_A$

— chi

Tak, te dwie kategorie są równoważne, a trzecia równoważna wersja to wersja skromnych zestawów (wyszukaj „skromne zestawy i zespoły”).

— Andrej Bauer,