3148972478

Reprezentowalność funkcji rekurencyjnych w A-rachunku

Definicja. Funkcja częściowo rekurencyjna f :N^k —> N jest definiowalna w beztypowym rachunku lambda, jeśli istnieje zamknięty term F, spełniający dla dowolnych nj... nfc G N następujące warunki:

(i)    Jeśli f{n\... nfi) — m, to Fni... =g m;

(ii)    Jeśli wartość f{n\... nk) jest nieokreślona, to Fni... nk nie ma postaci normalnej.

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