Fundovaná rekurze

Fundovaná 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. 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.

Související články

• Fundovaná indukce
• Transfinitní rekurze