Powszechnie wiadomo, że kombinatory S i K są Turing Complete. Czy istnieją kombinatory, które wystarczają, aby uzyskać (tylko) pierwotne funkcje rekurencyjne?
Powszechnie wiadomo, że kombinatory S i K są Turing Complete. Czy istnieją kombinatory, które wystarczają, aby uzyskać (tylko) pierwotne funkcje rekurencyjne?
Odpowiedzi:
Tak, ale musisz wziąć pod uwagę kombinatory maszynowe. Oznacza to, że musisz podać i następujące schematy typów: gdzie i są meta-zmiennymi, które mogą być tworzone przy użyciu dowolnego konkretnego typu przy każdym użyciu.K K : A → B → A S : ( A → B → C ) → ( A → B ) → ( A → C ) A , B C
Następnie chcesz dodać typ liczb naturalnych do języka typów i dodać następujące kombinatory: z : N s u c c : N → N i t e r : N → ( N → N ) → N → N
Reguły równości dla dodatków to:
O wiele łatwiej jest czytać pisane programy, jeśli po prostu piszesz programy w prostym typie rachunku lambda, powiększonego o cyfry i iterację. System, który opisałem, jest ograniczeniem T Goedela , języka arytmetyki wyższego typu. W Goedel's T wpisywanie iteracji jest mniej ograniczone: W T , możesz utworzyć na dowolnym typie, a nie tylko na liczbach naturalnych. To prowadzi Cię do prymitywnej rekurencji i pozwala zdefiniować takie rzeczy, jak funkcja Ackermana.
EDYCJA: Xoff zapytał, jak zakodować funkcję poprzednika. Wynika to standardową lewą. Aby to wyjaśnić, użyję do tego notacji lambda (którą można wyeliminować za pomocą abstrakcji nawiasów), ponieważ jest to o wiele bardziej czytelne. Najpierw załóżmy, że mamy pary i bardziej ogólny typ dla . Następnie możemy zdefiniować:
Jeśli masz tylko iterator typu nat, musisz wykorzystać izomorfizm, który , co jest denerwujące, ale nie stanowi podstawowej przeszkody.
iter
. To może być przedmiotem pytania na cs.stackexchange.com ...