Fundovaná rekurze
Author
Albert FloresFundovaná rekurze je matematický pojem z oblasti teorie množin, který zobecňuje transfinitní rekurzi.
Věta o fundované rekurzi
Věta o fundované rekurzi zní takto:
Nechť R je úzká fundovaná binární relace a G je třídová funkce definovaná na celé univerzální třídě. Pak existuje jediná funkce F definovaná na univerzální třídě splňující F(x)=G(F|\{y;yRx\}) pro všechna x.
Náznak důkazu
Definujme nejprve třídu P všech „parciálních“ funkcí f, tj. takových, jejichž definiční obor je R-tranzitivní množina (množina uzavřená na R-předchůdce svých prvků) a které splňují f(x)=G(f|\{y;yRx\}) pro všechna x z definičního oboru f. +more Fundovanou indukcí (podle R) se snadno dokáže, že pro funkce f,g z P a x z průniku jejich definičních oborů je f(x)=g(x) a dále, že každé x je v definičním oboru nějaké funkce z P. Pak F= \bigcup A je funkce definovaná na univerzální třídě vyhovující tvrzení věty.