3148972480

Reprezentowalność funkcji rekurencyjnych w A-rachunku

Lemat. Funkcje A-definiowalne są zamknięte ze względu na rekursję prostą.

{RecghOx = gx    J f(0,x) = g(x),

Rec g h (suc n) x = hn (Recghnx)x 1 f(S(n),£) = h{n, f(n,x),x),

Ideę obliczania rekursora wyjaśnia poniższy program (porównaj z programem dla poprzednika).

V := 0; 1 J	<0 ,g(x))
while y ^ n	do (* 2 = f(y,x) *)
begin
z := h(y, z,	^X’^>’ j«(t/,z> -* <suc
V ■= sucy\
end
'* z = f(n,x)	*)

Teraz ten algorytm możemy zapisać w postaci A-termu.

n-krotna operacji q

iteracja

Rec =

\ghnx.snó (Iter n (Ap.pair (suc (fstp)) (h (fstp) (snd p)x)) (pair 0 (gx))

Zdzisław Spławski: Teoretyczne Podstawy Języków Programowania, Wykład 4. Siła wyrazu rachunku A 18