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.

Tak, to jest to samo.

Curry to koncepcja z rachunku. Jest to transformacja między A × B → C i A → ( B → C ) . Pomyśl o tym jak „jeśli mamy funkcję dwóch argumentów typu A i B , wówczas możemy naprawić pierwszy argument (typu A ), a otrzymamy funkcję pozostałego argumentu (typu B )”. 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 A jest zbiorem, a ν A : N → A jest częściowym przypuszczeniem, tj. Mapą liczb na A , która również może być niezdefiniowana. Jeśli ν ( n ) = x mówimy, że n jest to kod o x . 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 φ n ( k ) jest liczbą obliczoną przez częściową funkcję obliczalną zakodowaną przez n, gdy zastosowana do k . (Wynik może być niezdefiniowany.)$\varphi$$\varphi_n(k)$$n$$k$

Morfizm zbiorów numerowanych to zrealizowana mapa , co oznacza, że ​​istnieje n ∈ N, takie że f ( ν A ( k ) ) = ν B ( φ n ( k ) ) dla wszystkich k w dziedzinie v A . 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 ϕ n implementuje funkcję f ”.$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$