From 3bb775a68241658eb3f2d6ee3ec4e31aae4391e9 Mon Sep 17 00:00:00 2001 From: oskar Date: Sun, 22 Mar 2026 01:36:08 +0100 Subject: [PATCH] MacBook-Pro-de-Oscar.local 2026-3-22:1:36:7 --- .obsidian/plugins/header-enhancer/data.json | 2 +- S2 LOGOS . incomplétude et indécidabilité.md | 6 +++- fonction d'ackermann de cori et lascar.md | 35 ++++++++++++++++++++ fonction récursive primitive.md | 22 +++++------- 4 files changed, 50 insertions(+), 15 deletions(-) create mode 100644 fonction d'ackermann de cori et lascar.md diff --git a/.obsidian/plugins/header-enhancer/data.json b/.obsidian/plugins/header-enhancer/data.json index ba18b5f3..756afa5c 100644 --- a/.obsidian/plugins/header-enhancer/data.json +++ b/.obsidian/plugins/header-enhancer/data.json @@ -16,7 +16,7 @@ "yamlDefaultStartNumber": "1", "yamlDefaultSeparator": ".", "globalAutoNumberingEnabled": true, - "perDocumentStates": "{\"suite finies d'entiers.md\":false,\"fonction récursive primitive.md\":false}", + "perDocumentStates": "{\"suite finies d'entiers.md\":false,\"fonction récursive primitive.md\":false,\"fonction d'ackermann de cori et lascar.md\":true}", "isSeparateHeaderFont": false, "headerFontFamily": "inherit", "headerFontSize": "inherit", diff --git a/S2 LOGOS . incomplétude et indécidabilité.md b/S2 LOGOS . incomplétude et indécidabilité.md index beae112a..d7f05aa4 100644 --- a/S2 LOGOS . incomplétude et indécidabilité.md +++ b/S2 LOGOS . incomplétude et indécidabilité.md @@ -13,6 +13,10 @@ BC-list-note-field: down --- - [[fonction récursive primitive]] + - sch - [[schéma mu borné|schéma µ borné]] - - [[suites finies d'entiers comme fonctions récursives primitives]] + - fonctions récursives primitives particulières : + - [[divisibilité#^recursive-primitive|prédicat de divisibilité]] + - [[fonction pi|fonction π]] + - [[suites finies d'entiers comme fonctions récursives primitives]] - [[ensemble récursif primitif]] diff --git a/fonction d'ackermann de cori et lascar.md b/fonction d'ackermann de cori et lascar.md new file mode 100644 index 00000000..f15c80ba --- /dev/null +++ b/fonction d'ackermann de cori et lascar.md @@ -0,0 +1,35 @@ +--- +up: + - "[[fonction récursive primitive]]" +tags: + - s/maths/logique + - s/informatique +aliases: +--- + + +> [!definition] [[fonction d'ackermann de cori et lascar]] +> [[fonction d'Ackermann]] modifiée pour la simplicité des preuves. +> On la note $\xi$, et on la définit comme suit : +> - $\forall x \in \mathbb{N},\quad \xi(0, x) = 2^{x}$ +> - $\forall y,\quad \xi(y, 0) = 1$ +> - $\forall x, y \in \mathbb{N},\quad \xi(y+1, x+1) = \xi(y, \xi(y+1, x))$ +> +> On pourra aussi noter : +> $\xi _{n}(x) = \xi(n, x)$ +^definition + +# Propriétés + +> [!proposition]+ Unicité +> La définition donnée désigne bien une unique fonction. +> > [!démonstration]- Démonstration +> > On utilise la notation $\xi _{n}$ et la récurrence : +> > $\begin{cases} \xi _{n}(0) = 1\\ \xi _{n}(x+1) = \xi _{n-1}(\xi _{n}(x)) \end{cases}$ +> > Cela établit clairement que chaque $\xi _{n}$ est bien définie, et donc que $\xi$ est unique. + +# Exemples + + + + diff --git a/fonction récursive primitive.md b/fonction récursive primitive.md index 789bcbd0..afc0bb78 100644 --- a/fonction récursive primitive.md +++ b/fonction récursive primitive.md @@ -11,8 +11,6 @@ header-auto-numbering: - state off --- - - > [!definition] [[fonction récursive primitive]] > On définit par [[induction]] l'ensemble des fonctions récursives primitives comme suit : > > [!definition] ensembles $\mathscr{F}_{p}$ et $\mathscr{F}$ @@ -68,7 +66,7 @@ header-auto-numbering: # Propriétés -> [!proposition]+ les fonctions récursives primitives possèdent des algorithmes les calculant +> [!proposition]- les fonctions récursives primitives possèdent des algorithmes les calculant > Il existe un algorithme pour calculer chacune des fonctions récursives primitives. > > [!démonstration]- Démonstration > > Cela est évident : @@ -90,7 +88,7 @@ header-auto-numbering: ## Fonctions élémentaires Dans cette section, on démontre que quelques fonctions élémentaires sont récursives primitives. -> [!proposition]+ L'addition est récursive primitive +> [!proposition]- L'addition est récursive primitive > La fonction d'addition $\lambda x y. x + y$ est récursive primitive > - dem $\operatorname{add} = \rho(P_1^{1}, S(P_3^{3}))$ > @@ -103,7 +101,7 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc > > ^addition -> [!proposition]+ La multiplication est récursive primitives +> [!proposition]- La multiplication est récursive primitives > $\operatorname{mult} =\lambda xy. x \times y$ est récursive primitive > - dem $\operatorname{mult} = \rho(C_1^{0}, \operatorname{add}(P_3^{3}, P_{3}^{1}))$ > @@ -113,12 +111,12 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc > > Comme on sait déjà que $\operatorname{add}$ est récursive primitive, il suit que $\operatorname{mult}$ l'est également ^multiplication -> [!proposition]+ La fonction puissance est récursive primitive +> [!proposition]- La fonction puissance est récursive primitive > $\operatorname{pow} = \lambda xy. x^{y}$ est récursive primitive > - dem $\operatorname{pow} = \rho(C_{1}^{1}, \operatorname{mult}(P_{3}^{3}, P_3^{1}))$ ^puissance -> [!proposition]+ La soustraction positive est récursive primitve +> [!proposition]- La soustraction positive est récursive primitve > On note $x \dot{-} y$ la soustraction avec un plancher à 0 : > $x \dot{-} y = \begin{cases} x-y \text{ si } x \geq y\\ 0 \text{ sinon} \end{cases}$ > La fonction $\lambda xy. x \dot{-} y$ est récursive primitive. @@ -134,7 +132,7 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc > > Maintenant, on peut définir $\operatorname{sub} = \lambda xy.x \dot{-} y$ comme : > > $\operatorname{sub} = \rho(P_1^{1}, \operatorname{prec}(P_3^{3}))$ -> [!proposition]+ La fonction signe est récursive primitive +> [!proposition]- La fonction signe est récursive primitive > On définit la [[fonction signe]] par : > $\operatorname{sg}: \begin{cases} \operatorname{sg}(0) = 0\\ \operatorname{sg(x) = 1 \text{ si } x \neq 0} \end{cases}$ (car on est sur $\mathbb{N}$) > Cette fonction est récursive primitive @@ -144,11 +142,11 @@ Dans cette section, on démontre que quelques fonctions élémentaires sont réc > > - $\operatorname{sg} = \rho(C_0^{0}, C_2^{1})$ > > Ce qui montre, dans tous les cas, que $\operatorname{sg}$ est récursive primitive -> [!proposition]+ Le prédicat $x>y$ est récursif primitif +> [!proposition]- Le prédicat $x>y$ est récursif primitif > Le prédiat $x>y$ est récursif primitif. > - dem ce prédicat est équivalent à $\operatorname{sg}(x \dot{-}y)$ -> [!proposition]+ Somme et produits limités +> [!proposition]- Somme et produits limités > Soit $f \in \mathscr{F}_{p+1}$ une fonction récursive primitive > Alors les fonctions : > - $g = \lambda x_1 x_2 \dots x_{p} y. \sum\limits_{t=0}^{y} f(x_1, x_2, \dots, x_{p}, t)$ @@ -235,7 +233,7 @@ On peut trouver de nouveaux schémas de définitions de fonctions qui sont stabl > Et ces fonctions $f$ et $f'$ sont récursives primitives dès que $g, g', h, h'$ sont toutes les quatres récursives primitives. > > > [!démonstration]- Démonstration -> > Pour montrer que $f$ et $f'$ sont prim-réc dès que $g, g', h$ et $h'$ le sont, introduisons la fonctions $k = \alpha_2(f, f')$. +> > Pour montrer que $f$ et $f'$ sont prim-réc dès que $g, g', h$ et $h'$ le sont, introduisons la fonctions $k = \alpha_2(f, f')$, en utilisant $\alpha_2$ qui bijecte les couples de $\mathbb{N}^{2}$ et les entiers de $\mathbb{N}$ (voir [[suites finies d'entiers comme fonctions récursives primitives]]) > > Comme $f$ et $f'$ sont en même temps dans cette fonction, on peut la définir d'un seul coup par schéma de récurrence. Pour cela, on mélange les deux valeurs de $f$ et $f'$ en une seule (c'est la valeur de $k$), et on la sépare à nouveau lors du calcul du schéma de récurrence. > > $k$ peut donc être définie comme suit : > > $k(\overline{x}, 0) = \alpha_2(g(\overline{x}), g'(\overline{x}))$ @@ -244,8 +242,6 @@ On peut trouver de nouveaux schémas de définitions de fonctions qui sont stabl ![[schéma mu borné#^main|schéma µ borné]] - - # Exemples > [!example] fonction partie entière $q(x, y)$