Reprezentowalność funkcji rekurencyjnych w A-rachunku

Lemat. Funkcje A-definiowalne są zamknięte ze względu na operację minimum.

Dowód. Niech funkcja g będzie A-definiowalna za pomocą termu G. Wówczas funkcja f{x) = (yim.g{x, m) = 0) jest A-definiowalna za pomocą termu

mi = Aa:.szukaj 0 x    (~»_v szukaj 0)

gdzie

szukaj = © Afmćc.if isZero (Gxm) thenm else f (sucm) x. Ponieważ © F -» F(© F), to

szukaj mx -» if isZero (Gxm) thenm else szukaj (sucm) x

Wobec tego szukaj 0 x zaczynając od zera poszukuje najmniejszej liczby m takiej, że (Gxm) — 0, co jest zgodne z definicją operacji minimum.

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