Kombinatory dla pierwotnych funkcji rekurencyjnych

Powszechnie wiadomo, że kombinatory S i K są Turing Complete. Czy istnieją kombinatory, które wystarczają, aby uzyskać (tylko) pierwotne funkcje rekurencyjne?

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 $S$$K$

$$\begin{array}{lcl} K & : & A \to B \to A \\ S & : & (A \to B \to C) \to (A \to B) \to (A \to C) \end{array}$$ $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 → $\mathbb{N}$

$$\begin{array}{lcl} z & : & \mathbb{N} \\ succ & : & \mathbb{N} \to \mathbb{N} \\ iter & : & \mathbb{N} \to (\mathbb{N} \to \mathbb{N}) \to \mathbb{N} \to \mathbb{N} \end{array}$$

Reguły równości dla dodatków to:

$$\begin{array}{lcl} iter\;i\;f\;z & = & i \\ iter\;i\;f\;(succ\;e) & = & f(iter\;i\;f\;e) \end{array}$$

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.

$$\begin{array}{lcl} iter & : & A \to (A \to A) \to \mathbb{N} \to A \end{array}$$ $iter$

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ć:$\mathit{iter}$

$$\begin{array}{lcl} pred' & = & \lambda k.\;iter \;(z, z) \; (\lambda (n, n').\; (succ\;n, n))\;k\\ pred & = & \lambda k.\;snd(pred'\;k) \end{array}$$

Jeśli masz tylko iterator typu nat, musisz wykorzystać izomorfizm, który , co jest denerwujące, ale nie stanowi podstawowej przeszkody.$\mathbb{N} \simeq \mathbb{N} \times \mathbb{N}$