---
up:
  - "[[fonction récursive primitive]]"
tags:
  - s/informatique
  - s/maths/logique
aliases:
  - schéma µ borné
---

> [!proposition] schéma mu borné
> Soit $A \subseteq \mathbb{N}^{p+1}$ un [[ensemble récursif primitif]]
> La fonction $f \in \mathscr{F}_{p+1}$ définie comme suit est [[fonction récursive primitive|récursive primitive]] :
>  - $f(\overline{x}, z) = 0$ s'il n'existe pas d'entier $t \leq z$ tel que $(\overline{x}, t) \in A$
>  - sinon $f(\overline{x}, z)$ est égal au plus petit des entiers $t \leq z$ tels que $(\overline{x}, t) \in A$
> - i On utilisera la notation : $\boxed{f(\overline{x}, z) = \mu t \leq z ((\overline{x}, t) \in A)}$
> 
> > [!definition] Définition formelle
> > La fonction $f$ est définie par récurrence, [[fonction récursive primitive#^schema-par-cas|schéma de définition par cas]], et par [[fonction récursive primitive#^somme-et-produits-limites|somme limitée]] :
> >  - $f(\overline{x}, 0) = 0$
> >  - $f(\overline{x}, z+1) = f(\overline{x}, z)$ si $\sum\limits_{y=0}^{z} \Big( \chi _{A}(\overline{x}, y) \Big)\geq 1$ (permet de tester si au moins un $y \leq z$ est dans $A$)
> >  - $f(\overline{x}, z+1) = z+1$ sinon et si $(\overline{x}, z+1) \in A$
> >  - $f(\overline{x}, z+1) = 0$ dans les autres cas
^main